[Haskell-cafe] Lightweight type-level dependent programming in Haskell

[Matt Morrow]

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.spam at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090611/0e881229/attachment.html