yonutix February 2016

Which is the difference between these polymorphic types?

In System F, what is the difference between the following 3 types: Three formulas involving forall and implies as below.

Reproduced in text here:

∀X.((X → X) → (X → X))
∀X.((X → X) → ∀X.(X → X))
((∀X.X → X) → (∀X.X → X))

Is the second one more general than the first?


Heimdell February 2016

Depends on how tight forall quantifier binds. Lets assume that it binds on next terminal expression (variable or ()-block).

The first will become (X0 -> X0) -> (X0 -> X0) where X0 is a fresh type variable.

The second will become (X0 -> X0) -> forall X1. (X1 -> X1) where X0 and X1 are fresh.

The third - (bot -> X) -> (bot -> X) where X is the old binding and bot is the uninhabited forall X. X.

Post Status

Asked in February 2016
Viewed 1,149 times
Voted 7
Answered 1 times


Leave an answer