30 07 2008

## Intro

The type inference is the ability to a programming language deduct the data types of all functions of a program. It is a feature present in many strongly typed languages, such as Haskell. Where is not mandatory write the signature of the functions. What is great because it increases the production of code, and security because if the inference algorithm fail means that we have an error of types in our code, all this in compilation time.

As I said in previous post, one of the upgrades of Pointfree calculator is the type inference. After reading some scientific articles about Damas-Milner algorithm, also known as W algorithm, I began to imagine a way to implement this in Java, which is the mother language of Pointfree calculator. I started to do some sketches on paper and, after talking with professor José Nuno Oliveira, I realize that the algorithm isn’t that hard.

## Remainings

Definition of $(\nabla)$ (either in Haskell):

NOTE: $+$ in types means Either in Haskell

$(\nabla)~:~(a~\rightarrow~c)~\rightarrow~(b~\rightarrow~c)~\rightarrow~a+b~\rightarrow~c$
$(\nabla)~f~g~(Left~a)~=~f~a$
$(\nabla)~f~g~(Right~b)~=~g~b$

Definition of $(+)$:
$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$
$f + g = (Left \circ f)\nabla(Right \circ g)$

Type signature of Left and Right:

$Left~:~a\rightarrow~a+b$
$Right~:~b\rightarrow~a+b$

## Talking same language

I will use a different notation to represent the domain and codomain of functions in order to help the explanation of the algorithm.

For $(+)$ function we have the type:

$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$

I will write that as:

$(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$

Remember the definition of $(+)$, we receive two functions, f and g. Because the notation is in pointfree, we represent also de domain and codomain of function $(f + g)$ in front of that, like we do for f and g.
In fact the type of $(f + g)$ is represented as:

$(f + g)~:~a+c~\rightarrow~b+d$

I will also use the symbol $a \sim b$, to say that type a unify with type b, that means, informally, that $a = b$.

## Let’s infer!

I will explain the algorithm to infer the type of function f:

$f = (id + Left) \nabla (Right \circ Right)$

The first step of the algorithm is attribute to all functions polymorphic types, so I will call the first type $t_1$ and the last $t_n$ $\forall_{1,\ldots,n}\in\mathbb{N}$

$\begin{array}{|l|}\hline((id_{{\color{blue}t_1}}^{{\color{blue}t_2}} + Left_{{\color{blue}t_3}}^{{\color{blue}t_4}})_{{\color{blue}t_5}}^{{\color{blue}t_6}} \nabla (Right_{{\color{blue}t_7}}^{{\color{blue}t_8}} \circ Right_{{\color{blue}t_9}}^{{\color{blue}t_{10}}})_{{\color{blue}t_{11}}}^{{\color{blue}t_{12}}})_{{\color{blue}t_{13}}}^{{\color{blue}t_{14}}}\\\hline\end{array}$

Because, $id$ have type $id~:~a\rightarrow~a$, we conclude $t_2 \sim t_1$;
Also, because $Left$ have the type $Left~:~a\rightarrow~a+b$, we can conclude $t_4 \sim t_3 + t_4$;
Same thing to $Right$, that have the type $Right~:~b\rightarrow~a+b$, we can conclude $t_8 \sim t_8 + t_7$ and $t_{10} \sim t_{10} + t_9$, so we have:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_2 \sim t_1, t_4 \sim t_3 + t_4, t_8 \sim t_8 + t_7, t_{10} \sim t_{10} + t_9 \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{{\color{blue}t_1}} + Left_{t_3}^{{\color{red}t_3+t_4}})_{t_5}^{t_6} \nabla (Right_{t_7}^{{\color{green}t_8+t_7}} \circ Right_{t_9}^{{\color{green}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because, the definition of $\circ$: $f \circ g = f(g(x))$, we can say that the domain of f is equal to codomain of g, and so we can conclude $t_7 \sim t_{10}+t_9$, as we replace a type that is used in the codomain of first Right, we must also conclude $t_8 + t_7 \sim t_8 + (t_{10} + t_9)$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_7 \sim t_{10}+t_9 \Rightarrow t_8 + t_7 \sim t_8 + (t_{10} + t_9) \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_5}^{t_6} \nabla (Right_{{\color{blue}t_{10}+t_9}}^{{\color{red}t_8+(t_{10}+t_9)}} \circ Right_{t_9}^{{\color{blue}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

As I explain before, the function $(+)$, have the following type: $(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$, so:
$t_6 \sim t_1+(t_3+t_4)$ and $t_5 \sim t_1+t_3$;
Because $f \circ g$ have the type: $(f_{a}^{b} \circ g_{c}^{d})_{c}^{b}$, so $t_{12} \sim t_8+(t_{10}+t_9)$ and $t_{11} \sim t_9$:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_6 \sim t_1+(t_3+t_4), t_5 \sim t_1+t_3 ,\\ t_{12} \sim t_8+(t_{10}+t_9), t_{11} \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{{\color{blue}t_1+t_3}}^{{\color{blue}t_1+(t_3+t_4)}} \nabla\\ (Right_{t_{10}+t_9}^{t_8+(t_{10}+t_9)} \circ Right_{t_9}^{t_{10}+t_9})_{{\color{red}t_9}}^{{\color{red}t_8+(t_{10}+t_9)}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because the definition of $(\nabla)$ is $(f_{a}^{b} \nabla g_{c}^{b})_{a+c}^{b}$, we need the same codomain in both functions, so we conclude $t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9)$, as both type trees have the same structure, we can conclude even more: $t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9) \Rightarrow\\ t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla\\ (Right_{{\color{blue}t_3}+{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})} \circ Right_{{\color{green}t_4}}^{{\color{blue}t_3}+{\color{green}t_4}})_{{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})})_{t_{13}}^{t_{14}}\\\hline\end{array}$

And now we have the function, just with the needed types to simplify:

$f_{t_{13}}^{t_{14}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

Now we just need to unify: $t_{14} \sim t_1+(t_3+t_4)$ and $t_{13} \sim (t_1+t_{3})+t_4$,

$\begin{array}{|l|}\hline\Leftrightarrow \{t_{14} \sim t_1+(t_3+t_4), t_{13} \sim (t_1+t_{3})+t_4\}\\\hline\end{array}$

$f_{{\color{red}(t_1+t_{3})+t_4}}^{{\color{blue}t_1+(t_3+t_4)}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

We infer the type for function $f = (id + Left) \nabla (Right \circ Right)$, $f : (t_1+t_3)+t_4 \rightarrow t_1+(t_3+t_4)$.
Or if you prefer; in Haskell:

f :: Either (Either a b) c -> Either a (Either b c)