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.
Spencer Janssen
On Oct 17, 2006, at 6:37 PM, Greg Buchholz wrote:
I'm wondering about creating a data structure that has the type of
decreasing numbers. If I want an increasing list, it is easy...
{-# OPTIONS -fglasgow-exts #-}
data Succ a = S a deriving Show
data Zero = Z deriving Show
data Seq' a = Cons' a (Seq' (Succ a)) | Nil' deriving Show
...which can be used like...
zero = Z
one = S zero
two = S one
three = S two
increasing = Cons' zero (Cons' one (Cons' two (Cons' three Nil')))
...on the other hand, if I want the decreasing list, I can try...
class Pre a b | a -> b
instance Pre (Succ a) a
instance Pre Zero Zero
data (Pre a b) => Seq a = Cons a (Seq b) | Nil
decreasing = Cons three (Cons two (Cons one Nil))
...but that complains about "Not in scope: type variable `b'". Of
course that makes perfect sense, but I'd like to know if there is a
Haskell idiom that I'm missing in order to get this to work.
Thanks,
Greg Buchholz
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
