Fwd: [Haskell-cafe] GADTs: the plot thickens?

[Pablo Nogueira]

---------- Forwarded message ----------
From: Pablo Nogueira <pirelo at googlemail.com>
Date: 31-Jan-2007 12:04
Subject: Re: [Haskell-cafe] GADTs: the plot thickens?
To: Conor McBride <ctm at cs.nott.ac.uk>


I haven't tried this yet, but would declaring the class Nat be a starting point?

class Nat n
instance Nat Z
instance Nat n => Nat (S n)

data Fin :: * -> * where
   Fz :: Nat n => Fin (S n)
   Fs :: Nat n => Fin n -> Fin (S n)

thin :: Nat n => Fin (S n) -> Fin n -> Fin (S n)
thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)

Btw, apparently we have to use GHC HEAD if we want GADTs to compile properly.

The error seems very similar to the one you get when trying to write
(++) for dependent lists with length encoded as GADTs. To make sure I
understand,  you are asking if there is a hack that will enable us to
tell the Haskell type checker that  n = (S n1), right?

Regards,
P.