[Question] What is the state of subtyping in mlish?

[Georges Dupéron]

Hi! I'm trying to extend mlish with subtypes. Here's what I understand of the current state of things:

• mlish infers variance on the polymorphic type variables (Xs) for custom variants declared with define-type, at least if they are not (mutually-)recursive types.
• #%app seems to handle subtyping just fine
• there is no subtyping relationship (I'm rolling my own, which takes advantage of #:arg-variances annotations, so that it doesn't need a special case for every type)
• some primitive types lack these variance annotations, e.g. the List type from stlc+cons.rkt (this was trivial to fix)
• most importantly, the solve function in mlish.rkt and the add-constraints/var? function from type-constraints.rkt do not take subtyping into account, this means that it will fail to unify X and some type if it already unified X with a sub/super-type, regardless of the variance on X.

I'm currently implementing that last point. Are there any other things that I should be aware of?

Did I miss a branch or piece of code which already implements parts of these? E.g. I'm surprised that I didn't find a general subtyping relationship which uses the #:arg-variances annotations, but maybe it's just implemented in another file.

Thanks!

Also, could we enable the wiki either here on bitbucket or on github? This would allow users like me to add some notes about the example languages and similar implementation details, which don't really have their place in the official documentation, as they are likely to evolve.

[Stephen Chang]

Hi Georges. Essentially, mlish does not support subtyping. @AlexKnauth may be able to give more details but any partial support is accidental I believe.

To add subtyping, your third and last bullet are most important, specifically:

• Override current-typecheck-relation with a proper subtyping predicate, utilizing arg-variances if possible

• Make sure solve uses current-typecheck-relation. There may also be other problems with solve and other related functions since we developed it specifically for mlish and other similar languages. One of our future work items is to try to make more general.

Also, be sure to report any problems with arg-variances, since it is an experimental features that has not really been explored fully.

[Stephen Chang]

Oh and a wiki is a good idea. Since most development has moved to github, I'll enable it there.

[Alex Knauth]

The arg variances are not used for subtyping. They are used to make the value restriction less restrictive, to allow polymorphism for more safe cases.

It's probably safe to use the arg variances for subtyping, but you won't be able to re-use much else for subtyping.

[Georges Dupéron]

Thanks for your answers! And thanks for opening the wiki, I started noting down a few things while the iron is hot.

A short report on my progress:

• Luckily (typecheck? τ₁ τ₂) seems to be used in a way that means τ₁ ⊑ τ₂, so most forms should work without modification.
• The (current-join) and (current-typecheck-relation) were easy to write using the arg-variances
• I had to pretty much rewrite add-constraints/var? from type-constraitns.rkt, as in the presence of subtyping, it needs to track whether it is trying to unify argument vs. signature in covariant or contravariant positions. I also realised that even if an X appears in an invariant position, its inferred type can still be generalised when considering later arguments. E.g. given (λ (a b f) (f a b)) : (→ X X (→ X X Y) Y), one can still call the function with arguments of the type Sub Super (→ Super Super Int), in that case X will be first "solved" as Sub, then "solved" as Super. For now, I'm tracking a lower bound and an upper bound (contravariant positions call (current-join) on the lower bound, covariant positions call (current-meet) on the upper bound, although I should modify this so that a current-meet is not necessary)
• the infer.rkt language uses add-constraints/var? in a weird way, it introduces some temporary type variables, and that breaks the clean caller vs callee distinction upon which my implementation relies. For now I'm leaving it out, since I'm only interested in adding subtyping to mlish.
• I'll dogfood this a bit, and hopefully submit a PR at some point.

Right now subtyping seems to work for MLish with my changes, but I need to things clean up, test, and see if I can cope with infer.rkt's more general use of add-constraints/var?.

[Georges Dupéron]

I just hit a variation of issue #15. With subtyping all arguments of a function can contribute to the type used for X, so the first argument of Cons does not place an expected type on the second argument anymore, and (Cons 1 Nil) fails to typecheck (with a user-defined List type).

Here are some solutions:

1. Introduce a ⊥ type, so that Nil : (List ⊥). In my current use case, I only have a partial order on types, with no need for ⊥ and ⊤, so I'd prever to avoid introducing them if possible, and for experimentation's sake it's probably better to not enforce their presence on language designers.
2. Add a sort of weak add-expected-type, to guide the instantiation for ⇐ rules, but still allow choosing a different type if a ⇒ rule applies. That sounds like a big change for a small issue, though.
3. Check whether a polymorphic type argument is actually used in the constructor, and give these positions an "irrelevant" variance, so that the #:arg-variances of (List X) produces irrelevant if the type is produced while typechecking Nil, but produces covariant otherwise.
4. Have Nil pick a dummy type that should disappear one inference is done, and add a syntax property on it indicating that it can be generalised to anything (similar to the previous point, but attaching the "irrelevant" info on a sort of ⊥ placeholder, instead of attaching it on the List tycons).
5. Something else?

Of course the solution should work in the general case for any variant, not just List X = Cons X (List X) | Nil.

Do you have any preference / suggestion ?