Algebra/Coalgebra

Algebra

If you have an arbitrary covariant Functor, T a you can consider the class of functions

alg :: T X -> X

for some specific type X called the carrier. The choice of carrier and the function alg together are called an algebra and are a recipe for creating Xes. For instance, the functor

data T x = T (Either () x)

has an algebra

alg :: T [()] -> [()]
alg (T (Left ()))  = []
alg (T (Right ls)) = () : ls

which demonstrates how to recursively create a list of units. Or it has the algebra

alg :: T Int -> Int
alg (T (Left ())) = 0
alg (T (Right n)) = succ n

which demonstrates how to create natural numbers, or lenths of the lists before. It also has the algebra

data Fix f = In { out :: f (Fix f) }

alg :: T (Fix T) -> Fix T
alg = In    

which shows that we can construct fixed points of T from the functor T itself in a very compact way.

The upshot is that a functor like T provides a signature of functions in a universal algebra to construct elements of the carrier type.

Coalgebra

If you have an arbitrary covariant Functor, T a you can consider the class of functions

coalg :: X -> T X

for some specific type X called the carrier. The choice of carrier and the function coalg together are called a coalgebra and are a recipe for observing Xes. For instance, the functor

data T x = T (Either () x)

has a coalgebra

coalg :: [()] -> T [()]
coalg []     = T (Left ())
coalg (x:xs) = T (Right xs)

which demonstrates how to check a list of units to see if it is empty. Or it has the coalgebra

coalg :: Int -> T Int
coalg 0 = T (Left ())
coalg n = T (Right (pred n))

which demonstrates how to count down the natural numbers, or the lengths of the lists before. It also has the coalgebra

data Fix f = In { out :: f (Fix f) }

coalg :: Fix T -> T (Fix T)
coalg = out

which shows that we can observe fixed points of T via the functor T itself in a very compact way.

Construction/Observation

Functors in normal forms

Clearly, these concepts are duals and both arise from the nature of Functors of some kind.

We can write functors in an algebraic form inherited from the algebraic form of ADTs. For instance, T from above

data T x = T (Either () x)

is compactly written as

T X = 1 + X

and

data T x = T ((), x)

is compactly written as

T X = 1 * X

since Either is a canonical sum type, (,) a canonical product type, and () a unit. If we are dealing with nice, distributive functors where we have

A + (B * C) <-> (A + B) * (A + C)

then we can always write them in disjunctive normal form

T X = T1 X + T2 X + T3 X + T4 X + ...

where the Tn subfunctors are each sum-free or conjunctive normal form

T X = T1 X * T2 X * T3 X * T4 X * ...

where the subfunctors are each product-free. These simplified forms tell us a lot about what alg or coalg must be doing.

Construction/Observation

Consider alg. For disjunctive normal form its first step must be to branch on one of many sub algebras corresponding to the particular branch in the sum.

-- pseudo-Haskell
alg tx = case tx of
  t1@T1{} -> alg_1 t1
  t2@T2{} -> alg_2 t2
  ...

while ach of the alg_ns are no longer able to be conditional of the structure of their arguments, they must create a new carrier object with only the information from the chosen branch.

alg_1 (T1 a b c d) = ...

If we give them names then we might think of them as the various recursive construction functions for the carrier T. Specifically, we can think of the list constructors nil :: [a] and cons :: a -> [a] -> [a] as two subalgebras on the disjunctive normal form functor

data T a x = 1 + (a, x)

alg :: T a [a] -> [a]
alg ()      = nil
alg (a, as) = cons a as

Consider coalg. For conjunctive normal form its first step must be to distribute its work to many sub coalgebras

-- psuedo-Haskell
coalg t = (coalg_1 t, coalg_2 t, coalg_3 t)

each of which returning a component of the an observation from the carrier, though they may choose to return useless information like (). Specifically, we can think of the stream observers head :: Stream a -> a and tail :: Stream a -> Stream as two subcoalgebras on the conjuctive normal form functor

{- data Stream a = Cons a (Stream a) -}

data T a x = (a, x)

coalg :: Stream a -> T a (Stream a)
coalg s = (head s, tail s)