I like this one:<br><br>-----------------------------------------------------------------------------<br><br>data N a where<br> Z :: N ()<br> N :: N a -> N (N a)<br><br>type family Nest n (f :: * -> *) a<br>
nest :: N n -> (forall a. a -> f a) -> a -> 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> nest $(nat 18) (:[]) 42<br>[[[[[[[[[[[[[[[[[[[42]]]]]]]]]]]]]]]]]]]<br>-}<br>
<br>-- ghci> toInt $(nat 1000)<br>-- 1000<br>toInt :: N a -> Int<br>toInt = go 0<br> where go :: Int -> N a -> 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 -> ExpQ<br>nat n<br> | n < 1 = [|Z|]<br> | otherwise = [|N $(nat (n-1))|]<br><br>instance Show (N a) where<br> showsPrec _ Z = showString "Z"<br> showsPrec p (N x_1)<br> = showParen (p > 10)<br>
(showString "N" . (showChar ' ' . (showsPrec 11 x_1 . id)))<br><br>-----------------------------------------------------------------------------<br><br>-- :(<br><br>{-<br>ghci> 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]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wx} :: {Show [[t_a1U3]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Ww} :: {Show [[[t_a1U3]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wv} :: {Show [[[[t_a1U3]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wu} :: {Show [[[[[t_a1U3]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wt} :: {Show [[[[[[t_a1U3]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Ws} :: {Show [[[[[[[t_a1U3]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wr} :: {Show [[[[[[[[t_a1U3]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wq} :: {Show [[[[[[[[[t_a1U3]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wp} :: {Show [[[[[[[[[[t_a1U3]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wo} :: {Show [[[[[[[[[[[t_a1U3]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wn} :: {Show [[[[[[[[[[[[t_a1U3]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wm} :: {Show [[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]}'<br>
arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wl} :: {Show [[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wk} :: {Show [[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wj} :: {Show [[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]}'<br>
arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wi} :: {Show [[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
`$dShow{a1Wh} :: {Show [[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Wg} :: {Show<br> [[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]}'<br>
arising from a use of `print' at <interactive>:1:0-22<br> `$dShow{a1Um} :: {Show<br> [[[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]]}'<br> arising from a use of `print' at <interactive>:1:0-22<br>
-}<br><br>-----------------------------------------------------------------------------<br><br>Also, Dan Doel wrote an Agda version of `nest' which<br>eliminates the duplication, but interestingly requires<span id="li-2429-1"><span class="cm"><br>
'--type-in-type</span></span>':<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"><<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>></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;">
> induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S x)) -> p n<br>
> induction n z s = caseNat n isZ isS where<br>
> isZ :: n ~ Z => p n<br>
> isZ = z<br>
> isS :: forall x. (n ~ S x, Nat x) => x -> p n<br>
> 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>