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?

  • $\begingroup$ 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. $\endgroup$ Sep 22, 2022 at 10:25
  • $\begingroup$ @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? $\endgroup$
    – Oleg Dats
    Sep 22, 2022 at 13:24
  • $\begingroup$ 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) $\endgroup$ Sep 24, 2022 at 10:39
  • $\begingroup$ 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$. $\endgroup$
    – Oleg Dats
    Sep 24, 2022 at 13:01
  • $\begingroup$ 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. $\endgroup$ Sep 24, 2022 at 16:41


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.