Type inference

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 (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)

Actions

Information

One response

6 08 2008
José Pedro Magalhães

I remember having found some serious problems with type inference in pointfree expressions when working on that with a classmate some years ago. One of the problems is that we needed to achieve a monomorphic result, but I think that’s not a problem for you here…

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s




%d bloggers like this: