--------------------
-- Factorial encoded in the structure of a nested datatype
-- Fritz Ruehr, Willamette University, August 2001

-- Natural numbers encoded at the level of types
-- (punning the list constructor names)

data Zero   a = Nil
data Succ n a = Cons a (n a)

zero        a = Nil
suck      n a = Cons a (n a)


-- A higher-order, nested datatype encoding factorial structure,
-- and a function which builds canonical (infinite) values

data Facs n a = Fac a (Facs (Succ n) (Succ n a))

facs :: (forall a. a -> n a) -> a -> Facs n a
facs      n a = Fac a (facs (suck n) (suck n a))


-- Instances and classes to lift map and fold to Zero/Succ types

instance Functor Zero where
  fmap f Nil = Nil

instance Functor n => Functor (Succ n) where
  fmap f (Cons x y) = Cons (f x) (fmap f y)

class Folding n where
  fold :: (a -> b -> b) -> b -> n a -> b

instance Folding Zero where
  fold c n Nil = n

instance Folding n => Folding (Succ n) where
  fold c n (Cons x y) = c x (fold c n y)


-- A function to count the "sizes" of successive elements in a Facs
-- and an application to a particular instance (of units) of Facs type

next f = fold (+) 0 . fmap f

count :: (Functor n, Folding n) => (a -> Integer) -> Facs n a -> [Integer]
count f (Fac a m) = f a : count (next f) m

sizes :: Facs Zero a -> [Integer]
sizes = count (const 1)


-- The size of an element in the Facs structure is the factorial of its index

fac n = sizes (facs zero ()) !! n