Mendler-Style Catamorphisms.

Encode.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeSynonymInstances #-}

-- https://www.youtube.com/watch?v=HqvBBf_cjDo
-- https://wiki.haskell.org/Catamorphisms

module Encode where

import Prelude hiding (succ)

data NatF :: * -> * where
    ZeroF :: NatF a
    SuccF :: a -> NatF a

data Fix :: (* -> *) -> * where
    Fix :: { unFix :: f (Fix f) } -> Fix f

type Nat = Fix NatF

zero :: Nat
zero = Fix ZeroF

succ :: Nat -> Nat
succ = Fix . SuccF

instance Show Nat where
    show (Fix ZeroF)     = show 0
    show (Fix (SuccF x)) = show (1 + read (show x))

-- AlgebraM :: (* -> *) -> * -> *
type AlgebraM f a = forall r. (r -> a) -> f r -> a

isEvenAlg :: AlgebraM NatF Bool
isEvenAlg _ ZeroF       = True
isEvenAlg rec (SuccF x) = not (rec x)

cataM :: AlgebraM f a -> Fix f -> a
cataM alg = alg (cataM alg) . unFix

isEven :: Nat -> Bool
isEven = cataM isEvenAlg