dfinity
`switch` should specialise the scrutinee as it eliminates cases
Many times the need arises to eliminate certain alternatives from variants and return a subtype of the scrutinee. Such a need surged in the VRC project, where some alternatives are of administrative rôle, while others should be public.
I have a function there
func tonise(e : LedgerEntry) : Tonsaction =
switch e {
case (#checkpoint _) panic "BAD!";
case (#buy b) #buy b;
case (#issue i) #issue i;
case (#list l) #list l;
case (#request r) #request r;
case (#retire r) #retire r;
case (#reject r) #reject r
};
whose job is to eliminate one alternative from a variant type. Note that this function has a lot of boilerplate, i.e. it grows in length with the number of alternatives. It will also run longer code sequences. I'd really like to write
func tonise(e : LedgerEntry) : Tonsaction =
switch e {
case (#checkpoint _) panic "BAD!";
case a a
};
but the type system won't let me.
This PR (for now) asks for removing variant alternatives that have already been tried (and failed, despite irrefutable sub-patterns).
In the example a should get Tonsaction type since type LedgerEntry = Tonsaction or { #checkpoint }.
Future extensions
In future (when we have some kind of type difference operator), we could progressively remove the inferred type of the case patterns from the scrutinee type for other type categories than variants too.
I know that coverage analysis already does something like this, I'd just want this feature in typing.ml with a user-facing benefit.
Alternatively, I’d like to have a type specialisation operator for variants (and maybe options) variantVal :\ #foo which operationally would switch on variantVal with case (#foo _) trap() and return variantVal otherwise. If variantVal : { #foo : T } or U then (variantVal :\ #foo) : U.
:\ pronounced as variant difference (like set difference).
There is of course a reason why practically no type checker does this: for this to make sense, you'll need a type system that can essentially represent the full domain of the abstract interpretation used for coverage checking, and moreover, a set-like type algebra that is sufficiently closed under difference. That is almost impossible to achieve in the presence of nested patterns, products, subtyping, variance, etc. It worked for XDuce/CDuce, but not much else.
The closest you can reasonably get in a clean enough manner is a sort of "cut" pattern:
func tonise(e : LedgerEntry) : Tonsaction =
switch e {
case (#checkpoint _) panic "BAD!";
case (a :! Tonsaction) a
};
where p :! T is a new pattern form that matches every case of T and checks p under that type (and p must cover all cases of T).
A somewhat more general way is decoupling this from binding and doing some sort of type refinement along conjunctive patterns ("as patterns"):
func tonise(e : LedgerEntry) : Tonsaction =
switch e {
case (#checkpoint _) panic "BAD!";
case (!Tonsaction and a) a
};
where !Tonsaction is a new pattern form that matches everything in that type. That is sort of what Ocaml does (where it's written #t), but with subtyping it becomes much more complex and hacky.
PS: What Flow (per your citation) does is control-flow sensitive typing, which is a whole different beast, super ad-hoc, very costly and very complicated in general. The only reason to have something like that is to add types to an untyped language after the fact -- it was invented for the Schemes and JavaScripts of this planet. You certainly don't want that in a properly typed language.
