<p>Here I mean only simple typed Lambda calculus / Combinatory logic. <br>
Notation: Combinatory logic terms: <span class="math-container">$F, X_i, Y_i$</span>. Term application: <span class="math-container">$(F*X_1)$</span>. Type variables <span class="math-container">$x_i,y_i$</span>. Type assignment: <span class="math-container">$X:x_i$</span>.</p>
<p>There is well known <a href="https://en.wikipedia.org/wiki/Principal_type" rel="nofollow noreferrer">principal-type algorithm</a>. For a given term M we can derive the most general type (if it exists)</p>
<p>For example: <span class="math-container">$K:a\rightarrow(b\rightarrow a)$</span>, <span class="math-container">$KK:c\rightarrow(a\rightarrow(b\rightarrow a))$</span>, <span class="math-container">$SII$</span>:does not have a type.</p>
<p><strong>I am interested in the following problem:</strong></p>
<p>Hidden term: <span class="math-container">$F:x\rightarrow y$</span></p>
<p>Given: <span class="math-container">$\{(X_1:x_1, Y_1=(F*X_1):y_1), (X_2:x_2, Y2=(F*X_2):y_2)\}$</span>, all pairs come in normal reduced form.</p>
<p>How to infer a type of hidden term <span class="math-container">$F$</span>? Such that <span class="math-container">$(F:x\rightarrow  y* X_1:x_1):y_1$</span> and <span class="math-container">$(F:x\rightarrow  y* X_2:x_2):y_2$</span></p>
<p><strong>For example:</strong></p>
<p>There is hidden term <span class="math-container">$F$</span>, <span class="math-container">$F=S:(a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$</span> <br>
We have access only to 2 (input, output) pairs:</p>
<p><span class="math-container">$X_1:x_1 = K:(a\rightarrow (b\rightarrow a))$</span> <br>
<span class="math-container">$Y_1:y_1 = F * X_1 = SK:(a\rightarrow b)\rightarrow (a\rightarrow a))$</span></p>
<p><span class="math-container">$X_2:x_2 = S:((a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$</span> <br>
<span class="math-container">$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)))$</span></p>
<p>How to infer a type <span class="math-container">$(x\rightarrow y)$</span> of hidden term <span class="math-container">$F$</span>, such that:
<span class="math-container">$(F:x\rightarrow y * X_1:(a\rightarrow (b\rightarrow a))) : (a\rightarrow b)\rightarrow (a\rightarrow a))$</span> <br>
<span class="math-container">$(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)))$</span></p>
<p>In this particular example, the answer is: <span class="math-container">$x\rightarrow y = (a\rightarrow (b\rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)))$</span> <br>
It is easy to verify. Given this type and type of <span class="math-container">$X_i$</span>, the principle type algorithm will derive <span class="math-container">$Y_i$</span> in both cases.</p>
<p>It is like backward type inference. For a set of <span class="math-container">$\{(input_1, output_1),..\}$</span> derive a most general type of a function.</p>
<p>Maybe there is a name for this problem that was already implemented in some programming languages?</p>

CC BY-SA 4.0
2022-09-22T10:25:29.850Z
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.
Martin Berger
CC BY-SA 4.0
2022-09-22T13:24:18.083Z
@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?
Oleg Dats
CC BY-SA 4.0
2022-09-24T10:39:39.363Z
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)
Martin Berger
CC BY-SA 4.0
2022-09-24T13:01:27.250Z
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$.
Oleg Dats
CC BY-SA 4.0
2022-09-24T16:41:19.703Z
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.
Martin Berger
CC BY-SA 4.0
2022-09-25T13:40:58.827Z
Understand now. I can not make a working Haskell code. :t (\f -> let x = k::a->b->a in let y = ((f x)::b1->a2->b2->a2) in f) Error: "Couldn't match expected type .. with actual type .. because type variables .. would escape their scope." Can you please provide a working code?
Oleg Dats
CC BY-SA 4.0
2022-09-26T13:32:58.830Z
I'm not a very proficient in Haskell, googling the error message, it have something to do with higher-ranked types which are not, in general, inferable. So you may have to add some type annotations?
Martin Berger
<type-theory><lambda-calculus><typed-lambda-calculus><combinatory-logic>
How to implement the next type inference algorithm?
Oleg Dats
# How to implement the next type inference algorithm?

(Asked by: username_0 on 2022-09-22)

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](https://en.wikipedia.org/wiki/Principal_type). 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?

**Tags:** type-theory, lambda-calculus, typed-lambda-calculus, combinatory-logic

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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?  
> **username_1**: 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)  
> **username_0**: 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$.  
> **username_1**: 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.  
> **username_0**: Understand now. I can not make a working Haskell code. :t (\f -> let x = k::a->b->a in let y = ((f x)::b1->a2->b2->a2) in f) Error: "Couldn't match expected type .. with actual type .. because type variables .. would escape their scope." Can you please provide a working code?  
> **username_1**: I'm not a very proficient in Haskell, googling the error message, it have something to do with higher-ranked types which are not, in general, inferable. So you may have to add some type annotations?  

---

## 0 answers

