haskell - 自然地图推导算法

Question

Edward Kmett 的这篇 Reddit 帖子提供了自然地图的建设性定义，它来自自由定理（fmap我在另一篇Edward Kmett 的帖子中读到）：

对于给定f的 ,和g,这样: , 其中是给定构造函数的自然映射。hkf . g = h . k$map f . fmap g = fmap h . $map k$map

我不完全理解算法。让我们一步一步地接近它：

我们可以通过对您给出的任何特定具体选择的归纳来定义“自然地图” 。F最终，任何这样的 ADT 都是由 sum、products、(->)'s、1s、0s、a's、其他仿函数的调用等组成的。

考虑：

data Smth a = A a a a | B a (Maybe a) | U | Z Void deriving ...

没有箭头。让我们看看fmap（我认为这是任何没有 s 的 ADT 的自然选择(->)）在这里如何操作：

instance Functor Smth where
  fmap xy (A x x1 x2)  = A (xy x) (xy x1) (xy x2)
  fmap xy (B x xPlus1) = B (xy x) (fmap xy xPlus1) 
  -- One can pattern-match 'xPlus1' as 'Just x1' and 'Nothing'.
  -- From my point of view, 'fmap' suits better here. Reasons below.
  fmap _xy U     = U 
  fmap _xy (Z z) = absurd z

这看起来很自然。更正式地说，我们适用xy于 every x，适用fmap xy于 every T x，其中Ta Functor，我们保持每个单元不变，然后将 every 传递Void给absurd。这也适用于递归定义！

data Lst a = Unit | Prepend a (Lst a) deriving ...

instance Functor Lst where
    fmap xy Unit             = Unit
    fmap xy (Prepend x lstX) = Prepend (xy x) (fmap xy lstX)

对于非归纳类型：（_{链接帖子下}_此答案_{的详细说明。）}

Graph a = Node a [Graph a]

instance Functor Graph where
    fmap xy (Node x children) = Node (xy x) (fmap (fmap xy) children)

这部分很清楚。

当我们允许时，(->)我们现在有了第一个混合方差的东西。的左侧类型参数(->)处于逆变位置，右侧处于协变位置。因此，您需要通过整个 ADT 跟踪最终类型变量，并查看它是否出现在正和/或负位置。

现在我们包括(->)s。让我们尝试继续进行这种归纳：

我们以某种方式推导出和的自然映射。因此，我们要考虑以下几点：T aS a

data T2S a = T2S (T a -> S a)

instance ?Class? T2S where
    ?map? ?? (T2S tx2sx) = T2S $ \ ty -> ???

我相信这是我们开始选择的起点。我们有以下选择：

（幻影） a既不在T也不在S。ainT2S是幻像，因此，我们可以同时实现fmap和contramapasconst phantom。
（协变） a出现在S a和不出现在中T a。因此，这在ReaderTwith S a（实际上并不依赖于a）作为环境的行中，它?Class?用Functor、?map?with fmap、???、??with代替xy：
```
let tx = phantom ty 
    sx = tx2sx tx
    sy = fmap xy sx
in sy
```
（逆变） a出现在T a，不出S a。我看不到让这个东西成为协变函子的方法，所以我们Contravariant在这里实现一个实例，它?map?用contramap、??withyx、???with 代替：
```
let tx = fmap yx ty 
    sx = tx2sx tx
    sy = phantom sx 
in sy
```
（不变量） a同时出现在T a和S a。我们不能再使用phantom，它派上用场了。Edward Kmett有一个模块Data.Functor.Invariant。它为以下类提供了一个地图：
```
class Invariant f where
  invmap :: (a -> b) -> (b -> a) -> f a -> f b
  -- and some generic stuff...
```
然而，我看不出有什么方法可以把它变成我们可以加入 fmap 的自由定理id的东西——这种类型需要一个额外的函数参数，我们不能把它当作什么东西刷掉。无论如何，我们将invmap代替?map?,xy yx代替??, 并将以下内容代替???:
```
let tx = fmap yx ty 
    sx = tx2sx tx
    sy = fmap xy sx
in sy
```

那么，我对这种算法的理解正确吗？如果是这样，我们如何正确处理Invariant情况？

score 2 · Accepted Answer

我认为您的算法太复杂了，因为您正在尝试编写一种算法。相反，编写两种算法会使事情变得简单得多。一种算法将构建自然 fmap，另一种算法将构建自然 contramap。但是两种算法都需要在以下意义上是不确定的：会有一些类型无法成功，因此不返回实现；并且会有一些类型可以通过多种方式取得成功，但它们都是等价的。

首先，让我们仔细定义参数化类型的含义。以下是我们可以拥有的不同类型的参数化类型：

F ::= F + F'
    | F * F'
    | F -> F'
    | F . F'
    | Id
    | Const X

在Const X中，X范围涵盖所有具体的、非参数化类型，例如Int等等Bool。这是他们的解释，即一旦给定参数，它们就同构的具体类型：

[[F + F']] a = Either ([[F]] a) ([[F']] a)
[[F * F']] a = ([[F]] a, [[F']] a)
[[F -> F']] a = [[F]] a -> [[F']] a
[[F . F']] a = [[F]] ([[F']] a)
[[Id]] a = a
[[Const X]] a = X

现在我们可以给出我们的两种算法。您已经自己编写的第一部分：

fmap @(F + F') f (Left x) = Left (fmap @F f x)
fmap @(F + F') f (Right x) = Right (fmap @F' f x)
fmap @(F * F') f (x, y) = (fmap @F f x, fmap @F f y)
fmap @(Id) f x = f x
fmap @(Const X) f x = x

这些与您在第一个实例中给出的条款相对应。然后，在您的[Graph a]示例中，您给出了一个与此相对应的子句：

fmap @(F . F') f x = fmap @F (fmap @F' f) x

这很好，但这也是我们第一次得到一些不确定性。使它成为函子的一种方法确实是嵌套fmap的；但另一种方式是嵌套contramaps。

fmap @(F . F') f x = contramap @F (contramap @F' f) x

如果两个子句都是可能的，那么or中都没有Ids ，因此两个实例都将返回不变。FF'x

现在唯一剩下的是箭头盒，你问的那个。但事实证明，这种形式很容易，只有一种选择：

fmap @(F -> F') f x = fmap @F' f . x . contramap @F f

这就是定义 natural 的完整算法fmap。...除了一个细节，这是 natural 的算法contramap。但希望如果您遵循上述所有内容，您可以自己重现该算法。我鼓励你试一试，然后在下面对照我的答案检查你的答案。

contramap @(F + F') f (Left x) = Left (contramap @F f x)
contramap @(F + F') f (Right x) = Right (contramap @F' f x)
contramap @(F * F') f (x, y) = (contramap @F f x, contramap @F' f y)
contramap @(F -> F') f x = contramap @F' f . x . fmap @F f

contramap @(F . F') f x = contramap @F (fmap @F' f) x
-- OR
contramap @(F . F') f x = fmap @F (contramap @F' f) x

-- contramap @(Id) fails
contramap @(Const X) f x = x

我个人感兴趣的一件事：事实证明，这contramap @(Id)是唯一失败的叶子案例。所有进一步的失败都是最终源自此失败的归纳失败——这是我以前从未想过的事实！（双重陈述是事实证明这fmap @(Id)是唯一实际使用其第一个函数参数的叶子案例。）

haskell - 自然地图推导算法

1 回答 1

Related

Reference