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

[Spencer Janssen]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe