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

[Greg Buchholz]

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