[Agda] Parameterized type families

[Dan Doel]

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?

Cheers,
Dan