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.