Does Damas-Milner still have principal types if existential type schemata are added? In the Damas-Milner type system, type schemata can be formed in two ways:


$T$
$\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?
Yes, adding existentials doesn't add many complications for type inference, if quantifier alternation is controlled carefully. This is not surprising since universals and existentials are dual and the the function space operator gives a form of negation. Small type annotations that can help regaining type-inference are discussed in (4).

Adding existentials to pragmatically viable programming languages was first discussed in N. Perry's dissertation (1).  Perry's work was later formalised by Odersky and Läufer in (2). Läufer also described how to integrate existentials with Haskell type classes (3). 


1. N. Perry, The Implementation of Practical Functional Programming Languages.

2. K. Läufer, M. Odersky, Polymorphic type inference and abstract data types.

3. K. Läufer, Type classes with existential types.

4. M. Odersky, K. Läufer, Putting type annotations to work.