An another MLsub study

There seem to be no victories in type inference.

Last weekend I started a project to implement Stephen Dolan's MLsub type inference in a small language explicitly designed for studying subtyping.

SuoML was a huge success. I learned a lot about the subject I embarked on studying.

What I learned is disappointing though. Solving problems of subtyping does not directly solve the problems of coercion.

Change of plans

The original plan to get this to work, was to solve the problems through cancellation. The function to retrieve x component from the vector would have ended up looking like:

get_x :: vector & a -> a without vector

This turned out to be a bad idea. The problem is that coercion extends the type and doesn't narrow it.

If the vector of integers was presented as vector|int, it would require that the vector of integers would have less features than what integers have. Otherwise we end up with questions such as should int <: getattr.x subsume?

SubML's algorithms would appear to require that int <: getattr.x fails if the int cannot satisfy the constraint on its own.

The another problem in cancellation was that it would add complexity to the algorithm of type inference. The state in inferencing biunification is already very complex and has lot of questions to answer, so we would prefer to not make it more complex from what it is.

This means that the problems related to coercion need to be solved outside from MLsub's inference system. Fortunately MLSub excels in representing traits.

Traits

The type system present in MLsub naturally represents ideas that datatypes can have multiple features and purposes that can be individually addressed.

For example, the requirement that the input should have accessible .x -attribute can be represented like this:

getattr_x :: a & getattr("x", b) -> b

Similarly we can represent that an input argument needs to have addition or multiplication implemented.

matrix_multiply :: [[a&(+,*)]] -> [[a&(+,*)]] -> [[a]]

Without the need for coercions we would get away with relatively simple type annotations. It could still form a nice language.

Implicit conversion from int to real or float would likely require care with specifying the division -operation. It might have to be of the form:

(/) :: a&(/) -> a&(/) -> fractional

It could be about as nice language as what your usual ML language is.

A way to solving coercions

The traits also provide a potential way to solving coercions. You could represent each operation with a relation and then have those relations leak out from the function a bit like how traits do.

When the relations do not leak out from the function you would know that you have a set of relations that are resolvable. You would solve them and feed the results back into the type inference graph.

I am planning to study this approach in detail next week.

Parametric polymorphism and recursion

Last week I did study Hindley-Milner type inference so that I'd get more out of the MLsub.

Like Hindley-Milner does it, it looks like MLsub can also distinguish between bound and free type variables.

Type inference in MLsub happens explicitly in graphs. If you copy a graph, you essentially do something similar to instantiating a graph.

The problem is that while HM treats type variables as explicit objects you remove by substitution, in MLsub the type variables are merely annotating data flows between variables.

In Hindley-Milner, generalize(expr, env) will add forall-binding for every variable that is free in the expression but not free in the environment. It's doing this for every environment variable, so the most outmost type environment isn't really treated different than what the innermost type environment is treated.

instantiate(expr) then eliminates the forall-binding, giving the HM its characteristic all-present parametric polymorphism.

In MLsub, the subset construction and graph copying serves some similar purposes for these two mechanisms, but these ideas are not as clear-cut. I think there exists a reliable isomorphism between these concepts, but I still have to find it.

Despite these problems, MLsub is relatively polymorphic. When treated with parametric polymorphism, MLsub needs the same fix that is also necessary in HM.

Assessments

It would seem that when the type system has to track out the relations, it will make the results grow larger than they would otherwise do.

I have one experiment left to do. If it succeeds then I am certain that I am going to get the coercion model to work and the ideas on this post will end up to my programming language.