自然图推导算法

Question

This Reddit post by Edward Kmett provides a constructive definition of a natural map, the one from the free theorem for fmap (which I read in yet another Edward Kmett's post):

For given f, g, h and k, such that f . g = h . k: $map f . fmap g = fmap h . $map k, where $map is the natural map for the given constructor.

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

We can define a "natural map" by induction over any particular concrete choice of F you give. Ultimately any such ADT is made out of sums, products, (->)'s, 1s, 0s, a's, invocations of other functors, etc.

考虑：

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 应用于每个 x，将 fmap xy 应用于每个 T x，其中 T 是一个 Functor，我们保持每个单元不变，我们将每个 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)

并为non-inductive types:_{(Detailed explanation in this answer下联post.)}

Graph a = Node a [Graph a]

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

这部分说清楚了。

When we allow (->) we now have the first thing that mixes variance up. The left-hand type argument of (->) is in contravariant position, the right-hand side is in covariant position. So you need to track the final type variable through the entire ADT and see if it occurs in positive and/or negative position.

现在我们包括 (->)s。让我们试着让这个归纳继续下去：

我们以某种方式为 T a 和 S a 导出了 自然图 。因此，我们要考虑以下几点：

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

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

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

(Phantom) a occurs neither in T nor in S. a in T2S is phantom, thus, we can implement both fmap and contramap as const phantom.
（协变） a 出现在 S a 中，不出现在 T a 中。因此，ReaderT 行中的某些内容以 S a（实际上并不依赖于 a）作为环境，它将 ?Class? 替换为 Functor，?map? 与 fmap、???、?? 与 xy 与：
```
let tx = phantom ty 
    sx = tx2sx tx
    sy = fmap xy sx
in sy
```
(Contravariant) a 出现在 T a 中，不出现在 S a 中。我没有找到让这个东西成为协变函子的方法，所以我们在这里实现了一个 Contravariant 实例，它将 ?map? 替换为 contramap，将 ?? 替换为 yx, ??? 与：
```
let tx = fmap yx ty 
    sx = tx2sx tx
    sy = phantom sx 
in sy
```
(Invariant) a occurs both in T a and S a. We can no longer use phantom, which came in quite handy. There is a module Data.Functor.Invariant 作者：爱德华·克梅特。它为以下 class 提供了一张地图：
```
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 情况？

Answer 1

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

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

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

很好，但这也是我们第一次遇到不确定性。使它成为仿函数的一种方法确实是嵌套 fmaps；但另一种方式是嵌套 contramaps.

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

如果两个子句都是可能的，那么 F 或 F' 中都没有 Id，因此两个实例都将 return x 不变.

现在只剩下箭盒了，就是你问的那个。但事实证明在这种形式主义中非常容易，只有一个选择：

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

这就是定义自然 fmap 的完整算法的全部细节。 ...除了一个细节，这是自然 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) 是唯一实际使用其第一个函数参数的叶子案例。）

自然图推导算法

Natural map derivation algorithm

haskell

covariance

contravariance

functor

denotational-semantics