I just wrote a family of functions that operate over some type, e.g.
type t = A | B | C
A is a happy path of sorts, and can be handled easily and cheaply; others need much more complicated “clean up” of sorts. So, most of the functions I wrote had a structure like so:
let foo x y t = match t with A -> (x, y) | _ -> (* costly computations over x, y *) match t with | A -> (x, y) | B -> (* computation *) | C -> (* computation *)
It’s unfortunate that I had to repeat the
A case anywhere after that first
match to satisfy the exhaustiveness checks.
There’s a notion in Typed Racket called “occurrence typing”, where within the
then branch of a conditional (for example), the type of a checked value is narrowed based on the predicate used.
It seems that something similar would be very helpful in cases like this, where in the second arm of the above example’s first
match, the effective type of
t could be narrowed to
type t = B | C. The benefits might be amplified to whatever extent functions like
foo call hidden helper functions with values of narrowed types.
Is this something that has been discussed or proposed previously?