2
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • $\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$
    – Martin Berger
    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$
    – Martin Berger
    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$
    – Martin Berger
    Sep 24, 2022 at 16:41

0

Reset to default

Your Answer

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