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

Question

在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

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

Answer 1

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.

举一个具体的例子,假装你不能写递归值.居民Mu Maybe,即价值观:: forall r. (Maybe r -> r) -> r,是自然,{0,1,2,...}; 居民Nu Maybe,即价值观:: exists x. (x, x -> Maybe x),是fatural的{0,1,2,...,∞}.想想这些类型的可能值,看看为什么Nu Maybe有一个额外的居民.

如果你想对这些类型有一些直觉,那么在没有递归的情况下实现以下内容可能是一种有趣的练习(大致按难度递增顺序):

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

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

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

Mu f是最不固定的点,并且Nu f是最大的,因此编写函数:: Mu f -> Nu f非常容易,但编写函数:: Nu f -> Mu f很难; 就像在逆流而行.

(有一点,我的意思是写出这些类型的更详细的解释,但这种格式可能有点太长了.)