Replace Greatest Dynamic Supertype with general retractive subtypes

[AshleyYakeley]

More useful, possibly more awkward?
Might annoy the user:

x1 = fn {
    a :: b => "non-empty";
    [] => "empty";
};

x2 = fn @(Node a b) {
    a :: b => "non-empty";
    [] => "empty";
};

This will yield x1 : (Pair Any Any & Unit) -> Text, x2 : Node Any Any -> Text.
There's just no way to infer a better argument type.

Solution: "partial" grounded types

Every "normal" ground type constructor G has a "partial" GTC partial G with representation Rep(partial G A B C...) = Maybe Rep(G A B C...).

Given a negative type T, we define Partial T:

• Partial None = None
• Partial (A & B) = (Partial A) & (Partial B)
• Partial x = x -- type variable
• Partial (G A B C...) = partial G A B C.. -- "normal" GTC
• Partial (partial G A B C...) = partial G A B C.. -- "partial" GTC

A case pat => expr with pat : P and expr : Q has type (Partial P) -> Q. (or get rid of Partial and put it in the pattern typing?)

Given a case c with type T, fn c : T. (or be non-partial here?)

Given cases c1 : T1, c2 : T2, etc., fn {c1; c2; ...} : T1 | T2 | ...

Subtype relations

If GTC G is in scope, then subtype G a b c... <: partial G a b c... is in scope.

At any point in scope, there is a consistent system of subtype relations between "normal" GTCs. However, some of these relations may be retractive. All "neutral" relations are retractive.

If there is a "retractive" path from grounded types P to Q then we have partial Q <: partial P.

Given "normal" grounded types P and Q and their "partial" counterparts partial P and partial Q, we determine subtype relations:

• P <: Q as normal, any path P to Q
• P <: partial Q is P <: P' and partial P <: partial Q
• partial P <: Q fails
• partial P <: partial Q: retractive path Q to P

Link Example

We have:

• subtype retractive Unit <: Link None None
• subtype retractive Pair a b <: Link a b

So now for our original example:

x1 = fn {
    a :: b => "non-empty";
    [] => "empty";
};

• case a :: b => "non-empty" has type Partial (Pair Any Any) -> Text = partial Pair Any Any -> Text
• case [] => "empty" has type Partial Unit -> Text = partial Unit -> Text
• So, x1 : (partial Pair Any Any -> Text) | (partial Unit -> Text) = x1 : (partial Pair Any Any & partial Unit) -> Text.
• And we have subsumption Link Any Any <: partial Pair Any Any & partial Unit:
  • Link Any Any <: partial Pair Any Any breaks down into Link Any Any <: partial Link Any Any (given) and partial Link Any Any <: partial Pair Any Any.
  • partial Link Any Any <: partial Pair Any Any requires a retractive path Pair Any Any to Link Any Any, which exists.

[AshleyYakeley]

• depends on fn type annotations #342

[AshleyYakeley]

With #342, if you omit the type annotation, you get the intersection of all the cases.

[AshleyYakeley]

Should be able to declare them.