I like this one:
-----------------------------------------------------------------------------
data N a where
Z :: N ()
N :: N a -> N (N a)
type family Nest n (f :: * -> *) a
nest :: N n -> (forall a. a -> f a) -> a -> Nest n f a
type instance Nest () f a = f a
nest Z f a = f a
nest (N n) f a = f (nest n f a)
type instance Nest (N n) f a = f (Nest n f a)
-----------------------------------------------------------------------------
import Language.Haskell.TH.Lib(ExpQ)
{-
ghci> nest $(nat 18) (:[]) 42
[[[[[[[[[[[[[[[[[[[42]]]]]]]]]]]]]]]]]]]
-}
-- ghci> toInt $(nat 1000)
-- 1000
toInt :: N a -> Int
toInt = go 0
where go :: Int -> N a -> Int
go n Z = n
go n (N a) = go (n+1) a
-- TH, since no dep types
nat :: Int -> ExpQ
nat n
| n < 1 = [|Z|]
| otherwise = [|N $(nat (n-1))|]
instance Show (N a) where
showsPrec _ Z = showString "Z"
showsPrec p (N x_1)
= showParen (p > 10)
(showString "N" . (showChar ' ' . (showsPrec 11 x_1 . id)))
-----------------------------------------------------------------------------
-- :(
{-
ghci> nest $(nat 19) (:[]) 42
Top level:
Context reduction stack overflow; size = 20
Use -fcontext-stack=N to increase stack size to N
`$dShow{a1Wy} :: {Show [t_a1U3]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wx} :: {Show [[t_a1U3]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Ww} :: {Show [[[t_a1U3]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wv} :: {Show [[[[t_a1U3]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wu} :: {Show [[[[[t_a1U3]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wt} :: {Show [[[[[[t_a1U3]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Ws} :: {Show [[[[[[[t_a1U3]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wr} :: {Show [[[[[[[[t_a1U3]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wq} :: {Show [[[[[[[[[t_a1U3]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wp} :: {Show [[[[[[[[[[t_a1U3]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wo} :: {Show [[[[[[[[[[[t_a1U3]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wn} :: {Show [[[[[[[[[[[[t_a1U3]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wm} :: {Show [[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wl} :: {Show [[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wk} :: {Show [[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wj} :: {Show [[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wi} :: {Show [[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wh} :: {Show [[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Wg} :: {Show
[[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
`$dShow{a1Um} :: {Show
[[[[[[[[[[[[[[[[[[[[t_a1U3]]]]]]]]]]]]]]]]]]]]}'
arising from a use of `print' at <interactive>:1:0-22
-}
-----------------------------------------------------------------------------
Also, Dan Doel wrote an Agda version of `nest' which
eliminates the duplication, but interestingly requires
'--type-in-type':
http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=2429
Matt
On Wed, Jun 10, 2009 at 10:01 PM, Ryan Ingram <ryani.s...@gmail.com> wrote:
> > induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x ->
> p (S x)) -> p n
> > induction n z s = caseNat n isZ isS where
> > isZ :: n ~ Z => p n
> > isZ = z
> > isS :: forall x. (n ~ S x, Nat x) => x -> p n
> > isS x = s (induction x z s)
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
