自然图推导算法 [英] Natural map derivation algorithm

问题描述

爱德华·克梅特(Edward Kmett)的这篇Reddit帖子提供了一个建设性的定义自然图，是 fmap 的定理中的一个(我在另一个

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

对于给定的 f ， g ， h 和 k ，例如 f.g = h.k : $ map f.fmap g = fmap h.$ map k ，其中 $ map 是给定构造函数的自然映射.

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.

我不完全了解该算法.让我们逐步解决它:

I do not fully understand the algorithm. Let us approach it step-by-step:

我们可以通过对您给出的 F 的任何具体选择进行归纳来定义自然图" .最终，任何此类ADT都是由总和，乘积，(->)， 1 s， 0 s，一个的，其他的调用函子等.

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 (我认为其中不带(->)的任何ADT的自然选择)将如何操作在这里:

No arrows. Let us see how fmap (which I reckon to be the natural choice for any ADT without (->)s in it) would operate here:

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 传递到荒谬上.这也适用于递归定义！

Which seems natural. To put this more formally, we apply xy to every x, apply fmap xy to every T x, where T is a Functor, we leave every unit unchanged, and we pass every Void onto absurd. This works for recursive definitions too!

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)

对于 非归纳类型:_{(链接文章下方的此答案中的详细说明.)}

And for the non-inductive types:_{(Detailed explanation in this answer under the linked post.)}

Graph a = Node a [Graph a]

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

这部分很清楚.

当我们允许(->)时，我们第一件事就是将方差混合在一起.(->)的左侧类型参数处于协变位置，右侧处于协变位置.因此，您需要在整个ADT中跟踪最终类型变量，并查看它是否出现在正位置和/或负位置.

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.

现在，我们包含(->).让我们尝试使这种归纳继续进行:

Now we include (->)s. Let us try to keep this induction going:

我们以某种方式为 T a 和 S a 导出了自然图.因此，我们要考虑以下因素:

We somehow derived natural maps for T a and S a. Thus, we want to consider the following:

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

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

我相信这是我们开始选择的重点.我们提供以下选项:

And I believe this to be the point where we start choosing. We have the following options:

• (幻影) a 既不会出现在 T 中，也不会出现在 S 中.T2S 中的 a 是幻像，因此，我们可以将 fmap 和 contramap 都实现为

• (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.
• (Covariant) a occurs in S a and does not occur in T a. Thus, this something among the lines of ReaderT with S a (which does not actually depend on a) as environment, which substitutes ?Class? with Functor, ?map? with fmap, ???, ?? with xy with:

let tx = phantom ty 
    sx = tx2sx tx
    sy = fmap xy sx
in sy

(相反) a 出现在 T a 中，而不发生在 S a 中.我没有看到一种使该函数成为协变函子的方法，因此我们在这里实现了一个 Contravariant 实例，该实例用 contramap 替换了?map?， ?? 与 yx ， ??? 与:

(Contravariant) a occurs in T a and does not occur in S a. I do not see a way to make this thing a covariant functor, so we implement a Contravariant instance here, which substitutes ?map? with contramap, ?? with yx, ??? with:

let tx = fmap yx ty 
    sx = tx2sx tx
    sy = phantom sx 
in sy

(不变) a 出现在 T a 和 S a 中.我们再也不能使用 phantom 了，它非常方便.有一个模块 Data.Functor.Invariant ，由Edward Kmett撰写.它为下面的类提供了一个映射:

(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 by Edward Kmett. It provides the following class with a map:

class Invariant f where
  invmap :: (a -> b) -> (b -> a) -> f a -> f b
  -- and some generic stuff...

但是，我看不到有什么方法可以将其转化为fmap的自由定理的类型-该类型需要附加的函数参数，因此我们无法将其刷除为id 之类的.无论如何，我们用 invmap 代替?map?，用 xy yx 代替 ?? ，然后用以下代码代替的 ??? :

And yet, I cannot see a way to turn this into something we can pluf into the free theorem for fmap - the type requires an additional function-argument, which we can't brush off as id or something. Anyway, we put invmap instead of ?map?, xy yx instead of ??, and the following instead of ???:

let tx = fmap yx ty 
    sx = tx2sx tx
    sy = fmap xy sx
in sy

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

So, is my understanding of such an algorithm correct? If so, how are we to properly process the Invariant case?

推荐答案

我认为您的算法太复杂了，因为您正在尝试编写一个算法.写两个算法反而使事情变得简单得多.一种算法将构建自然的fmap，另一种算法将构建自然的conmap.但是在以下意义上，两种算法都必须是不确定的:在某些类型中它们无法成功执行，因此不返回实现；在某些类型中，它们可以通过多种方式取得成功，但它们都是等效的.

I think your algorithm is too complex, because you are trying to write one algorithm. Writing two algorithms instead makes things much simpler. One algorithm will build the natural fmap, and the other will build the natural contramap. BUT both algorithms need to be nondeterministic in the following sense: there will be types where they cannot succeed, and so do not return an implementation; and there will be types where there are multiple ways they can succeed, but they're all equivalent.

首先，让我们仔细定义成为参数化类型的含义.这是我们可以使用的各种类型的参数化类型:

To start, let's carefully define what it means to be a parameterized type. Here's the different kinds of parameterized types we can have:

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

在 Const X 中， X 覆盖所有具体的非参数类型，例如 Int 和 Bool 等等.这是它们的解释，即，一旦指定了参数，它们便是同构的具体类型:

In Const X, the X ranges over all concrete, non-parameterized types, like Int and Bool and so forth. And here's their interpretation, i.e. the concrete type they are isomorphic to once given a parameter:

[[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

现在，我们可以给出两种算法.您已经写好自己的第一句话:

Now we can give our two algorithms. The first bit you've already written yourself:

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] 示例中，您提供了与此相对应的子句:

These correspond to the clauses you gave in your first instance. Then, in your [Graph a] example, you gave a clause corresponding to this:

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

很好，但这也是我们获得不确定性的第一刻.使它成为函子的一种方法的确是嵌套的 fmap s.但另一种方法是嵌套 contramap s.

That's fine, but this is also the first moment where we get some nondeterminism. One way to make this a functor is indeed nested fmaps; but another way is nested contramaps.

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

如果两个子句均可行，则 F 或 F'中都没有 Id ，因此两个实例都将返回 x 不变.

If both clauses are possible, then there are no Ids in either F or F', so both instances will return x unchanged.

现在剩下的唯一一个是箭头盒，您要问的那个.但是事实证明，在这种形式主义中非常容易，只有一种选择:

The only thing left now is the arrow case, the one you ask about. But it turns out it's very easy in this formalism, there is only one choice:

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

这是用于定义自然的 fmap 的整个算法的详细信息....一个细节除外，这是自然 contramap 的算法.但是希望您遵循了以上所有内容，就可以自己重现该算法.我鼓励您试一试，然后根据下面的内容检查您的答案.

That's the whole algorithm, in full detail, for defining the natural fmap. ...except one detail, which is the algorithm for the natural contramap. But hopefully if you followed all of the above, you can reproduce that algorithm yourself. I encourage you to give it a shot, then check your answers against mine below.

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)是唯一使用其第一个函数参数的唯一叶子情况.)

One thing of interest to me personally: it turns out that contramap @(Id) is the only leaf case that fails. All further failures are inductive failures ultimately deriving from this one -- a fact I had never thought of before! (The dual statement is that it turns out that fmap @(Id) is the only leaf case that actually uses its first function argument.)

这篇关于自然图推导算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！