# How to implement the next type inference algorithm?

Here I mean only simple typed Lambda calculus / Combinatory logic.
Notation: Combinatory logic terms: $$F, X_i, Y_i$$. Term application: $$(F*X_1)$$. Type variables $$x_i,y_i$$. Type assignment: $$X:x_i$$.

There is well known principal-type algorithm. For a given term M we can derive the most general type (if it exists)

For example: $$K:a\rightarrow(b\rightarrow a)$$, $$KK:c\rightarrow(a\rightarrow(b\rightarrow a))$$, $$SII$$:does not have a type.

I am interested in the following problem:

Hidden term: $$F:x\rightarrow y$$

Given: $$\{(X_1:x_1, Y_1=(F*X_1):y_1), (X_2:x_2, Y2=(F*X_2):y_2)\}$$, all pairs come in normal reduced form.

How to infer a type of hidden term $$F$$? Such that $$(F:x\rightarrow y* X_1:x_1):y_1$$ and $$(F:x\rightarrow y* X_2:x_2):y_2$$

For example:

There is hidden term $$F$$, $$F=S:(a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$$
We have access only to 2 (input, output) pairs:

$$X_1:x_1 = K:(a\rightarrow (b\rightarrow a))$$
$$Y_1:y_1 = F * X_1 = SK:(a\rightarrow b)\rightarrow (a\rightarrow a))$$

$$X_2:x_2 = S:((a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$$
$$Y_2:y_2 = F * X_2 = SS:(((a\rightarrow (b\rightarrow c))\rightarrow (a\rightarrow b))\rightarrow ((a\rightarrow (b\rightarrow c))\rightarrow (a\rightarrow c)))$$

How to infer a type $$(x\rightarrow y)$$ of hidden term $$F$$, such that: $$(F:x\rightarrow y * X_1:(a\rightarrow (b\rightarrow a))) : (a\rightarrow b)\rightarrow (a\rightarrow a))$$
$$(F:x\rightarrow y * X_2:((a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))) : (((a\rightarrow (b\rightarrow c))\rightarrow (a\rightarrow b))\rightarrow ((a\rightarrow (b\rightarrow c))\rightarrow (a\rightarrow c)))$$

In this particular example, the answer is: $$x\rightarrow y = (a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$$
It is easy to verify. Given this type and type of $$X_i$$, the principle type algorithm will derive $$Y_i$$ in both cases.

It is like backward type inference. For a set of $$\{(input_1, output_1),..\}$$ derive a most general type of a function.

Maybe there is a name for this problem that was already implemented in some programming languages?

• I'm not sure I understand your formalism. What is , what does $X_i$ and $F$ range over? I assume that $x, y, a, b$ are types, or type variables? If you are in the *simply-typed world, are up sure you can have principle types? Your question would be easier to answer, if you added more information about this. Sep 22, 2022 at 10:25
• @MartinBerger I have added an explanation and one more example. Is it clear now? Can you please explain your remark about the simply-typed world? Sep 22, 2022 at 13:24
• Can you not simply convert it into a standard type inference problem where you ask the type inference to check the term $let\ p_i : x_i = X_i\ in\ let\ q_i : y_i = Fp_i\ in\ F$ which should give you a principal type of $F$ if it exists. (I'm using let-notation for simplicity, you can translate this into pure lambda-calculus) Sep 24, 2022 at 10:39
• The setup of my problem is different. I do not have access to $F$. This function is hidden. I have access only to (input, output) and their types. The task is to infer a type of hidden function that is compatible with provided data. I can not substitute $F$ in your term because I do not have $F$. Sep 24, 2022 at 13:01
• I know you don't have access to $F$, I suggest to see $F$ as a variable, I should have made this clear, sorry. So you can wrap the let-expressions into e.g. $(\lambda F:z. ....)$ or something like that. Then you can read off the type you are looking for from the function. Sep 24, 2022 at 16:41