It suffices to describe sums, products and their identities to obtain the full wealth of ADTs:
newtype a + b = Sum{ matchSum :: forall r. (a -> r) -> (b -> r) -> r) }
left :: a -> a + b
left x = Sum \l _ -> l x
right :: b -> a + b
right y = Sum \_ r -> r y
newtype Void = Void{ absurd :: forall r. r }
newtype a * b = Product{ matchPair :: forall r. (a -> b -> r) -> r }
pair :: a -> b -> a * b
pair x y = Product \f -> f x y
newtype Unit = Unit (forall r. r -> r)
unit :: Unit
unit = Unit \r -> rRecursion is where it gets a bit more interesting. Luckily, we can factor this consideration out: write a base functor with the above, E.g.
newtype ListF a s = ListF (Unit + a * s)Then transform it with a suitable fixpoint operator.
Using Haskell's direct type-level recursion, we obtain Fix, corresponding to the Scott encoding.
newtype Fix f = In{ out :: f (Fix f) }
type ScottList a
= Fix (ListF a)
-- ~ ListF a (ScottList a)
-- ~ Unit + a * ScottList a
-- ~ forall r. (Unit -> r) -> (a * ScottList a -> r) -> r
-- ~ forall r. r -> (a -> ScottList a -> r) -> rThe resulting "destructor" corresponds to shallow pattern matching.
Somewhat miraculously, absent any actual recursion, we can also define the least fixed-point operator, corresponding to the Church (or Boehm-Berarducci) encoding.
-- AKA Mu
newtype LFP f = LFP{ fold :: forall r. (f r -> r) -> r }
type ChurchList a
= LFP (ListF a)
-- ~ forall r. (ListF a r -> r) -> r
-- ~ forall r. ((Unit + a * r) -> r) -> r
-- ~ forall r. (Unit -> r) -> (a * r -> r) -> r
-- ~ forall r. r -> (a -> r -> r) -> rThe type of the resulting "destructor" might just be familiar.
Indeed, it should be—it corresponds to foldr, or a catamorphism in general.
The fact that foldr (rearranged a little) transforms lists into into this (more fusile) alternative representation is what underpins foldr/build fusion.
There's another (miraculously non-recursive) fixpoint operator, but it's not really used in this context.
-- AKA Nu
data GFP f = forall s. GFP{ grow :: s -> f s, seed :: s }