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?

Answers


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

Search




Leave an answer