In the Damas-Milner type system, type schemata can be formed in two ways:
- $\forall X. S$
Where $T$ ranges over monotypes and $S$ ranges over type schemata. The type-checking algorithm for this system is well known, and explanations of it can be found in several places.
What happens if I add a third type schema former?
- $\exists X. S$
In other words, type schemata must still be in prenex normal form, but both universal and existential quantifiers may be used. As in Damas-Milner, only
let-bound variables may be ascribed type schemata.
My questions are:
- Does this system still have principal types?
- How much does the type-checking algorithm change?