Type inference

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 (either in Haskell):

NOTE: in types means Either in Haskell

Definition of :

Type signature of Left and Right:

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:

I will write that as:

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 in front of that, like we do for f and g.
In fact the type of is represented as:

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

Let’s infer!

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

The first step of the algorithm is attribute to all functions polymorphic types, so I will call the first type and the last

Because, have type , we conclude ;
Also, because have the type , we can conclude ;
Same thing to , that have the type , we can conclude and , so we have:

Because, the definition of : , we can say that the domain of f is equal to codomain of g, and so we can conclude , as we replace a type that is used in the codomain of first Right, we must also conclude , so:

As I explain before, the function , have the following type: , so:
and ;
Because have the type: , so and :

Because the definition of is , we need the same codomain in both functions, so we conclude , as both type trees have the same structure, we can conclude even more: , so:

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

.

Now we just need to unify: and ,

.

We infer the type for function , .
Or if you prefer; in Haskell:

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

About these ads