What is the runtime of Coq's (dependent) Type Inference?

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.


related:

1 Like

It’s exponential but usually very quick: the slow cases occur in very unnatural code (source: TAPL).

“Type inference” seems too vague to answer, since Coq doesn’t have a single type inference algorithm (Program and refine use a more powerful one). Decidability is also probably affected by which features are used. Coq functions themselves are total, so per se they’re not a problem, however:

  • Higher-order unification is undecidable in general but has decidable restrictions; I’m not sure how much of that is used in type inference/unification. Also note that Coq has at least 2 unification algorithms — tactic unification, and evarconv.

  • Typeclass search need not terminate.

  • Canonical structure inference is pretty powerful but I cannot comment on its decidability, and there might be more.

hmmm…I was thinking something like “any piece of Coq code written, can we decide it’s type”. Not sure if that is too vague to give formal results + references.

Would restricting to Gallina help? (which is most of Coq as far as I understand, perhaps minus ltac and ssreflect)

Official references would be most useful. :slight_smile:

As I was trying to say, restricting to Gallina is still not enough: Definition foo uses a different inference algorithm from Program Definition foo (which also enables other features) and refine term. But if Gallina includes typeclasses (which IMHO it should), you can trivially add an instance loop to make inference diverge; you can probably encode more interesting problems to show TC search is Turing-complete.

So let’s maybe focus on pure Gallina using the Definition vernacular, without typeclasses, canonical structures, or any ways to invoke custom proof search procedures. Is there any description of the time complexity of some idealized inference algorithm?

Typechecking of fully specified terms is decidable, this is what the kernel does.
Once you have holes (_ or from implicit arguments) decidability is lost.

1 Like

The time complexity of Coq type inference is at least the time complexity of conversion checking for types. That involves evaluating arbitrary Coq functions, so the worst case complexity is bounded by Coq’s proof-theoretic strength, which is far beyond any decidable complexity class that comes up in complexity theory. In other words, if we pick a collection of decidable features (e.g. exclude looping tactics, instances etc), then the worst case complexity is still unimaginably high.

1 Like

Is there an official reference for Coq that analyzes the type inference algorithm?

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.

Both of your questions are covered by the answers above (EDIT: except for the reference, but I don’t think you could publish the reference you want in a paper, and I don’t know a textbook discussing this).

  • checking the proof objects that Coq builds must be decidable (as you say), but that is just type checking not type inference: all the holes and implicit arguments have already been inferred.
  • as Andras says, conversion checking (hence typechecking) takes virtually unbounded time. Since Coq can implement Ackermann’s function, it can express functions outside the “Primitive Recursive” class (PR (complexity) - Wikipedia). You can also write loops taking Ackermann(inputs) iterations. All Coq functions are recursive (so in R (complexity) - Wikipedia), even if Coq can’t express all recursive functions (in particular, not its own self-interpreter, by usual computability proof techniques).
1 Like

I think we can say that asking for the complexity of the typechecker has no meaning. Would you ask for the complexity of e.g. the ocaml toplevel? There is no bound to the time it may take to execute an (even small) arbitrary program. It is the same here since typechecking may need to actually execute a program.

Concrete example in ocaml:

ack 1000 1000;;

Concrete in coq typechecking:

Check (eq_refl (ack 1000 1000): ack 1001 1001=ack 1001 1001).

1 Like