如何解决自然地图推导算法
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。它为以下类提供了地图：
然而，我看不出有什么方法可以将其转化为我们可以将其推入 fmap 的自由定理——该类型需要一个额外的函数参数，我们不能将其视为 {{1 }} 或者其他的东西。不管怎样，我们用phantomclass 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) 是唯一实际使用其第一个函数参数的叶案例。）
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
