inline unsigned factorial(unsigned n, unsigned a = 1)
{ return n ? factorial(n - 1, a * n) : a; }

NI>template<int N>
NI>struct factorial
NI>{
NI>    static const int value = N*factorial<N-1>::value;
NI>};

NI>template<>
NI>struct factorial<0>
NI>{
NI>    static const int value = 1;
NI>};

NI>int main()
NI>{
NI>    int array[factorial<6>::value];
NI>}
NI>

const int factorialTable[ ] = {1, 1, 2, 6, 24, 120, 720, 5040, 40320,
        362880, 3628800, 39916800, 479001600};

int main()
{
   int array[ factorialTable[6] ];
}

— explicit type recursion with functors and catamorphisms

newtype Mu f = In (f (Mu f))

unIn (In x) = x

cata phi = phi . fmap (cata phi) . unIn

— base functor and data type for natural numbers,
— using locally-defined «eliminators»

data N c = Z | S c

instance Functor N where
  fmap g  Z    = Z
  fmap g (S x) = S (g x)

type Nat = Mu N

zero = In Z
suck n = In (S n)

add m = cata phi where
  phi  Z    = m
  phi (S f) = suck f

mult m = cata phi where
  phi  Z    = zero
  phi (S f) = add m f

— explicit products and their functorial action

data Prod e c = Pair c e

outl (Pair x y) = x
outr (Pair x y) = y

fork f g x = Pair (f x) (g x)

instance Functor (Prod e) where
  fmap g = fork (g . outl) outr

— comonads, the categorical «opposite» of monads

class Functor n => Comonad n where
  extr :: n a -> a
  dupl :: n a -> n (n a)

instance Comonad (Prod e) where
  extr = outl
  dupl = fork id outr


gcata :: (Functor f, Comonad n) =>
           (forall a. f (n a) -> n (f a))
             -> (f (n c) -> c) -> Mu f -> c

gcata dist phi = extr . cata (fmap phi . dist . fmap dupl)

zygo chi = gcata (fork (fmap outl) (chi . fmap outr))

para :: Functor f => (f (Prod (Mu f) c) -> c) -> Mu f -> c
para = zygo In

fac = para phi where
  phi  Z             = suck zero
  phi (S (Pair f n)) = mult f (suck n)

int = cata phi where
  phi  Z    = 0
  phi (S f) = 1 + f

instance Show (Mu N) where
  show = show . int