[Agda] Parameterized type families

[Matthieu Sozeau]

Le 29 oct. 08 à 10:52, Dan Doel a écrit :

> On Sunday 26 October 2008 6:14:37 pm Conor McBride wrote:
>> I'm not sure this is quite the whole story. Consider this
>> small collection of examples:
> ...
>> data Tm (n : Nat) : Set where
>>  var : Fin n -> Tm n
>>  app : Tm n -> Tm n -> Tm n
>>  lam : Tm (suc n) -> Tm n
>
> I'm not well read on this subject, but Tm is (modulo lifting  
> naturals to the
> type level) a perfectly ordinary algebraic type in Haskell (for  
> instance) is
> it not?
>
>   {-# LANGUAGE EmptyDataDecls, GADTs #-}
>
>   data Z
>   data S n
>
>   data Fin n where
>     FZ :: Fin (S n)
>     FS :: Fin n -> Fin (S n)
>
>   data Tm n = Var (Fin n)
>             | App (Tm n) (Tm n)
>             | Lam (Tm (S n))
>
> Are Haskell 98 algebraic datatypes not merely parameterized, but in  
> some cases
> indexed? Or is this a distinction that makes sense in the sort of  
> type theory
> underlying Agda, but not Haskell? Or am I missing something else  
> entirely?

The Tm datatype is nested in the Lam case, which is a restricted case  
of indexed family:
the constructors all build a term in the same instance but the  
constructors may contain
objects in varying instances. The pattern-matching problem related to  
nested datatypes is
simpler than for full inductive families, and is supported in ML or  
Haskell. However, to
write recursive functions on these datatypes you need polymorphic  
recursion (your recursive
calls are on (Tm (S n)) not (Tm n)), which only Haskell supports.

Hope this helps,
-- Matthieu