4
$\begingroup$

I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME).

I was wondering, since Coq allows programs/values themselves to be in the Type somehow my guess would be that type inference is either:

  1. Doubly EXPTIME
  2. Undecidable

Does someone know the answer to this? A reference and an intuition would be highly appreciated too.


Now that I think about it - I don’t think it should be undecidable. Given a program (or a proof object), computing its type should be decidable given that we have all the constructors of the object. It seems very similar to type checking, except that we need to construct the type. If it were undecidable it feels it would be very hard to check the proof objects Coq builds.


related:

$\endgroup$
2
  • $\begingroup$ “It seems very similar to type checking, except that we need to construct the type” — You seem to be thinking that if type checking is decidable then so is type inference. This is not the case. A well-known counterexample is System F, for which type checking is decidable but inference is not. ML-style polymorphism hits a sweet spot where full inference is deciable. Basically anything fancier (in terms of type parametrization) requires at least partial annotations. $\endgroup$ Dec 22, 2021 at 19:55
  • $\begingroup$ @Gilles'SO-stopbeingevil' your guess makes sense - however, I was careful not to state that because it wasn't clear to me they were the same. I suspected they weren't and that's why I didn't state they were the same. I am overall interested in type inference only for the sake of this question. Overall, I tried to give context to the question. $\endgroup$ Dec 23, 2021 at 15:03

3 Answers 3

7
$\begingroup$

There are actually two questions here.

Is the Coq type system decidable?

Long answer short, we hope so, as in it would be a bug if it were not.

It is not a universal requirement for a type theory to have decidable type-checking, but it is considered a desirable property. When type-checking is not decidable, one has to cheat to implement the theory as a proof assistant. There are two typical ways out.

  • Only implement an approximation of the type-theory. So now there are two different type systems, the ideal-undecidable one, and the practical-decidable one. One can then try to relate these in some formal way, but usually it comes with its share of issues. Typically, the actual system breaks other good properties like e.g. subject reduction. This is the path taken by Lean.
  • Implement type-checking as a back-and-forth process with an oracle (i.e. the user) and rely on the additional missing information to make type-checking decidable again. Once again there are two systems, but the link between enriched derivations and raw terms is clearer. This is what the Andromeda system does, or, in another style, the PRL family of provers.

By design, Coq wants to prevent both situations, for foundational reasons. It is thus a requirement that CIC, the underlying type theory of Coq, enjoys decidable type-checking. This is a subtle property that goes beyond mere consistency of the system, or even strong normalization. The standard proof of decidability critically relies on the latter, but in the abstract it does not seem like a sufficient condition for a type theory to enjoy decidable type-checking.

As of today, the proofs of decidability of type-checking for CIC are murky, to say the least. Even though it is widely believed, it is not even clear that CIC is strongly normalizing. Add atop of that the fact that CIC is not really a well-defined system but rather an ever-growing system reflecting the liveliness of the Coq proof assistant, and you get an even more opaque situation.

As a matter of fact, Coq as in "the actual code" is known to not be strongly normalizing for silly reasons. Thankfully it seems to be normalizing for weak head reduction a priori, and this is enough for consistency / decidability, but this is quite frightening from a theoretical perspective.

What it the complexity of Coq type-checking algorithm?

Because Coq features dependent types, it is at least the complexity of the functions it can prove terminating. Indeed, if one can write e.g. a closed term M : nat -> bool such that M always answers true, it can be lifted in the type system by a reflexivity proof refl : M n = true for any closed natural number n. This always typechecks, but and cost of type-checking is obviously the one of reducing M n to a normal form.

Since we can write crazy functions in the logic of Coq (e.g. strong normalization of impredicative logics such as System F), typechecking complexity goes really, really beyond EXPTIME, or even ELEMENTARY as you seem to imply. CIC expressive power dwarves any complexity class you can think of.

Rather, it would be surprising to find a total function that cannot be written in Coq, barring standard Gödelian counterexamples like "an interpreter of CIC".

