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!
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.