--------------------
-- 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