[Haskell-cafe] type-level programming support library

[José Pedro Magalhães]

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 <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/5da97f60/attachment.htm