Spencer Janssen wrote: ] Here's an attempt with GADTs: ] ] \begin{code} ] {-# OPTIONS_GHC -fglasgow-exts #-} ] data Succ a ] data Zero ] data Seq a b where ] Cons :: a -> Seq a b -> Seq a (Succ b) ] Nil :: Seq a Zero ] \end{code} ] ] Seems to work for me.
Hmm. Maybe I'm missing something. With the program below I get the following error message (with ghci 6.6)... Couldn't match expected type `Succ Zero' against inferred type `Zero' Expected type: Succ (Succ (Succ Zero)) Inferred type: Succ (Succ Zero) In the first argument of `Cons', namely `two' In the second argument of `Cons', namely `(Cons two (Cons one Nil))' > {-# OPTIONS -fglasgow-exts #-} > > data Succ a = S a deriving Show > data Zero = Z deriving Show > > zero = Z > one = S zero > two = S one > three = S two > > data Seq a b where > Cons :: a -> Seq a b -> Seq a (Succ b) > Nil :: Seq a Zero > > decreasing = Cons three (Cons two (Cons one Nil)) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe