Your answer is one click away!

yonutix February 2016
### Haskell bind operator in System F including kinds

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

Asked in February 2016

Viewed 3,390 times

Voted 8

Answered 1 times

Viewed 3,390 times

Voted 8

Answered 1 times