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?
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):
Then we introduce a new type
Split
which we will use to detect whether aList
is empty or not (and get, in the case it's non empty, a head and a tail):This new type forms a monoid: indeed we know how to append two lists.
Which means that we can get a function from
List a
toSplit a
usingList a
'sapply
:head
andtail
can finally be trivially derived fromsplit
: