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

Question

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

haskellrecursive-datastructuresrecursion-schemesfixpoint-combinators

31

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

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

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

- hgiesel

2

我不太了解理论，但我了解对于更加证明性的语言，“Mu”是最小不动点，“Nu”是最大不动点。在Haskell中，这三个都应该是等价的（我相信）。请注意，对于“Mu”，实现“cata”非常容易，而对于“Nu”，实现“ana”也非常容易。 - dfeuer

4

尝试解决这个 kata https://www.codewars.com/kata/folding-through-a-fixed-point/haskell - xgrommx

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- shachaf · Accepted Answer

Mu 以其折叠形式表示递归类型，Nu 以其展开形式表示递归类型。在 Haskell 中，它们是同构的，并且是表示相同类型的不同方式。如果假装 Haskell 没有任意递归，这些类型之间的区别就变得更加有趣: Mu f 是 f 的最小（初始）不动点，而 Nu f 是其最大（终极）不动点。

f 的不动点是一种类型 T，其中包含 T 和 f T 之间的同构，即反函数对 in :: f T -> T、out :: T -> f T。类型 Fix 只是使用 Haskell 的内置类型递归来直接声明同构。但你可以为 Mu 和 Nu 实现 in/out。

举个具体的例子，假设您暂时无法编写递归值。则 Mu Maybe 的成员，即值 :: forall r. (Maybe r -> r) -> r，是自然数 {0, 1, 2, ...}；Nu Maybe 的成员，即值 :: exists x. (x, x -> Maybe x)，是共自然数 {0，1，2，...，∞}。思考这些类型的可能值，看看为什么 Nu Maybe 有一个额外的成员。

如果您想对这些类型有一些直觉，可以尝试在没有递归的情况下实现以下内容（按难度递增的粗略顺序）：

zeroMu :: Mu Maybe、succMu :: Mu Maybe -> Mu Maybe

zeroNu :: Nu Maybe：零型“Nu”是一个包含的Maybe类型的空列表。

succNu :: Nu Maybe -> Nu Maybe：将给定的“Nu Maybe”类型中的元素添加到尾部并返回新的“Nu Maybe”。

inftyNu :: Nu Maybe：无限制的“Nu Maybe”类型，其中包含无限个空值“Maybe”。

muTofix :: Mu f -> Fix f：将极小不动点“Mu f”转换为具有相同类型参数的不动点“Fix f”。

fixToNu :: Fix f -> Nu f：将不动点“Fix f”转换为最大不动点“Nu f”。

inMu :: f (Mu f) -> Mu f：将类型参数为“Mu f”的函数应用于类型为“f（Mu f）”的值，并返回一个新的“Mu f”类型的值。

outMu :: Mu f -> f (Mu f)：从类型“Mu f”中提取出类型参数为“f”的函数，并返回一个新的类型为“f（Mu f）”的值。

inNu :: f (Nu f) -> Nu f：将类型参数为“Nu f”的函数应用于类型为“f（Nu f）”的值，并返回一个新的“Nu f”类型的值。

outNu :: Nu f -> f (Nu f)：从类型“Nu f”中提取出类型参数为“f”的函数，并返回一个新的类型为“f（Nu f）”的值。

nuToFix :: Nu f -> Fix f：将最大不动点“Nu f”转换为具有相同类型参数的不动点“Fix f”。

fixToMu :: Fix f -> Mu f：将不动点“Fix f”转换为最小不动点“Mu f”。

注意，因为“Mu f”是极小不动点，而“Nu f”是最大不动点，所以编写函数“:: Mu f -> Nu f”非常容易，但编写函数“:: Nu f -> Mu f”却很困难；这就像逆水行舟一样。

这里可能需要更详细的解释，但超出了此格式的范围。