[Haskell-cafe] type-level programming support library

[spoon]

I've been doing some basic work on a support library for type level
programming ( see
http://hackage.haskell.org/trac/summer-of-code/ticket/1541 ).  I know
there have been similar attempts using fundeps ( Edward Kmett showed me
some of his work, but I've lost the address... ) but this approach uses
type families. 

Anyway, I would like to hear your critique!

Currently I have higher order type functions and ad-hoc parametrized
functions.

Here's what foldl looks like:

type family Foldl ( func :: * -> * -> * ) val list
type instance Foldl func val ( Cons first rest ) = Foldl func ( Eval
( func val first ) ) rest
type instance Foldl func val Nill = val

Notice the use of Eval - this is a trick to enable us to pass around
data with kind * -> *, or whatever, and then trip this into becoming a
value. Here's an example, using this trick to define factorial: 

-- multiplication 
type family Times x y 
type instance Times x Zero = Zero 
type instance Times x ( Succ y ) = Sum x ( Times x y ) 

-- The "first order" function version of Times 
data TimesL x y 

-- Where what Eval forced TimesL to become. 
type instance Eval ( TimesL x y ) = Times x y 

-- multiplies all the elements of list of Nat together 
type Product l = 
   Foldl TimesL ( Succ Zero ) l 

-- here list to creates a list from ( Succ Zero ) to the given number
type Factorial x = 
   Product ( ListTo x ) 

We can now use the function like this: 

*TPrelude> result ( ) :: Factorial ( Succ ( Succ ( Succ ( Zero ) ) ) ) 
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))

Using the parametrized types kinda reminds me of programming in Erlang:

-- What would conventionally be the monad type class, parametized over m 
type family Bind m ma ( f :: * -> * ) 
type family Return m a 
type family Sequence m ma mb 

Here's the maybe monad: 

-- Monad instance 
type instance Bind ( Maybe t ) Nothing f = Nothing 
type instance Bind ( Maybe t ) ( Just a ) f = Eval ( f a ) 
type instance Sequence ( Maybe t ) Nothing a = Nothing 
type instance Sequence ( Maybe t ) ( Just a ) b = b  
type instance Return ( Maybe t ) a = Just a 

type instance Eval ( Just x ) = Just x

Here's an example:
*TPrelude> result ( ) :: Bind ( Maybe Nat ) ( Just Zero ) Just
Just Zero

For more information and to download the loose collection of module
implementing this please see:
http://www.killersmurf.com/projects/typelib

John Morrice