Fix 的 Böhm-Beraducci 编码

Question

我的定点函子定义如下：

newtype Fix f =
  Fix
    { unfix ::
      f (Fix f)
    }

我想定义一个函数，它接受

Fix f

并给出其 Böhm-Beraducci 编码。所以应该有这样的类型：

cata :: Fix f -> (forall a. (f a -> a) -> a)

我可以轻松定义这样的函数，但有额外的限制，即

f

是

Functor

，但我在没有这个限制的情况下挣扎。

直观上，我想采用 AST 并用输入函数替换

Fix

构造函数的所有实例，但实际上，这似乎需要

Functor

的

F

实例。但据我了解，即使

f

不是

Functor

，Böhm-Beraducci 编码也应该存在。

我觉得我在这里错过了一些简单的东西。我缺少定义吗？如果确实需要

Functor

，为什么？ Böhm-Beraducci 编码何时需要这样的额外约束？

Answer 1

快速浏览原始论文，看起来 Böhm-Berarducci 编码使用 System F 类型表示项代数。

项代数本质上涉及隐式

f

，它始终是一个函子。

Haskell 超越了这一点，它允许任何

f

上的术语级固定点，甚至是那些无法转换为函子的点。

一个著名的例子是负递归类型

newtype R a = R {unR :: R a -> a }

。 Haskell 类型系统允许这种类型定义。单独使用这个

R a

，并且没有术语级递归，我们可以导出

fix :: forall a . (a -> a) -> a

（顺便说一句，这是一个简短但不平凡的练习）。

相比之下，系统 F 可以“不”那么通用。如果系统 F 中有

R a，我们也会有 fix

，因此 

fix id :: forall a . a

 可以用于驻留在任何系统 F 类型中。但我们知道系统 F 是一致的，所以这种情况不会发生。