lambda - Haskell bind operator in System F including kinds -

i need know system f type of haskell bind type (>>=) operator.

until writed this:

(m::*->* a::*) -> (a::* -> (m::*->* b::*)) -> (m::*->*  b:*) 

is right? if right how find final result?

thank you!

you're there. add explicit quantifiers type variables, , remove type annotations on each variable use.

∀m:*->*. ∀a:*. ∀b:*. m -> (a -> m b) -> m b 

i used more conventional : instead of haskell's ::.

note system f has no higher kinds (e.g. *->*), type above can found in more powerful type systems (e.g. system fω).

further, above "conveniently" omitted typeclass restriction on m, makes type close to, not-quite, haskell type of >>=. (also see comment below @danielwagner).

this swept-under-the-rug detail important. otherwise, type above general not inhabited -- no lambda term has type. indeed, assume contradiction there f having general type above. then,

f (λt:*. t->⊥) : ∀a,b:* . (a -> ⊥) -> (a -> b -> ⊥) -> b -> ⊥ 

where ⊥ empty type (e.g. void, in haskell). then, taking ⊤ nonempty type (e.g. (), in haskell) inhabitant u, 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 ⊥ inhabited -- contradiction.

more informally, above merely proves data t = t (a -> void) can not monad.