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 differ…

Accepted Answer

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!

Parametrized Inductive Types in Agda

Solution

Problem