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

Hello, I suppose Lennart is referring to type-level [1]. But type-level uses functional dependencies, right? There is also tfp [2], which uses type families. In general, how would you say your work compares to these two? Thanks, Pedro [1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level [2] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/tfp On Mon, Mar 30, 2009 at 08:22, 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