Type Inference

Type systems provide a kind of weak logic.

Binding Right

Type-Abstraction



Env + x:alpha |-  E : beta
____________________________________________

     Env |-  (\x. E) : beta

The Type System Used by POP2000

For POP2000 we have to adapt the above system to support type-inclusion.

The main idea is that we ascribe types to

Type-Application



Env  |-  F: alpha->beta      Env |- E:alpha
____________________________________________

     Env |-  (F E) : beta

Type-Abstraction



(rho + x:alpha,C) |-  E : beta
____________________________________________

(rho, C)     Env |-  (\x. E) : beta

Type-Application



Env  |-  F: alpha->beta      Env |- E:alpha
____________________________________________

     Env |-  (F E) : beta