Haskell bind operator in System F including kinds

Question

I need to know what is the System F type of the Haskell bind type (>>=) operator.

Until now I writed it like this:

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

Is it right? If it is right how do I find the final result?

Thank you!

Answer 1

You're almost there. Add explicit quantifiers for type variables, and remove the type annotations on each variable use.

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

I used the more conventional : instead of Haskell's ::.

Note however that System F has no higher kinds (e.g. *->*), so the type above can only be found in more powerful type systems (e.g. System Fω).

Further, above I "conveniently" omitted the typeclass restriction on M, which makes the type close to, but not-quite, the Haskell type of >>=. (Also see the comment below by @DanielWagner).

This swept-under-the-rug detail is important. Otherwise, the type above is so general that it is not inhabited -- no lambda term has that type. Indeed, assume by contradiction there is f having the general type above. Then,

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

where ⊥ is any empty type (e.g. Void, in Haskell). But then, taking ⊤ to be any nonempty type (e.g. (), in Haskell) with inhabitant u, we obtain

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 : ⊥

so ⊥ is inhabited -- contradiction.

More informally, the above merely proves that data T a = T (a -> Void) can not be a monad.