Re: [Haskell-cafe] type-level programming support library

Lennart, I think the major emphasis that John's library has is on doing things other than numbers well in the type system, using the type family syntax to avoid the proliferation of intermediary names that the fundep approach yields. I think his type family approach for type-level monads for instance is pretty neat and quite readable. The biggest problem that I see with the approach is the general lack of availability of currying due to Haskell not having 'polymorphic kinds'. So he'd have to use Curry combinators that are specific to both the number of arguments at the kinds of the arguments that a function has. John, http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-int contains my old type level 2s and 16s complement integer code and some machinery for manipulating type level lists a la HList. -Edward Kmett On Mon, Mar 30, 2009 at 3:22 AM, Lennart Augustsson wrote:

There is already a library for type level number, called typelevel. It's nice because it uses decimal representation of numbers and can handle numbers of reasonable size. I use it in the LLVM bindings.

-- Lennart

On Mon, Mar 30, 2009 at 1:07 AM, spoon wrote:

...

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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe