Two big MLsub hacks I made (that do not work)

In order to make MLsub fit my programming language, I've made two hacks into the system. They aren't the only ones, they're just the biggest.

These both have problems that I didn't anticipate when I came up with the idea. The constraints-idea doesn't produce a valid type-system as a result.

Relations/Constraints

I want algebra utilities that "just work". This desire leads to the first big hack.

1 + 1.5 + matrix[1, 0.2; 0, 1]

This code ends up instantiating the + twice. You get:

e with relations
    (+) [int|rational]       (int,rational) -> c
    (+) [c|matrix(rational)] (c,matrix(rational)) -> e

These are the first big hack, relations. The first relation can be solved because it's indexer no longer has any flow variables in it. We can solve the index because there is an unique coercion to rational:

{int}      ==> rational
{rational} =/> int

The addition for rational gives the type:

(rational, rational) -> rational

When we substitute this back in, we have solved one of the relations and we have an another that we can solve:

c with relations
    (+) [rational|matrix(rational)] (rational,matrix(rational)) -> c

Just like before, the indexer no longer has any free variables in it. Note that we take the constructors, not the whole type when searching for unique coercion.

{rational} ==> matrix
{matrix}   =/> rational

The rational is lifted into a matrix and we get to work with type:

(matrix(a), matrix(b)) -> matrix(c) with relations
    Add [a|b] (a,b) -> c

And when we substitute this back in, we get:

matrix(c) with relations
    (+) [rational] (rational,rational) -> c

This finally reduces to:

matrix(rational)

Like the other ML-style type inferencers, the MLsub works by generating constraints and then eliminating them from the equation. The problem here is that we have to eliminate every constraint before we can get to solve the relation clauses here.

Invalidity

The problem in the above model is that the logic doesn't add up. If I have addition with (int|rational, int), it potentially returns (int,int) and (rational, int) variations. I cannot isolate this effect into a single "indexer" variable without decreasing the precision of the type checker a lot.

Subtyping methods

The subtyping in MLsub is meant for simple situations, such as..

if p() then
    record = {x=1,y=2,z=3}
else
    record = {x=3,y=4}
return record.x

The records and attribute access can use similar signatures, so they will always fit.

A similar situation is with the function arguments or other 'simple' types.

But lets say we wanted to resolve something like:

vector(int) <: get.magnitude(a)

Our implementation for get.magnitude might be:

get.magnitude => (v): return v.x*v.x + v.y*v.y + v.z*v.z
vector(a): get.magnitude(c)
    Add [a] (a, a) -> b
    Mul [b] (b, b) -> c

We will end up with constraints:

get.magnitude(c) <: get.magnitude(a)
Add [int] (int,int) -> b
Mul [b] (b,b) -> c

And those constraints will resolve:

get.magnitude(int) <: get.magnitude(a)

This is the second hack I should do, and it suspiciously looks a lot like the first one. If it goes to this, we could as well just represent get.magnitude with..

get.magnitude :: a -> b
    Get.magnitude [a] b

This is different in that solving the constraint doesn't involve coercion. We just take instantiations and feed them back into Get.magnitude.

While we're at it, we can also transform calls:

(a,b,c,d): a(b,c,d) :: (a,b,c,d) -> e
    Call [a] (b,c,d) -> e

At this point we no longer have any contravariant in our system. It seems that the simple change of adding constraints means that this system is very different from MLsub.

I need to start looking around. I feel like I'm not going to get this to work after all.

Similar posts