Re: [Haskell-cafe] Type level functions (type of decreasing list)

17 Oct 2006


      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))

Re: [Haskell-cafe] Type level functions (type of decreasing list)

Greg Buchholz