I like this one:<br><br>-----------------------------------------------------------------------------<br><br>data N a where<br>  Z :: N ()<br>  N :: N a -&gt; N (N a)<br><br>type family Nest  n      (f ::        * -&gt; *)    a<br>
nest ::           N n -&gt; (forall a. a -&gt; f a) -&gt; a -&gt; Nest n f a<br>type instance Nest  ()   f a = f a<br>nest                Z    f a = f a<br>nest               (N n) f a = f (nest n f a)<br>type instance Nest (N n) f a = f (Nest n f a)<br>
<br>-----------------------------------------------------------------------------<br><br>import Language.Haskell.TH.Lib(ExpQ)<br><br>{-<br>ghci&gt; nest $(nat 18) (:[]) 42<br>[[[[[[[[[[[[[[[[[[[42]]]]]]]]]]]]]]]]]]]<br>-}<br>
<br>-- ghci&gt; toInt $(nat 1000)<br>-- 1000<br>toInt :: N a -&gt; Int<br>toInt = go 0<br>  where go :: Int -&gt; N a -&gt; Int<br>        go n  Z     = n<br>        go n (N a) = go (n+1) a<br><br>-- TH, since no dep types<br>
nat :: Int -&gt; ExpQ<br>nat n<br>  | n &lt; 1     = [|Z|]<br>  | otherwise = [|N $(nat (n-1))|]<br><br>instance Show (N a) where<br>  showsPrec _ Z = showString &quot;Z&quot;<br>  showsPrec p (N x_1)<br>    = showParen (p &gt; 10)<br>
        (showString &quot;N&quot; . (showChar &#39; &#39; . (showsPrec 11 x_1 . id)))<br><br>-----------------------------------------------------------------------------<br><br>-- :(<br><br>{-<br>ghci&gt; nest $(nat 19) (:[]) 42<br>
<br>Top level:<br>    Context reduction stack overflow; size = 20<br>    Use -fcontext-stack=N to increase stack size to N<br>        `$dShow{a1Wy} :: {Show [t_a1U3]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wx} :: {Show [[t_a1U3]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Ww} :: {Show [[[t_a1U3]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wv} :: {Show [[[[t_a1U3]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wu} :: {Show [[[[[t_a1U3]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wt} :: {Show [[[[[[t_a1U3]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Ws} :: {Show [[[[[[[t_a1U3]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wr} :: {Show [[[[[[[[t_a1U3]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wq} :: {Show [[[[[[[[[t_a1U3]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wp} :: {Show [[[[[[[[[[t_a1U3]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wo} :: {Show [[[[[[[[[[[t_a1U3]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wn} :: {Show [[[[[[[[[[[[t_a1U3]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wm} :: {Show [[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]}&#39;<br>
          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wl} :: {Show [[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wk} :: {Show [[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wj} :: {Show [[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]}&#39;<br>
          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wi} :: {Show [[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
        `$dShow{a1Wh} :: {Show [[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Wg} :: {Show<br>                            [[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]}&#39;<br>
          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>        `$dShow{a1Um} :: {Show<br>                            [[[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]]}&#39;<br>          arising from a use of `print&#39; at &lt;interactive&gt;:1:0-22<br>
-}<br><br>-----------------------------------------------------------------------------<br><br>Also, Dan Doel wrote an Agda version of `nest&#39; which<br>eliminates the duplication, but interestingly requires<span id="li-2429-1"><span class="cm"><br>
&#39;--type-in-type</span></span>&#39;:<br><br><a href="http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=2429">http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=2429</a><br><br>Matt<br><br>On Wed, Jun 10, 2009 at 10:01 PM, Ryan Ingram <span dir="ltr">&lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt;</span> wrote:<br>
<div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
&gt; induction :: forall p n. Nat n =&gt; n -&gt; p Z -&gt; (forall x. Nat x =&gt; p x -&gt; p (S x)) -&gt; p n<br>
&gt; induction n z s = caseNat n isZ isS where<br>
&gt;    isZ :: n ~ Z =&gt; p n<br>
&gt;    isZ = z<br>
&gt;    isS :: forall x. (n ~ S x, Nat x) =&gt; x -&gt; p n<br>
&gt;    isS x = s (induction x z s)<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>
</blockquote></div><br>