5
$\begingroup$

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:

  1. Does this system still have principal types?
  2. How much does the type-checking algorithm change?
Improve this question
$\endgroup$
5
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ Is that true for arbitrary quantifier alternation? By a quick scan of the works you cite I see restrictions on mixing quantifiers, existentials are only allowed in a few positions. This corresponds to my intuition that allowing existentials in arbitrary positions would have a similar effect to allowing universals under arrows, which makes inference impossible. $\endgroup$ – Gilles 'SO- stop being evil' Jul 18 '16 at 11:56
  • $\begingroup$ @Gilles Yes, you are right, I should have phrased myself more carefully, it's been a while since I looked at existentials. I've edited the answer. Anyway, quantifier alternation is the problem of higher-ranked types (HRTs). Rank essential counts the number of quantifier alternations. Type inference of HRTs is undecidable for rank > 2. Damas-Milner also imposes strong restrictions on where the universal quantifiers can appear. $\endgroup$ – Martin Berger Jul 18 '16 at 12:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.