<div>Lennart,</div>
<div> </div>
<div>I think the major emphasis that John&#39;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. </div>

<div> </div>
<div>I think his type family approach for type-level monads for instance is pretty neat and quite readable.</div>
<div> </div>
<div>The biggest problem that I see with the approach is the general lack of availability of currying due to Haskell not having &#39;polymorphic kinds&#39;. So he&#39;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.</div>

<div> </div>
<div>John, </div>
<div> </div>
<div><a href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-int">http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-int</a></div>
<div> </div>
<div>contains my old type level 2s and 16s complement integer code and some machinery for manipulating type level lists a la HList.</div>
<div> </div>
<div>-Edward Kmett</div>
<div> </div>
<div> </div>
<div> </div>
<div class="gmail_quote">On Mon, Mar 30, 2009 at 3:22 AM, Lennart Augustsson <span dir="ltr">&lt;<a href="mailto:lennart@augustsson.net">lennart@augustsson.net</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">There is already a library for type level number, called typelevel.<br>It&#39;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 &lt;<a href="mailto:spoon@killersmurf.com">spoon@killersmurf.com</a>&gt; wrote:<br>&gt; I&#39;ve been doing some basic work on a support library for type level<br>
&gt; programming ( see<br>&gt; <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>&gt; there have been similar attempts using fundeps ( Edward Kmett showed me<br>
&gt; some of his work, but I&#39;ve lost the address... ) but this approach uses<br>&gt; type families.<br>&gt;<br>&gt; Anyway, I would like to hear your critique!<br>&gt;<br>&gt; Currently I have higher order type functions and ad-hoc parametrized<br>
&gt; functions.<br>&gt;<br>&gt; Here&#39;s what foldl looks like:<br>&gt;<br>&gt; type family Foldl ( func :: * -&gt; * -&gt; * ) val list<br>&gt; type instance Foldl func val ( Cons first rest ) = Foldl func ( Eval<br>&gt; ( func val first ) ) rest<br>
&gt; type instance Foldl func val Nill = val<br>&gt;<br>&gt; Notice the use of Eval - this is a trick to enable us to pass around<br>&gt; data with kind * -&gt; *, or whatever, and then trip this into becoming a<br>&gt; value. Here&#39;s an example, using this trick to define factorial:<br>
&gt;<br>&gt; -- multiplication<br>&gt; type family Times x y<br>&gt; type instance Times x Zero = Zero<br>&gt; type instance Times x ( Succ y ) = Sum x ( Times x y )<br>&gt;<br>&gt; -- The &quot;first order&quot; function version of Times<br>
&gt; data TimesL x y<br>&gt;<br>&gt; -- Where what Eval forced TimesL to become.<br>&gt; type instance Eval ( TimesL x y ) = Times x y<br>&gt;<br>&gt; -- multiplies all the elements of list of Nat together<br>&gt; type Product l =<br>
&gt;   Foldl TimesL ( Succ Zero ) l<br>&gt;<br>&gt; -- here list to creates a list from ( Succ Zero ) to the given number<br>&gt; type Factorial x =<br>&gt;   Product ( ListTo x )<br>&gt;<br>&gt; We can now use the function like this:<br>
&gt;<br>&gt; *TPrelude&gt; result ( ) :: Factorial ( Succ ( Succ ( Succ ( Zero ) ) ) )<br>&gt; Succ (Succ (Succ (Succ (Succ (Succ Zero)))))<br>&gt;<br>&gt; Using the parametrized types kinda reminds me of programming in Erlang:<br>
&gt;<br>&gt; -- What would conventionally be the monad type class, parametized over m<br>&gt; type family Bind m ma ( f :: * -&gt; * )<br>&gt; type family Return m a<br>&gt; type family Sequence m ma mb<br>&gt;<br>&gt; Here&#39;s the maybe monad:<br>
&gt;<br>&gt; -- Monad instance<br>&gt; type instance Bind ( Maybe t ) Nothing f = Nothing<br>&gt; type instance Bind ( Maybe t ) ( Just a ) f = Eval ( f a )<br>&gt; type instance Sequence ( Maybe t ) Nothing a = Nothing<br>
&gt; type instance Sequence ( Maybe t ) ( Just a ) b = b<br>&gt; type instance Return ( Maybe t ) a = Just a<br>&gt;<br>&gt; type instance Eval ( Just x ) = Just x<br>&gt;<br>&gt; Here&#39;s an example:<br>&gt; *TPrelude&gt; result ( ) :: Bind ( Maybe Nat ) ( Just Zero ) Just<br>
&gt; Just Zero<br>&gt;<br>&gt; For more information and to download the loose collection of module<br>&gt; implementing this please see:<br>&gt; <a href="http://www.killersmurf.com/projects/typelib" target="_blank">http://www.killersmurf.com/projects/typelib</a><br>
&gt;<br>&gt; John Morrice<br>&gt;<br>&gt; _______________________________________________<br>&gt; Haskell-Cafe mailing list<br>&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;<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>