[WIP] Infer instantiations for polymorphic arguments to polymorphic functions [rebase of Alex Knauth's PR on bitbucket]

[SuzanneSoy]

Hello,

I took @AlexKnauth somewhat outdated PR https://bitbucket.org/stchang/macrotypes/pull-requests/21 and rebased it onto master. There were a few simple conflicts, so it's possible that I accidentally discarded or damaged part of the original patch.

The changes are only applied to the macrotypes/ subfolder for now. Is there an automated translation between the macrotypes/ and turnstile/ folders, or is the procedure simply to manually apply the changes in both directories?

After a few adjustments, most tests seem to succeed (I still have a few to fix).

it seems incapable of typechecking (Cons (λ ([x : X]) x) Nil), regardless of how many ann and inst I add to the expression. I suspect that this is because the ∀ are now lifted outwards as much as possible, but the solve and add-constraints probably need some adjustment to work with that.

[SuzanneSoy]

The reason why (Cons (λ ([x : Y]) x) Nil) would not typecheck was because the Y in → Y Y appeared in a contravariant position, and the relaxed value restriction (from http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf) says that polymorphic type variables cannot be generalisable if they appear in a contravariant position.

However, I suspect that this restriction only concerns type variables which were in the original signature of the function being called, not type variables which belong to arguments.

The last commit (9d812c0) therefore checks whether the X which may cause an error belongs to #'Xs (the stx-list of type variables from the (∀ (tyvar …) τ) signature of the function being called), instead of checking whether the X belongs to #'Xs* (the stx-list of type variables which appear in the signature + those which appear in the types of arguments).

I am not 100% sure this is the right thing to do, however, and cannot guarantee that this does not open the door to unsoundness with weird edge cases.

[stchang]

Yes, the examples in macrotypes and turnstile are independent. It has helped some people to be able to look at the two implementations side-by-side. It does result in somewhat more maintenance work but usually any changes are similar.

Is this still WIP?

[SuzanneSoy]

Yes, it's still WIP. Sorry for the delay, hopefully I'll be able to finish it soon.

[stchang]

No rush, just checking.

[stchang]

Would the original test still pass?

[SuzanneSoy]

No, that's one of the remaining issues.

With @AlexKnauth's change which lifts nested ∀ from the function's return type, the outer lambda has type (∀ (X Y) (→ X (→ Y Y))), but then the value restriction kicks in, and prevents Y from appearing in covariant positions (in case the body was a let-over-lambda capturing the Y type).

If I revert that commit, then the outer lambda's type is (∀ (X) (→ X (∀ (Y) (→ Y Y)))) (which sounds good to me as I used Typed Racket a lot, but @AlexKnauth I'm not sure if it is okay to revert that commit). The problem then becomes that (∀ (Y) (→ Y Y)) cannot be annotated as (→ Int Int), because the former is not a subtype of the former (an explicit instantiation is needed instead).

So I'm trying to see if I can find some combination of changes to solve + add-constraints + subtyping which makes everything work.

[stchang]

Ok, yes I'm playing around a bit more and see the behavior you mention. I'm starting to remember now and I think that was one of the original holdups because it means programs like (((λ ([x : X]) (λ ([y : Y]) y)) 1) 1) will be rejected which is not ideal.

Thanks for the update and thanks for work on this!

[AlexKnauth]

The type of the outer lambda should be (∀ (X Y) (→ X (→ Y Y))) so that type inference can instantiate either X or Y if it needs to. Here it needs to instantiate X as Int, but Y isn't constrained. So why is Y also solved to Int here?

[SuzanneSoy]

@AlexKnauth I'm not sure what you mean by "why is Y also solved to Int here?", could you clarify? Thanks!

Tentative answer: In that test, the (check-type … : (→ Int Int)) places an expected-type on the outer lambda's return value, which allows the Y to be instantiated to Int (but then the return type cannot be left as (→ Y Y), as the value restriction forces it to be monomorphic, IIUC).

[AlexKnauth]

Oh, right. So the test could just as easily be (check-type … : (→ String String)) and it would still pass. The Y in the answer we want should a non-generalizable type variable, like the ones notated '_a in the "Relaxing the Value Restriction" paper.