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!
I take the liberty to rename the data types. The first, which is
indexed on Set
will be called ListI
, and the second ListP
,
has Set
as a parameter:
data ListI : Set → Set₁ where
[] : {A : Set} → ListI A
_∷_ : {A : Set} → A → ListI A → ListI A
data ListP (A : Set) : Set where
[] : ListP A
_∷_ : A → ListP A → ListP A
In data types parameters go before the colon, and arguments after the colon are called indicies. The constructors can be used in the same way, you can apply the implicit set:
nilI : {A : Set} → ListI A
nilI {A} = [] {A}
nilP : {A : Set} → ListP A
nilP {A} = [] {A}
There difference comes when pattern matching. For the indexed version we have:
null : {A : Set} → ListI A → Bool
null ([] {A}) = true
null (_∷_ {A} _ _) = false
This cannot be done for ListP
:
-- does not work
null′ : {A : Set} → ListP A → Bool
null′ ([] {A}) = true
null′ (_∷_ {A} _ _) = false
The error message is
The constructor [] expects 0 arguments, but has been given 1
when checking that the pattern [] {A} has type ListP A
ListP
can also be defined with a dummy module, as ListD
:
module Dummy (A : Set) where
data ListD : Set where
[] : ListD
_∷_ : A → ListD → ListD
open Dummy public
Perhaps a bit surprising, ListD
is equal to ListP
. We cannot pattern
match on the argument to Dummy
:
-- does not work
null″ : {A : Set} → ListD A → Bool
null″ ([] {A}) = true
null″ (_∷_ {A} _ _) = false
This gives the same error message as for ListP
.
ListP
is an example of a parameterised data type, which is simpler
than ListI
, which is an inductive family: it "depends" on the
indicies, although in this example in a trivial way.
Parameterised data types are defined on the wiki, and here is a small introduction.
Inductive families are not really defined, but elaborated on in the wiki with the canonical example of something that seems to need inductive families:
data Term (Γ : Ctx) : Type → Set where
var : Var Γ τ → Term Γ τ
app : Term Γ (σ → τ) → Term Γ σ → Term Γ τ
lam : Term (Γ , σ) τ → Term Γ (σ → τ)
Disregarding the Type index, a simplified version of this could not be
written with in the Dummy
-module way because of lam
constructor.
Another good reference is Inductive Families by Peter Dybjer from 1997.
Happy Agda coding!
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With