Parametrized Inductive Types in Agda
Question
I'm just reading Dependent Types at Work. In the introduction to parametrised types, the author mentions that in this declaration
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
the type of List
is Set → Set
and that A
becomes implicit argument to both constructors, ie.
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
Well, I tried to rewrite it a bit differently
data List : Set → Set where
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
which sadly doesn't work (I'm trying to learn Agda for two days or so, but from what I gathered it's because the constructors are parametrised over Set₀
and so List A
must be in Set₁
).
Indeed, the following is accepted
data List : Set₀ → Set₁ where
[] : {A : Set₀} → List A
_::_ : {A : Set₀} → A → List A → List A
however, I'm no longer able to use {A : Set} → ... → List (List A)
(which is perfectly understandable).
So my question: What is the actual difference between List (A : Set) : Set
and List : Set → Set
?
Thanks for your time!
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow