---------- Forwarded message ----------
From: Pablo Nogueira
Date: 31-Jan-2007 12:04
Subject: Re: [Haskell-cafe] GADTs: the plot thickens?
To: Conor McBride
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.
