基于正确的Kan扩展名列表 [英] List based on right Kan extension

问题描述

在 Kan扩展程序优化中'通过Ralf Hinze有一个List类型的定义，该类型是基于monoid类别中健忘函数的正确Kan扩展（7.4节）。本文给出了Haskell的实现，如下所示：

  newtype List a = Abstr {
 apply :: forall z。 （Monoid z）=> （a  - > z） - > z 
} 
  

我可以定义通常的nil和cons构造函数：

  nil ::列出
 nil = Abstr（\f  - > mempty）
 
 cons :: a  - >列表a  - >列出
 cons x（Abstr app）= Abstr（\ f  - > mappend（fx）（app f））
  

对于Maybe函数，使用下面的Monoid类实例，我设法定义了头函数：

 实例Monoid（也许a）其中
 mempty = Nothing 
 mappend没有m = m 
 mappend（只是一个）m =只是一个
 
头::列表a - >也许一个
头（Abstr app）= app只需
  

问题：如何定义tail函数？

解决方案

这是一个相当有原则的解决方案，首先，我们知道如何去做一些事情，我们知道如何做到这一点。追加列表（稍后有用）：

  append :: List a  - >列表a  - >列出一个
 append（Abstr xs）（Abstr ys）= Abstr（\ f  - > xs f> ys f）
  

然后我们引入一个新类型 Split ，我们将用它来检测 List


  c $ c>是空的或不是空的（并且在非空的情况下获得头部和尾部）：
 newtype Split a = Split {outSplit :: Maybe（a，List a）} 
  

一个monoid：实际上我们知道如何追加两个列表。

  instance Monoid（Split a）其中
 mempty = Split没有任何
 mappend（Split Nothing）（Split nns）= Split nns 
 mappend（Split mms）（Split Nothing）= Split mms 
 mappend（Just（m，ms）））（ Split（Just（n，ns）））= 
 Split $ Just（m，append ms（cons n ns））
  

这意味着我们可以从列出一个到使用拆分 code>列出一个的 apply code>：

  split :: List a  - >拆分
 split xs = apply xs $ \ a  - > Split $ Just（a，nil）
  

头和 tail 最终可以从 split ：



  head :: List a  - >也许
 head = fmap fst。 outSplit。 split 
 
 tail ::列表a  - >也许（列表a）
 tail = fmap snd。 outSplit。拆分
  




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):

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

这篇关于基于正确的Kan扩展名列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！