$\endgroup$
6
  • 1
    $\begingroup$ hmmm...thanks Pierre! That was very interesting. I am curious, does this mean that Coq type inference (not type checking) is undecidable? I think I am mostly interested right now to at least know if type inference is decidable or undecidable. Thanks again. $\endgroup$ Dec 22, 2021 at 18:47
  • $\begingroup$ Type inference has no unique definition for systems such as Coq, because there is no formal definition of the unannotated system agreed upon. If you define it as "remove all type annotations" then yes, it is undecidable. Coq contains System F, whose type inference is already undecidable. $\endgroup$ Dec 23, 2021 at 10:54
  • $\begingroup$ Cool! I guess Coq contains System F, whose type inference is already undecidable. is what I was looking for. Do you have a refence for 1) Coq containing system F 2) System F's undecidability? I can probably get the second one myself (I hope). $\endgroup$ Dec 23, 2021 at 15:04
  • 2
    $\begingroup$ Coq containing system F is almost trivial, for 2), the standard reference is "Typability and type checking in System F are equivalent and undecidable" by Wells, but indeed as @Pierre-MariePédrot notes, the definition of what a system is, is sublte here. $\endgroup$
    – ejgallego
    Dec 23, 2021 at 23:45
  • $\begingroup$ @ejgallego thanks for the reference! I will look it up. I was wondering, what is the intuition that type inference is undecidable? To me it seems trivial to just construct a type looking at the type annotations and construct an object as we traverse/evaluate the term...why doesn't that (naive) method work? $\endgroup$ Dec 24, 2021 at 19:51
2
$\begingroup$

It is decidable, as a consequence of the usual consistency proof, tho the exact time bound is not well understood AFAICT.

You can encode really huge functions into Coq that can take long to normalize, for a nice example see Ralf Loader's famous entry in the Bignum Bakeoff contest:

http://djm.cc/bignum-results.txt

$\endgroup$
2
  • $\begingroup$ Do you have a paper reference for "It is decidable, as a consequence of the usual consistency proof, tho the exact time bound is not well understood AFAICT."? Btw, I am most interested in the properties/runtime of the type inference engine. Thanks in advance! $\endgroup$ Dec 22, 2021 at 18:45
  • 1
    $\begingroup$ Type inference is a whole different beast and undecidable, for example see Golbfarb's proof of the undecibability of 2nd order unification. $\endgroup$
    – ejgallego
    Dec 23, 2021 at 23:46
2
$\begingroup$

Spurred by comments in Pierre Marie's answer, I'll add some clarification on the difference between type checking and type synthesis.

Generally, type checking in a dependent type system is designed to be decidable up to normalization for fully annotated terms, that is, $\lambda x : T.t$ and $\Pi x : T. U$ for example (you need type annotations in other places as well, e.g. in constructors of $\Sigma$ types). The algorithm is notionally straightforward, just recurse on the structure of the type, with a conversion step at application time that depends on normalization: $t\ u$ is well typed if $t$ is of type $\Pi x : T. U$ and $u$ is of type $T' = T$, so we need to do some reduction.

If annotations are omitted, however, it's a whole different ball game. Now you're trying to (essentially) guess the annotations, which is quite hard. Already in the simply-typed case, it can be in EXPTIME, as you have noted. There are several subsystems of CIC for which we have proven that it is undecidable in general to reconstitute the annotations, as I mention here: https://cs.stackexchange.com/a/12957/988. This is often called inference in the PL community, but in the subcommunity of dependent types, it's often referred to as synthesis.

Now, interestingly, undecidability for a subsystem of CIC doesn't automatically imply undecidability for full CIC! Imagine the (admittedly stupid) system which is CIC with the new type $\mathrm{Any}$ and the further rule:

$$ \frac{}{\Gamma\vdash t:\mathrm{Any}}$$

Now type inference is trivially decidable in this extension! So the fact that System F and $\lambda\Pi$ are undecidable do not automatically imply that the CIC is undecidable.

That being said, it very probably is, since there is little chance that the difficulties that crop up in the sub-systems are resolved by the more powerful one (and indeed, probably many more difficulties appear).

It would probably be a simple undergraduate affair to prove this undecidability.

Now how do systems do it in practice? They use heuristics based on "classical" Hindley-Milner inference, along with a few bags of tricks from various constraint-solving and higher-order unification insights. One interesting question would be to identify a fragment that these tricks will always work on, in the style of e.g. Practical type inference for arbitrary-rank types, but I'm not aware of such work.

$\endgroup$

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.