Type level functions (type of decreasing list)
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
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
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))
Greg, What about the following (tested with GHC 6.6)? {-# OPTIONS -fglasgow-exts #-} data Zero = Zero data Succ n = Succ n zero = Zero one = Succ zero two = Succ one three = Succ two -- etc data Seq :: * -> * where Nil :: Seq Zero Cons :: Succ n -> Seq n -> Seq (Succ n) mySeq = Cons three (Cons two (Cons one Nil)) HTH, Stefan
participants (3)
-
Greg Buchholz -
Spencer Janssen -
Stefan Holdermans