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

[oleg at pobox.com]

Greg Buchholz wrote:
>     I'm wondering about creating a data structure that has the type of
> decreasing numbers. 
> 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'"

One way is to use existentials:

> data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1
>
> decreasing1 = Cons1 three (Cons1 two (Cons1 one Nil1))

which perhaps not entirely satisfactory because we have to specify all
the needed classes in the definition of Seq1.

Perhaps a better -- and a more general alternative -- is to use
type-level programming to its fullest. The following defines a list
whose elements are constrained to be in the decreasing, increasing,
or any other (defined in the future) order. This example shows that
Haskell truly has more kinds than it is commonly acknowledged.

For more details on constrained lists (list of odd numerals, even
numerals, etc), please see the following implementation of Tim
Sheard's `Half' example
	http://pobox.com/~oleg/ftp/Haskell/Half.hs

> data Succ a = S a
> data Zero   = Z
>
> zero  = Z
> one   = S zero
> two   = S one
> three = S two
>
> class KIND l a b
>
> data Cons a b = Cons a b
> data Nil = Nil
>
>
> data Increasing = Increasing
> instance KIND Increasing a (Succ a)
> data Decreasing = Decreasing
> instance KIND Decreasing (Succ a) a
> -- one can add non-increasing, non-decreasing, etc.
> 
> class ConstrainedL c l
> instance ConstrainedL c Nil
> instance ConstrainedL c (Cons a Nil)
> instance (KIND c a b, ConstrainedL c (Cons  b l))
>     => ConstrainedL c (Cons a (Cons b l))
>
> -- smart constructors. 
> -- Alternatively, define 
>    as_increasing :: ConstrainedL Increasing l => l -> l
> consi :: ConstrainedL Increasing (Cons a l) => a -> l -> Cons a l
> consi = Cons

> consd :: ConstrainedL Decreasing (Cons a l) => a -> l -> Cons a l
> consd = Cons

> incr =  consi one (consi two (consi three Nil))
> -- No instance for (KIND Increasing (Succ Zero) (Succ (Succ (Succ Zero))))
> -- incr1 = consi one (consi three Nil)

> decr =  consd three (consd two (consd one Nil))

-- No instance for (KIND Decreasing (Succ (Succ Zero)) (Succ (Succ (Succ Zero))
-- decr1 =  consd three (consd two (consd three Nil))