自然地图推导算法

编程问答 2022-05-09

问题描述

This Reddit post by Edward Kmett 提供了自然地图的建设性定义，该定义来自fmap的自由定理（我在另一个Edward Kmett's post)：

对于给定的f、g、h和k，使得f . g = h . k：$map f . fmap g = fmap h . $map k，其中$map是给定构造函数的自然映射。

我不完全理解算法。让我们一步一步来：

我们可以通过归纳您给出的任何具体的 F 选择来定义“自然地图”。 最终，任何此类 ADT 都是由总和、乘积、(->)、1、0、a、其他 函子等

考虑：

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

没有箭头。让我们看看 fmap（我认为它是任何不含 (->) 的 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：（链接帖子下的this answer中有详细说明。）

Graph a = Node a [Graph a]

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

这部分很清楚。

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

现在我们包含 (->)。让我们尽量保持这种归纳：

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

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

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

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

  • (Phantom) a 既不出现在 T 中，也不出现在 S 中。 a 中的 T2S 是幻像，因此，我们可以将 fmap 和 contramap 实现为 const phantom。
  • (Covariant) a 出现在 S a 中，而不出现在 T a 中。因此，这在 ReaderT 行中，以 S a（实际上并不依赖于 a）作为环境，将 ?Class? 替换为 Functor，{ {1}} 与 ?map?、fmap、??? 与 ?? 与： 
    xy
  • (Contravariant) let tx = phantom ty sx = tx2sx tx sy = fmap xy sx in sy 出现在 a 中，不出现在 T a 中。我看不出有办法让这个东西成为协变函子，所以我们在这里实现了一个 S a 实例，它用 Contravariant 代替 ?map?，用 contramap 代替 ?? },yx 与： 
    ???
  • (Invariant) let tx = fmap yx ty sx = tx2sx tx sy = phantom sx in sy 出现在 a 和 T a 中。我们不能再使用 S a，它非常方便。 Edward Kmett 有一个模块 Data.Functor.Invariant。它为以下类提供了地图： 
    phantom
    然而，我看不出有什么方法可以将其转化为我们可以将其推入 fmap 的自由定理——该类型需要一个额外的函数参数，我们不能将其视为 {{1 }} 或者其他的东西。不管怎样，我们用 class Invariant f where invmap :: (a -> b) -> (b -> a) -> f a -> f b -- and some generic stuff... 代替 id，用 invmap 代替 ?map?，用下面的代替 xy yx： 
    ??

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

解决方法

我认为您的算法太复杂了，因为您正在尝试编写一个算法。相反，编写两个算法会使事情变得简单得多。一种算法将构建自然 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

那很好，但这也是我们第一次遇到不确定性。使其成为函子的一种方法确实是嵌套 fmaps;但另一种方式是嵌套 contramaps。

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

如果两个子句都可能，那么 Id 或 F 中都没有 F'，因此两个实例都将返回 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) 是唯一实际使用其第一个函数参数的叶案例。）

contravariancecovariancedenotational-semanticsfunctorhaskellhaskell