I read a recent Functional Pearl by Hinze and this inspired me to write up an example of projective programming and its motivation in logic/model theory.

The key to understanding the value of abstraction comes from logic and model theory: when you have more axioms, you have fewer models satisfying the axioms and the axioms prove more theorems; conversely, when you have fewer axioms you have more models and fewer theorems. This means that something more abstract can be in some sense simpler.

Let us consider an example in Haskell, viz.

concat :: [[a]] -> [a]

This can we written several ways:

concat :: [[a]] -> [a]
concat [] = []
concat (x:xs) = x ++ concat xs

concat :: [[a]] -> [a]
concat = foldr (++) []

concat :: [[a]] -> [a]
concat = concatMap id

{-# LANGUAGE DeriveFunctor #-}

newtype Fix f = Fix { unFix :: f (Fix f) }

data ListF a b = Cons a b
| Nil
deriving (Functor)

cata :: Functor f => (f a -> a) -> (Fix f -> a)
cata f = g where g = f . fmap g . unFix

fixList :: [a] -> Fix (ListF a)
fixList [] = Fix Nil
fixList (x:xs) = Fix (Cons x (fixList xs))

concat :: [[a]] -> [a]
concat = cata a . fixList
where a Nil = []
a (Cons x xs) = x ++ xs

By contrast,

join :: Monad m => m (m a) -> m a

is expressible only as

join :: Monad m => m (m a) -> m a
join = (>>= id)

Note that `join`

is a generalization of `concat`

.

Despite the fact that `join`

is
more abstract, it is easier to come
up with its implementation: we write the only sensible thing that typechecks.

This is
not the case with our first implementation of `concat`

; we could have easily
written

concat :: [[a]] -> [a]
concat [] = []
concat (x:xs) = concat xs ++ x

# Coda

I believe programming in this style is a place where Haskell and its descendants have an advantage over other mainstream programming languages, notably due to typeclasses. I do not think this is the final word on abstraction by any means, but it does provide a poignant demonstration of the limits of non-functional programming languages.