Subtyping and Variance

Unofficial/unsupported notes (i.e. changes to the implementation may affect what follows):

Subtyping

To extend a language with subtyping, one needs to:

• override current-typecheck-relation, which seems to be the ⊑ relation, possibly using variances to automatically derive a subtyping relation between the existing type constructors
• make sure all type constructors properly use #:arg-variances
• override current-join, using variances in the same way
• possibly override current-check-relation?
• For the languages mlish.rkt and infer.rkt, it would be desirable to extend inference of polymorphic arguments so that it works as expected without the need to explicitly up-cast arguments (I (@jsmaniac) am working on something for mlish.rkt, ping me for more info).

Variance

• The documented #:arg-variances allows a type declared using define-type-constructor to compute the variance for each argument position.
• get-arg-variances is implemented in typecheck.rkt.
• When considering a type #'(tycons τ₁ … τₙ), the variance computed by the #:arg-variances option is stored on the #'tycons identifier itself, as a syntax property.
• Calling (syntax-parse τ [(tycons τ ...) (get-arg-variances #'tycons)]) will retrieve the list of variances originally computed by the #:arg-variances.
• The variance struct is a #:prefab struct, so it can safely be embedded into syntax objects (this makes it easier to call (syntax-parse (list τ₁ τ₂ the-variance) […] …), without the risk of creating 3D syntax)
• The variance struct contains two fields, accessible via variance-covariant? and variance-contravariant?.
• The other two cases are variance-invariant? (i.e. both fields are #f) and variance-irrelevant? (i.e. both fields are #t, I suspect this can only happen for phantom type variables which do not appear in the actual type, and similar situations)
• variance-join (Variance Variance -> Variance) performs a conservative join of two variance constraints. The result will be covariant if and only if both arguments were covariant. The result will be contravariant if and only if both arguments were contravariant.
• variance-compose (Variance Variance -> Variance) computes the variance of a x-variant position occurring within a y-variant position. For example in (→ (→ ? Int) String), the type ? is in a contravariant position of the inner →, which itself occurs in a contravariant position of the outer →, therefore the ? position is covariant in the overall type. As expected, (variance-compose contravariant contravariant) will return covariant. Generally speaking, a contravariant flips the other argument's variance if the other argument is either covariant or contravariant. invariant is unaffected by the operation (i.e. if either argument is invariant, the result is invariant). irrelevant absorbs the other argument, I'm not sure why.