2
$\begingroup$

Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this tradeoff.

Does a similar Damas-Milner-like subset of the calculus of constructions exist, for which global type inference is possible? I expect the answer to be “yes” based on the following clues:

  • 1ML's abstract syntax already unifies terms and types, in a way reminiscent of System Fω's definition as a pure type system, and then makes type inference work for a subset of the language.

  • AFAICT, Damas-Milner type inference only requires that the type language be first-order, pure, terminating and confluent. First-order unification doesn't require that all unification variables range over a single sort (namely, that of types). A first-order, pure, terminating language can be carved out of a higher-order, effectful, potentially nonterminating language, by means of syntactic restrictions on terms in the latter.

But is there a definitive answer?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ As far as I'm aware, 1ML is "sugar for plain System Fω". Haskell doesn't have fully kind inference, you need these $*$, $**$ etc. $\endgroup$
    – Martin Berger
    Commented Jul 21, 2016 at 9:23
  • $\begingroup$ @MartinBerger: Haskell has kind inference. What it doesn't have is polymorphic kinds, at least not without a GHC extension. So, at the end of the kind inference process, all remaining kind unification variables are unified with *. $\endgroup$
    – isekaijin
    Commented Jul 21, 2016 at 15:46
  • $\begingroup$ @MartinBerger: System Fω can be presented in (at least) two ways: (0) with a stratified abstract syntax for kinds, types and terms (TAPL, pp. 450-451), or (1) as a pure type system, with a unified abstract syntax for all sorts (ATTAPL, pp. 72-73). 1ML is closer to the latter than to the former. $\endgroup$
    – isekaijin
    Commented Jul 21, 2016 at 15:51

1 Answer 1

Reset to default
5
$\begingroup$

As far as I can tell, there is no prime candidate for an analogue of Damas-Milner for CoC. Certainly there is no definitive answer.

Arguably, Damas-Milner isn't even a perfect inference system for $\mathrm{F}_\omega$, as in general it can't infer types with higher kinds in them (though it is an open question as to whether higher kinds are really necessary, see this problem).

At any rate, here's a rather simple argument against a definitive system for the CoC: unification modulo $\beta$ conversion is undecidable in general, even for terms with simple types. But for a given unification problem $t\approx u$ it is rather easy to set up a term which can be typed if and only if $t$ unifies with $u$:

$$ A : \Pi \vec{x}.C\ t\rightarrow \mathrm{nat},\ B:\Pi\vec{x}.C\ u\vdash A\ B$$

where the $\vec{x}$ are the free (unification) variables in $t$ and $u$, as well as the "implicit arguments" which are the analogue of the polymorphic type variables in Damas-Milner.

That being said, there are restrictions of the unification problem which are decidable, most notably Miller patterns which have good properties (uniqueness of solutions), so it's common to restrict implicit argument resolution to Miller patterns and reject the term otherwise.

In practice every dependently typed language does have to solve this problem, if only because giving every single type annotation is unworkably tedious. However, that inference is usually designed to fail in which case the user is asked to supply additional annotations, something which is absent from usual programing language type inference systems.

More background in this cs.stackexchange answer: https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable

and this one, more centered on the unification problem:

https://stackoverflow.com/questions/1936432/higher-order-unification

And (tooting my own horn further, I guess), I recommend the article Elaboration in Dependent Type Theory by de Moura et al, as a discussion of the issues involved.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ @MartinBerger actually that's a common misconception! Just because system $F$ has undecidable type inference doesn't automatically imply undecidability for an extension. A trivial counter-example is the type system in which every term is typable. More representative examples are undecidable subsysems of (classical) propositional logic. That being said, I'd be very surprised if $F_1$ turned out to have decidable inference. $\endgroup$
    – cody
    Commented Jul 26, 2016 at 16:01
  • $\begingroup$ you are right of course. I've deleted the comment. $\endgroup$
    – Martin Berger
    Commented Jul 26, 2016 at 16:10
  • $\begingroup$ I think the comment is quite useful actually! This is a subtle point that someone had to clarify for me as well (it was Alexandre Miquel, I think?). $\endgroup$
    – cody
    Commented Jul 26, 2016 at 19:53
  • $\begingroup$ I was quite embarrassed about this mistake because I have criticised others in the past who made it ... and then I make it myself. :( $\endgroup$
    – Martin Berger
    Commented Jul 26, 2016 at 20:26
  • $\begingroup$ "An expert is a man who's made all the mistakes you can make, in a narrow field". - Niels Bohr $\endgroup$
    – cody
    Commented Jul 26, 2016 at 21:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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