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

<p>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 <a href="http://tlca.di.unito.it/opltlca/opltlcasu19.html#x24-34000" rel="nofollow noreferrer">this problem</a>).</p>

<p>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$:</p>

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

<p>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.</p>

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

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

<p>More background in this cs.stackexchange answer: <a href="https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable">https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable</a></p>

<p>and this one, more centered on the unification problem:</p>

<p><a href="https://stackoverflow.com/questions/1936432/higher-order-unification">https://stackoverflow.com/questions/1936432/higher-order-unification</a></p>

<p>And (tooting my own horn further, I guess), I recommend the article <a href="http://arxiv.org/abs/1505.04324" rel="nofollow noreferrer">Elaboration in Dependent Type Theory</a> by de Moura <em>et al</em>, as a discussion of the issues involved.</p>

CC BY-SA 3.0
2016-07-26T16:01:11.817Z
@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.
cody
CC BY-SA 3.0
2016-07-26T16:10:03.627Z
you are right of course. I've deleted the comment.
Martin Berger
CC BY-SA 3.0
2016-07-26T19:53:31.140Z
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?).
cody
CC BY-SA 3.0
2016-07-26T20:26:14.080Z
I was quite embarrassed about this mistake because I  have criticised others in the past who made it ... and then I make it myself. :(
Martin Berger
CC BY-SA 3.0
2016-07-26T21:00:56.743Z
"An expert is a man who's made all the mistakes you can make, in a narrow field". - Niels Bohr
cody
CC BY-SA 3.0
2016-08-09T00:21:12.977Z
I don't miss higher-kinded type constructors when programming in ML. Types parameterized by proper types (of kind `*` in Haskell) are good enough for my use cases. Similarly, in a dependently typed language, I don't need types parameterized by functions. Types parameterized by values of `eqtype`s are good enough for my use cases.
isekaijin
CC BY-SA 3.0
2016-08-09T00:29:25.080Z
And I don't like the approach of allowing type inference to fail. I'm willing to use a less powerful type system, if that's what it takes to make type inference decidable.
isekaijin
CC BY-SA 3.0
2016-07-25T21:40:58.343Z
2016-07-25T21:40:58.343Z
2017-05-23T12:40:09.333Z
cody
<p>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.</p>

<p>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:</p>

<ul>
<li><p><a href="https://www.mpi-sws.org/~rossberg/1ml/" rel="nofollow">1ML</a>'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.</p></li>
<li><p>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.</p></li>
</ul>

<p>But is there a definitive answer?</p>

CC BY-SA 3.0
2016-07-21T09:23:02.913Z
As far as I'm aware, 1ML is "sugar for plain System Fω". Haskell doesn't have fully kind inference, you need these $*$, $**$ etc.
Martin Berger
CC BY-SA 3.0
2016-07-21T15:46:08.647Z
@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 *.
isekaijin
CC BY-SA 3.0
2016-07-21T15:51:19.313Z
@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.
isekaijin
<lo.logic><pl.programming-languages><type-theory>
Damas-Milner-like subset of the calculus of constructions with global type inference
isekaijin
# Damas-Milner-like subset of the calculus of constructions with global type inference

(Asked by: username_0 on 2016-07-20)

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](https://www.mpi-sws.org/~rossberg/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?

**Tags:** lo.logic, pl.programming-languages, type-theory
> **Comments:**
> **username_1**: As far as I'm aware, 1ML is "sugar for plain System Fω". Haskell doesn't have fully kind inference, you need these $*$, $**$ etc.  
> **username_0**: @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 *.  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_2 on 2016-07-25. Score: 5 | Accepted answer

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](http://tlca.di.unito.it/opltlca/opltlcasu19.html#x24-34000)).

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](http://arxiv.org/abs/1505.04324) by de Moura *et al*, as a discussion of the issues involved.

> **Comments:**
> **username_2**: @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.  
> **username_1**: you are right of course. I've deleted the comment.  
> **username_2**: 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?).  
> **username_1**: I was quite embarrassed about this mistake because I  have criticised others in the past who made it ... and then I make it myself. :(  
> **username_2**: "An expert is a man who's made all the mistakes you can make, in a narrow field". - Niels Bohr  
> **username_0**: I don't miss higher-kinded type constructors when programming in ML. Types parameterized by proper types (of kind `*` in Haskell) are good enough for my use cases. Similarly, in a dependently typed language, I don't need types parameterized by functions. Types parameterized by values of `eqtype`s are good enough for my use cases.  
> **username_0**: And I don't like the approach of allowing type inference to fail. I'm willing to use a less powerful type system, if that's what it takes to make type inference decidable.  

---

