[Agda] Parameterized type families

[Conor McBride]

Hi all

On 22 Oct 2008, at 13:11, Nils Anders Danielsson wrote:

> lvaro Garca Prez wrote:
>
>> Do anybody know the differences between declaring one argument  
>> before the colon or after the colon in a data definition?
>
> See the Agda wiki:
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php? 
> n=Docs.DatatypeAndFunctionDefinitions.

I'm not sure this is quite the whole story. Consider this
small collection of examples:

{---------------------------------------------------------------------}

{- This example has neither parameters nor indices. -}

data Nat : Set where
   zero : Nat
   suc : Nat -> Nat

{- This example has a parameter, the element set X. -}

data List (X : Set) : Set where
   [] : List X
   _::_ : X -> List X -> List X

{- What makes X a parameter is that each special case
    can be defined individually. -}

data ListNat : Set where
   [] : ListNat
   _::_ : Nat -> ListNat -> ListNat

{- Meanwhile, here is Fin, indexed by natural numbers. The
    whole family is defined by mutual induction. Individual constructors
    may target specialized index subsets, e.g., nonzero numbers. -}

data Fin : Nat -> Set where
   zero : {n : Nat} -> Fin (suc n)
   suc : {n : Nat} -> Fin n -> Fin (suc n)

{- But here are the de Bruijn terms, necessarily defined by
    mutual induction, indexed rather than parametrized by natural
    numbers. Yet the index is left of the colon. -}

data Tm (n : Nat) : Set where
   var : Fin n -> Tm n
   app : Tm n -> Tm n -> Tm n
   lam : Tm (suc n) -> Tm n

{---------------------------------------------------------------------}

So, the left-or-right of the colon distinction is *not* the traditional
parameter-or-index distinction (nomenclature from P. Dybjer?). Rather,
it's the contentious sectarian distinction between (right of colon)
indices you can specialize in a return type and (left of colon) indices
you can only specialize in a recursive reference (eg the body of lam),
with parameters the trivial case where specialization happens nowhere.
And here we find all our old favourite issues about "restricted" (Agda
1) versus "general" (Agda 2) inductive families, intensional equality
types, the K rule,...

What these left of colon indices have in common with parameters is that
in a bidirectional type system, there is no need to store them in data:
they come in from the type. But there may be other distinctions which
should be drawn between parameters and indices and are currently not.
Should they be subject to the same "size" restrictions? Is it important
to be clear what we're taking fixpoints over?

Is there a case to revive the parameter-index distinction?

Cheers

Conor