Ed Kmett的递归方案包中的Fix，Mu和Nu有什么区别

问题描述

在Ed Kmett的recursion-scheme包中，有三个声明:

In Ed Kmett's recursion-scheme package, there are three declarations:

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

data Nu f where
  Nu :: (a -> f a) -> a -> Nu f

这三种数据类型有什么区别?

What is the difference between those three data types?

推荐答案

Mu表示递归类型为折叠，而Nu表示它为展开.在Haskell中，这些是同构的，并且是表示同一类型的不同方法.如果您假装Haskell没有任意递归，则这些类型之间的区别会变得更加有趣:Mu f是f的最小(初始)固定点，而Nu f是其最大的(终端)固定点.

Mu represents a recursive type as its fold, and Nu represents it as its unfold. In Haskell, these are isomorphic, and are different ways to represent the same type. If you pretend that Haskell doesn't have arbitrary recursion, the distinction between these types becomes more interesting: Mu f is the least (initial) fixed point of f, and Nu f is its greatest (terminal) fixed point.

f的不动点是T类型，在T和f T之间同构，即一对反函数in :: f T -> T，out :: T -> f T.类型Fix仅使用Haskell的内置类型递归直接声明同构.但是您可以同时为Mu和Nu实施输入/输出.

A fixed point of f is a type T an isomorphism between T and f T, i.e. a pair of inverse functions in :: f T -> T, out :: T -> f T. The type Fix just uses Haskell's built-in type recursion to declare the isomorphism directly. But you can implement in/out for both Mu and Nu.

举一个具体的例子，假装你不能写递归值. Mu Maybe的居民(即值:: forall r. (Maybe r -> r) -> r)是自然数{0，1，2，...}; Nu Maybe的居民(即值:: exists x. (x, x -> Maybe x))是自然变量{0，1，2，...，∞}.考虑一下这些类型的可能值，以了解为什么Nu Maybe有更多居民.

For a concrete example, pretend for a moment that you can't write recursive values. The inhabitants of Mu Maybe , i.e. values :: forall r. (Maybe r -> r) -> r, are the naturals, {0, 1, 2, ...}; the inhabitants of Nu Maybe, i.e. values :: exists x. (x, x -> Maybe x), are the conaturals {0, 1, 2, ..., ∞}. Think about the possible values of these types to see why Nu Maybe has an extra inhabitant.

如果您想对这些类型有一些直觉，可以很有趣地实现以下内容而无需递归(大致按难度递增的顺序):

If you want to get some intuition for these types, it can be a fun exercise to implement the following without recursion (roughly in increasing order of difficulty):

• zeroMu :: Mu Maybe，succMu :: Mu Maybe -> Mu Maybe
• zeroNu :: Nu Maybe，succNu :: Nu Maybe -> Nu Maybe，inftyNu :: Nu Maybe
• muTofix :: Mu f -> Fix f，fixToNu :: Fix f -> Nu f
• inMu :: f (Mu f) -> Mu f，outMu :: Mu f -> f (Mu f)
• inNu :: f (Nu f) -> Nu f，outNu :: Nu f -> f (Nu f)

• zeroMu :: Mu Maybe, succMu :: Mu Maybe -> Mu Maybe
• zeroNu :: Nu Maybe, succNu :: Nu Maybe -> Nu Maybe, inftyNu :: Nu Maybe
• muTofix :: Mu f -> Fix f, fixToNu :: Fix f -> Nu f
• inMu :: f (Mu f) -> Mu f, outMu :: Mu f -> f (Mu f)
• inNu :: f (Nu f) -> Nu f, outNu :: Nu f -> f (Nu f)

您也可以尝试实现这些，但是它们需要递归:

You can also try to implement these, but they require recursion:

• nuToFix :: Nu f -> Fix f，fixToMu :: Fix f -> Mu f

Mu f是最小固定点，而Nu f是最大固定点，因此编写函数:: Mu f -> Nu f非常容易，但是编写函数:: Nu f -> Mu f却很困难；就像逆流而上.

Mu f is the least fixed point, and Nu f is the greatest, so writing a function :: Mu f -> Nu f is very easy, but writing a function :: Nu f -> Mu f is hard; it's like swimming against the current.

(在某种意义上，我本来打算对这些类型进行更详细的说明，但是对于这种格式来说可能太长了.)

(At one point I was meaning to write a more detailed explanation of these types, but it might be a little too long for this format.)

这篇关于Ed Kmett的递归方案包中的Fix，Mu和Nu有什么区别的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！