[Haskell-cafe] type-level programming support library

[Lennart Augustsson]

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