title: List based on right Kan extension
body: <p>In the ``<a href="http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf" rel="noreferrer">Kan Extensions for Program Optimisation</a>'' 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:</p>
  
  <pre><code>newtype List a = Abstr {
    apply :: forall z . (Monoid z) =&gt; (a -&gt; z) -&gt; z
    } 
  </code></pre>
  
  <p>I was able to define usual nil and cons constructors:</p>
  
  <pre><code>nil :: List a
  nil = Abstr (\f -&gt; mempty)
  
  cons :: a -&gt; List a -&gt; List a
  cons x (Abstr app) = Abstr (\f -&gt; mappend (f x) (app f))
  </code></pre>
  
  <p>With the following instance of Monoid class for Maybe functor, I managed to define head function: </p>
  
  <pre><code>instance Monoid (Maybe a) where
    mempty = Nothing
    mappend Nothing m = m
    mappend (Just a) m = Just a
  
  head :: List a -&gt; Maybe a
  head (Abstr app) = app Just
  </code></pre>
  
  <p><strong>Question</strong>: How can one define tail function?</p>