Hello,<br><br>I suppose Lennart is referring to type-level [1]. But type-level uses functional dependencies, right?<br><br>There is also tfp [2], which uses type families. In general, how would you say your work compares to these two?<br>
<br><br>Thanks,<br>Pedro<br><br>[1] <a href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level">http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level</a><br>[2] <a href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/tfp">http://hackage.haskell.org/cgi-bin/hackage-scripts/package/tfp</a><br>
<br><div class="gmail_quote">On Mon, Mar 30, 2009 at 08:22, Lennart Augustsson <span dir="ltr"><<a href="mailto:lennart@augustsson.net">lennart@augustsson.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
There is already a library for type level number, called typelevel.<br>
It's nice because it uses decimal representation of numbers and can<br>
handle numbers of reasonable size.<br>
I use it in the LLVM bindings.<br>
<font color="#888888"><br>
-- Lennart<br>
</font><div><div></div><div class="h5"><br>
On Mon, Mar 30, 2009 at 1:07 AM, spoon <<a href="mailto:spoon@killersmurf.com">spoon@killersmurf.com</a>> wrote:<br>
> I've been doing some basic work on a support library for type level<br>
> programming ( see<br>
> <a href="http://hackage.haskell.org/trac/summer-of-code/ticket/1541" target="_blank">http://hackage.haskell.org/trac/summer-of-code/ticket/1541</a> ). I know<br>
> there have been similar attempts using fundeps ( Edward Kmett showed me<br>
> some of his work, but I've lost the address... ) but this approach uses<br>
> type families.<br>
><br>
> Anyway, I would like to hear your critique!<br>
><br>
> Currently I have higher order type functions and ad-hoc parametrized<br>
> functions.<br>
><br>
> Here's what foldl looks like:<br>
><br>
> type family Foldl ( func :: * -> * -> * ) val list<br>
> type instance Foldl func val ( Cons first rest ) = Foldl func ( Eval<br>
> ( func val first ) ) rest<br>
> type instance Foldl func val Nill = val<br>
><br>
> Notice the use of Eval - this is a trick to enable us to pass around<br>
> data with kind * -> *, or whatever, and then trip this into becoming a<br>
> value. Here's an example, using this trick to define factorial:<br>
><br>
> -- multiplication<br>
> type family Times x y<br>
> type instance Times x Zero = Zero<br>
> type instance Times x ( Succ y ) = Sum x ( Times x y )<br>
><br>
> -- The "first order" function version of Times<br>
> data TimesL x y<br>
><br>
> -- Where what Eval forced TimesL to become.<br>
> type instance Eval ( TimesL x y ) = Times x y<br>
><br>
> -- multiplies all the elements of list of Nat together<br>
> type Product l =<br>
> Foldl TimesL ( Succ Zero ) l<br>
><br>
> -- here list to creates a list from ( Succ Zero ) to the given number<br>
> type Factorial x =<br>
> Product ( ListTo x )<br>
><br>
> We can now use the function like this:<br>
><br>
> *TPrelude> result ( ) :: Factorial ( Succ ( Succ ( Succ ( Zero ) ) ) )<br>
> Succ (Succ (Succ (Succ (Succ (Succ Zero)))))<br>
><br>
> Using the parametrized types kinda reminds me of programming in Erlang:<br>
><br>
> -- What would conventionally be the monad type class, parametized over m<br>
> type family Bind m ma ( f :: * -> * )<br>
> type family Return m a<br>
> type family Sequence m ma mb<br>
><br>
> Here's the maybe monad:<br>
><br>
> -- Monad instance<br>
> type instance Bind ( Maybe t ) Nothing f = Nothing<br>
> type instance Bind ( Maybe t ) ( Just a ) f = Eval ( f a )<br>
> type instance Sequence ( Maybe t ) Nothing a = Nothing<br>
> type instance Sequence ( Maybe t ) ( Just a ) b = b<br>
> type instance Return ( Maybe t ) a = Just a<br>
><br>
> type instance Eval ( Just x ) = Just x<br>
><br>
> Here's an example:<br>
> *TPrelude> result ( ) :: Bind ( Maybe Nat ) ( Just Zero ) Just<br>
> Just Zero<br>
><br>
> For more information and to download the loose collection of module<br>
> implementing this please see:<br>
> <a href="http://www.killersmurf.com/projects/typelib" target="_blank">http://www.killersmurf.com/projects/typelib</a><br>
><br>
> John Morrice<br>
><br>
> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>