Я просто читаю зависимые типы в работе. Во введении к параметризованным типам автор упоминает, что в этой декларации
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
тип List
равен Set → Set
и что A
становится неявным аргументом для обоих конструкторов, т.е.
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
Ну, я попытался переписать его несколько иначе
data List : Set → Set where
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
который, к сожалению, не работает (я пытаюсь узнать Agda в течение двух дней или около того, но из того, что я собрал, потому что конструкторы параметризованы над Set₀
и поэтому List A
должен быть в Set₁
)..
В самом деле, принято следующее
data List : Set₀ → Set₁ where
[] : {A : Set₀} → List A
_::_ : {A : Set₀} → A → List A → List A
однако я больше не могу использовать {A : Set} → ... → List (List A)
(что совершенно понятно).
Итак, мой вопрос: какова фактическая разница между List (A : Set) : Set
и List : Set → Set
?
Спасибо за ваше время!