[Haskell-cafe] type-level programming support library

[Lennart Augustsson]

I wasn't questioning the utility of John's library.
But I saw him mentioning unary numbers and I think it's a mistake to
use those for anything practical involving even moderately sized
numbers.

I'd love to see a good type level programming library.  There's a lot
of it out there, but it's never packaged in a way that is reusable as
a good library.

  -- Lennart

2009/3/30 Edward Kmett <ekmett at gmail.com>:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>