系统 F 中的 Haskell 绑定运算符，包括种类

Question

我需要知道 Haskell 绑定类型 (>>=) 运算符的 System F 类型是什么。

到目前为止，我是这样写的：

(M::*->* A::*) -> (A::* -> (M::*->* B::*)) -> (M::*->*  B:*)

对吗？如果是正确的，我如何找到最终的结果？

谢谢！

Answer 1

你快到了。为类型变量添加显式量词，并删除每个变量使用的类型注释。

∀M:*->*. ∀A:*. ∀B:*. M A -> (A -> M B) -> M B

我使用了更传统的 : 而不是 Haskell 的 ::。

但是请注意，系统 F 没有更高的类型（例如 *->*），因此上述类型只能在更强大的类型系统中找到（例如 System Fω）。

此外，上面我“方便地”省略了M 的类型限制，这使得该类型接近但不完全是>>= 的Haskell 类型。 （另请参阅@DanielWagner 下面的评论）。

这个隐秘的细节很重要。否则，上面的类型太笼统了，以至于没有人居住——没有任何 lambda 术语具有这种类型。事实上，假设存在矛盾的 f 具有上述一般类型。那么，

f (λt:*. t->⊥) : ∀A,B:* . (A -> ⊥) -> (A -> B -> ⊥) -> B -> ⊥

其中 ⊥ 是任何空类型（例如，Void，在 Haskell 中）。但是然后，将⊤ 设为任何非空类型（例如，()，在 Haskell 中）与居民u，我们得到

f (λt:*. t->⊥) ⊥ : ∀B:* . (⊥ -> ⊥) -> (⊥ -> B -> ⊥) -> B -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ : (⊥ -> ⊥) -> (⊥ -> ⊤ -> ⊥) -> ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) : (⊥ -> ⊤ -> ⊥) -> ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) (λx:⊥. λy:⊤. x) : ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) (λx:⊥. λy:⊤. x) u : ⊥

所以⊥有人居住——矛盾。

更通俗地说，以上只是证明data T a = T (a -> Void) 不能是单子。