[Haskell-cafe] type-level programming support library

[Edward Kmett]

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
<lennart at augustsson.net>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 <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
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090330/7e7944f2/attachment.htm