Translating types with incompatible runtime representations in practice

[isaiahr]

First of all, thank you creating Simple-sub. I have (mostly) implemented it for my (hobby) language, and it seems to work great as far as I can tell.
That being said, I've ran into a bit of a roadblock in how to actually use the inferred types to compile code, when the runtime representation of subtypes isn't compatible, which maybe you can offer some insight on.

My intention is to translate functions using a large amount of monomorphization / specialization. For example, take the example

let getx = fun r -> r.x
let value = getx {x=3;y=2}
let value2 = getx {x=5}

Here I want to be able to produce 2 instances of getx, one where getx takes a struct of {x:int, y:int}, and the second a struct of {x:int}
Similarly, if I had a third call, perhaps with {x:string}, I would want to be able to produce a function of type {x:string} -> string.

So, my first question is, what is the best way to use the engine to properly constrain functions to do this? My initial approach is to traverse the AST for function calls, and then, if I had a = f x, to constrain x -> a <: f. Then since during the inference process, f <: x -> a, f will be constrained to be exactly type x->a. However the way I did this, it doesn't work, since x->a is receives its inferred type by determining its lower bound, and x->a's upper bound can be unconstrained. I think it might be possible to sort of copy the lower bound to the upper bound, to fix this approach, but there are still many other flaws with it, so I didn't attempt this.

Which leads my to the second question; how should I constrain the parameters? If you modify the environment to track all symbols, parameters, like r in the example, receive the bottom type. Of course this makes some sense because they are constrained by their use rather than their definition / value, but again, when translating types in practice, this is another difficulty. I think this question sort of overlaps with the first, in that the actual type of r should be determined when a specialized version of getx is produced. It seems to me that an elegant solution to my first question would propagate the constraints to the parameter and as such constrain its lower bound.
Third, How can I deal with the above problems in the general case? With my example above, the function call produces the specialization required, but in general this isn't true. For example, take

let id = fun x -> x
let apply = fun arg -> arg.f arg.x
let v = {f=id; x=3}
let u = apply v

Here id needs to be specialized even though it is not (directly) called.
The way I did this before switching to simple-sub, is to record every instantiation of a variable in the environment, which would typically receive enough constraints. however, doing this with simple-sub, gets types like a->(a∨Int), when inferring id 0 for example.

Sorry for all the lengthy questions. Perhaps subtyping isn't what I need at all, and hence all the difficulties. That being said it does feel I am really close to getting this to work, so any help would be much appreciated.

thanks.

[LPTK]

Hi @isaiahr, thanks for your interest in Simple-sub!

I am not sure I understood the details of what you are proposing, but it seems to me that you are trying to perform specialization at the same time as type inference/checking.

I have a feeling it would be cleaner (and easier to implement) to separate the two: first do type inference to ascribe polymorphic type schemes to your definitions and instantiate them where they are used; and then perform specialization. To do the latter, it should be enough to group all instantiation according to how they constrained the scheme's type variables.

Consider that each type has a coarser representation (also called "calling convention"), for example types nat and 42 both have calling convention int. To create specialized definitions, you'd group instantiations that constrain type variables with the same calling conventions, and report errors when conflicting calling conventions are used.

Though I have never tried to implement something like this, so I don't know how feasible/easy it is to do.

Third, How can I deal with the above problems in the general case? With my example above, the function call produces the specialization required, but in general this isn't true. For example, take

let id = fun x -> x
let apply = fun arg -> arg.f arg.x
let v = {f=id; x=3}
let u = apply v

Here id needs to be specialized even though it is not (directly) called.

That's a tougher problem, but I think the scheme I outlines above might work.

However, there will for sure be limitations (many things won't be compilable even if they type check), especially due to the lack of first-class polymorphism, for example if you do fun arg -> (arg.f "hi", arg.f 0).