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
scroll top