Literate haskell response:

{-# LANGUAGE GADTs, RankNTypes #-} module Digits where {-

On 6/23/08, Luke Palmer 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