---------- Forwarded message ---------- From: Pablo Nogueira <[EMAIL PROTECTED]> Date: 31-Jan-2007 12:04 Subject: Re: [Haskell-cafe] GADTs: the plot thickens? To: Conor McBride <[EMAIL PROTECTED]>
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
