Is there a general algorithm to fill holes in terms of the Calculus of Constructions? Suppose that you extend the Calculus of Constructions with "holes" - i.e., incomplete pieces of code that you didn't fill yet. I wonder if there is an algorithm to fill those roles automatically. For example (using Morte's syntax):

Case A:

λ (pred : ?) 
-&gt; λ (Nat : *) 
-&gt; λ (Succ : Nat -&gt; Nat) 
-&gt; λ (Zero : Nat)
-&gt; (Succ (pred Nat Succ Zero))


On this situation, a type inference algorithm can identify that ? can obviously only be ∀ (Nat : *) -&gt; (Nat -&gt; Nat) -&gt; Nat -&gt; Nat, because pred receives Nat : *, Succ : Nat -&gt; Nat, Zero : Nat, and must return Nat, because it is the first argument of Succ.

Case B:

(Id ? 4)


Where 4 is λ-encoded and Id is the identity function (i.e., ∀ (t:*) -&gt; λ (x:t) -&gt; x). On that situation, ´?´ is again clearly ∀ (N:*) -&gt; (N -&gt; N) -&gt; N -&gt; N, because that is the type of 4.

Case C:

(Id (Equals Nat 7 (add 3 ?)) (Refl 7))


Here,Equals and Refl are defined in a similar fashion to Idris. ? can obviously only be 4, but how do you figure that out? One way would be using the fact that ? : Nat, and Nat is a type which we know how to enumerate, so we can just try all Nats til it typechecks. That can be done for any enumerable type.

Case D:

(Id (Equal Nat 10 (MulPair ?)) 10)


Here, ? can only be of type Pair Nat; it has only more than one valid answer, though: it can be (Pair 10 1), (Pair 2 5), (Pair 5 2) and (Pair 1 10).

Case E:

(Id (Equal Nat 7 (Mul 2 ?)) 7)


Here, there is no valid answer, since 7 isn't a multiple of 2.



All those examples made me notice that we can make a general algorithm that identifies some known patterns and gives an answer by handpicking a specific algorithm (type inference, brute-force, and so on), kinda like Wolfram Alpha figures out the right strategy to solve an Integral. But that sounds like an engineering/hardcoded approach. Is there a principled way to solve this problem? Is there any research study/area on it?
There is certainly a lot of research into this problem! It often goes by the name of elaboration. It is an undecidable problem in general, as you may have guessed. The "holes" are often called meta-variables or unification variables.

As I explain a bit in this answer, the problem reduces to higher order unification, on which several people have written whole PhD dissertations.

As you note in your examples, some cases are somewhat easy, and can be solved by the application of simple rules, whereas some seem significantly more difficult, and have more of a "theorem proving" feel to them.

A third possible case is a "type class" type problem, where ? represents some kind of structure, such as a group or field structure, as in

mul ? 2 3


with mul : forall G:Group, G.carrier -&gt; G.carrier -&gt; G.carrier or some variant. Here we need to find a G such that G.carrier == nat.

In general, you want to have 3 different "regimes" for each type of problem, the simple unification, theorem proving, and type class resolution problems respectively.

We explain this a bit in the following paper:

Elaboration in Dependent Type Theory, de Moura, Avigad, Kong &amp; Roux.

You might want to look at the references of that paper for more info.



I've you've got a strong stomach, here is the open-source for elaboration in Lean.

Here is a wiki post that describes the interface to the elaborator in Idris.