List based on right Kan extension

Question

In the ``Kan Extensions for Program Optimisation'' by Ralf Hinze there is the definition of List type based on right Kan extension of the forgetful functor from the category of monoids along itself (section 7.4). The paper gives Haskell implementation as follows:

newtype List a = Abstr {
  apply :: forall z . (Monoid z) => (a -> z) -> z
  } 

I was able to define usual nil and cons constructors:

nil :: List a
nil = Abstr (\f -> mempty)

cons :: a -> List a -> List a
cons x (Abstr app) = Abstr (\f -> mappend (f x) (app f))

With the following instance of Monoid class for Maybe functor, I managed to define head function:

instance Monoid (Maybe a) where
  mempty = Nothing
  mappend Nothing m = m
  mappend (Just a) m = Just a

head :: List a -> Maybe a
head (Abstr app) = app Just

Question: How can one define tail function?

Answer 1

Here is a rather principled solution to implementing head and tail in one go (full gist):

First of all, we know how to append lists (it will be useful later on):

append :: List a -> List a -> List a
append (Abstr xs) (Abstr ys) = Abstr (\ f -> xs f <> ys f)

Then we introduce a new type Split which we will use to detect whether a List is empty or not (and get, in the case it's non empty, a head and a tail):

newtype Split a = Split { outSplit :: Maybe (a, List a) }

This new type forms a monoid: indeed we know how to append two lists.

instance Monoid (Split a) where
  mempty = Split Nothing
  mappend (Split Nothing)        (Split nns)            = Split nns
  mappend (Split mms)            (Split Nothing)        = Split mms
  mappend (Split (Just (m, ms))) (Split (Just (n, ns))) =
    Split $ Just (m, append ms (cons n ns))

Which means that we can get a function from List a to Split a using List a's apply:

split :: List a -> Split a
split xs = apply xs $ \ a -> Split $ Just (a, nil)

head and tail can finally be trivially derived from split:

head :: List a -> Maybe a
head = fmap fst . outSplit . split

tail :: List a -> Maybe (List a)
tail = fmap snd . outSplit . split

Answer 2

This implementation of lists as free monoids is provided in the package fmlist, which notes some interesting properties of it (unlike most implementations of lists, which are right-biased, this one is truly unbiased; you can make an arbitrary tree, and although of course the monoid laws force you to see it as flattened, you can still observe some differences in the infinite case. This is almost a Haskell quirk -- usually, free monoids). It also has an implementation of tail, so that's sort of an answer to your question (but see below).

With these sorts of representations (not just this particular one one, but also e.g. forall r. (a -> r -> r) -> r -> r lists), there are usually some operations (e.g. appending) that become easier, and some (e.g. zip and tail) that become more difficult. This is discussed a bit in various places, e.g. How to take the tail of a functional stream.

Looking more closely at fmlist, though, its solution is pretty unsatisfactory: It just converts the nice balanced tree that you give it to a right-biased list using foldr, which allows it to do regular list operations, but loses the monoidal structure. The tail of a "middle-infinite" list is no longer "middle-infinite", it's just right-infinite like a regular list.

It should be possible to come up with a clever Monoid instance to compute the tail while disturbing the rest of the structure as little as possible, but an obvious one doesn't come to mind off-hand. I can think of a non-clever "brute force" solution, though: Cheat and reify the "list" into a tree using an invalid Monoid instance, inspect the tree, and then fold it back up so the end result is valid. Here's what it would look like with my nonfree package and fmlist:

nail :: FM.FMList a -> FM.FMList a
nail (FM.FM k) = FM.FM $ \f -> foldMap f (nail' (k N))

nail' :: N a -> N a
nail' NEmpty = error "nail' NEmpty"
nail' (N x) = NEmpty
nail' (NAppend l r) =
  case normalize l of
    NEmpty -> nail' r
    N x -> r
    l' -> NAppend (nail' l') r

-- Normalize a tree so that the left side of a root NAppend isn't an empty
-- subtree of any shape. If the tree is infinite in a particular way, this
-- won't terminate, so in that sense taking the tail of a list can make it
-- slightly worse (but you were already in pretty bad shape as far as
-- operations on the left side are concerned, and this is a pathological case
-- anyway).
normalize :: N a -> N a
normalize (NAppend l r) =
  case normalize l of
    NEmpty -> normalize r
    l' -> NAppend l' r
normalize n = n