[Haskell-cafe] number-parameterized types and heterogeneous lists

[Ryan Ingram]

Literate haskell response:
> {-# LANGUAGE GADTs, RankNTypes #-}
> module Digits where
> {-

On 6/23/08, Luke Palmer <lrpalmer at gmail.com> wrote:

> > I also wonder if there is some kind of "generalized" foldr such that, e.g.
> >      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
> > I think that this foldr must be some "special" foldr that augments the data
> > type of the result in each foldr step.
> > Would this be possible or am I just chasing phantoms ?

> Mostly I believe you are.  What you are describing is firmly in the
> realm of dependent types, far beyond Haskell's type system. See
> Epigram or Agda for languages which have attempted to tackle this
> problem.

> -}

I'm not so sure, as long as you are willing to live with the result
being existentially quantified.  Here's an example:
ghci> mkNat [x1, x0, x3, x2]
(reifyInt 1032)
ghci> :t mkNat [x1, x0, x3, x2]
mkNat [x1, x0, x3, x2] :: AnyNat

I slightly specialize the constructors to wrap them in existential types:
d0 = AnyNat . D0  -- and so on for d1..d9
x0 = NatFn d0 -- and so on for x1..x9


Full code:

> data Sz = Sz
> data D0 a = D0 a
> data D1 a = D1 a
> data D2 a = D2 a
> data D3 a = D3 a
> data D4 a = D4 a
> data D5 a = D5 a
> data D6 a = D6 a
> data D7 a = D7 a
> data D8 a = D8 a
> data D9 a = D9 a

> class Nat n where
>    toIntAccum :: n -> Integer -> Integer

> toInt :: Nat n => n -> Integer
> toInt n = toIntAccum n 0

> instance Nat Sz where toIntAccum _ acc = acc

> instance Nat a => Nat (D0 a) where
>     toIntAccum (D0 n) acc = toIntAccum n (10 * acc + 0)
> instance Nat a => Nat (D1 a) where
>     toIntAccum (D1 n) acc = toIntAccum n (10 * acc + 1)
> instance Nat a => Nat (D2 a) where
>     toIntAccum (D2 n) acc = toIntAccum n (10 * acc + 2)
> instance Nat a => Nat (D3 a) where
>     toIntAccum (D3 n) acc = toIntAccum n (10 * acc + 3)
> instance Nat a => Nat (D4 a) where
>     toIntAccum (D4 n) acc = toIntAccum n (10 * acc + 4)
> instance Nat a => Nat (D5 a) where
>     toIntAccum (D5 n) acc = toIntAccum n (10 * acc + 5)
> instance Nat a => Nat (D6 a) where
>     toIntAccum (D6 n) acc = toIntAccum n (10 * acc + 6)
> instance Nat a => Nat (D7 a) where
>     toIntAccum (D7 n) acc = toIntAccum n (10 * acc + 7)
> instance Nat a => Nat (D8 a) where
>     toIntAccum (D8 n) acc = toIntAccum n (10 * acc + 8)
> instance Nat a => Nat (D9 a) where
>     toIntAccum (D9 n) acc = toIntAccum n (10 * acc + 9)

> data AnyNat where AnyNat :: Nat n => n -> AnyNat

> d0, d1, d2, d3, d4, d5, d6, d7, d8, d9 :: Nat n => n -> AnyNat
> d0 = AnyNat . D0
> d1 = AnyNat . D1
> d2 = AnyNat . D2
> d3 = AnyNat . D3
> d4 = AnyNat . D4
> d5 = AnyNat . D5
> d6 = AnyNat . D6
> d7 = AnyNat . D7
> d8 = AnyNat . D8
> d9 = AnyNat . D9

> reifyDigit :: Integer -> (forall n. Nat n => n -> AnyNat)
> reifyDigit 0 = d0
> reifyDigit 1 = d1
> reifyDigit 2 = d2
> reifyDigit 3 = d3
> reifyDigit 4 = d4
> reifyDigit 5 = d5
> reifyDigit 6 = d6
> reifyDigit 7 = d7
> reifyDigit 8 = d8
> reifyDigit 9 = d9
> reifyDigit _ = error "not a digit"

> reifyIntAccum :: Integer -> AnyNat -> AnyNat
> reifyIntAccum 0 acc          = acc
> reifyIntAccum n (AnyNat rhs) = let (l, r) = divMod n 10 in
>                                reifyIntAccum l (reifyDigit r rhs)

> reifyInt :: Integer -> AnyNat
> reifyInt n | n < 0  = error "negative"
> reifyInt n          = reifyIntAccum n (AnyNat Sz)

> instance Show AnyNat where
>     show (AnyNat n) = "(reifyInt " ++ show (toInt n) ++ ")"

> data NatFn where NatFn :: (forall n. Nat n => n -> AnyNat) -> NatFn

> x0, x1, x2, x3, x4, x5, x6, x7, x8, x9 :: NatFn
> x0 = NatFn d0
> x1 = NatFn d1
> x2 = NatFn d2
> x3 = NatFn d3
> x4 = NatFn d4
> x5 = NatFn d5
> x6 = NatFn d6
> x7 = NatFn d7
> x8 = NatFn d8
> x9 = NatFn d9

> foldNat :: [NatFn] -> AnyNat -> AnyNat
> foldNat []           z = z
> foldNat (NatFn f:xs) z = case foldNat xs z of AnyNat n -> f n

> mkNat :: [NatFn] -> AnyNat
> mkNat xs = foldNat xs (AnyNat Sz)

  -- ryan