Advanced type narrowing

Advanced narrowing will likely be useless for 99% of users, but understanding the narrowing internals can be a fun exercise if you are up for a challenge.

The is? and is-a? type utilities are very useful, but each serves a very specific purpose (although those purposes are likely sufficient for most people.) is? and is-a? are each built out of more fundamental building blocks, which could in theory be used to define more custom narrowing behaviors. These building blocks are:

• when - Extract the "effects" from a particular type and put it onto another type
• supersect - Perform an upper-bound type intersection
• minus - Perform an upper-bound type subtraction

For example, is? is defined as

(or (when (supersect TYPE PRED) True)
    (when (minus TYPE PRED) Nil))

In other words, return True in the cases where TYPE overlaps with PRED, and Nil in the cases where TYPE differs from PRED.
To see how narrows propagate, watch what happens when we type-check (stringp obj):

(supersect String|Number{= obj} String) -> String{= obj}
(when String{= obj} True) -> True{obj : String}

(minus String|Number{= obj} String) -> Number{= obj}
(when Number{= obj} Nil) -> Nil{obj : Number}

(is? String|Number{= obj} String) -> True{obj : String} | Nil{obj : Number}

Similarly, is-a? is defined by the following:

(or (when (supersect TYPE PRED) True)
    Nil)

The isnt? type utility, the opposite of is?, is defined by simply flipping the order of is?:

(or (when (supersect TYPE PRED) Nil)
    (when (minus TYPE PRED) True))

Why upper-bound type-intersection?

When intersecting or subtracting two types, a perfect answer is not always possible (e.g. intersecting Integer with Positive).
A lower-bound intersection, as is performed by the subsect utility, is guaranteed to be entirely contained within the true intersection. Namely, the Never type is a (trivially) valid lower-bound intersection for any pair of types; For Integer and Positive, it is the only valid lower-bound.
An upper-bound intersection, as is performed by the supersect utility, is guaranteed to entirely contain the true intersection. For our example, both Integer and Positive would be valid upper-bound intersections, as a type itself is always guaranteed to be at least as large as its intersection with any other type.

Consider a positivep function, with type (is? T Positive). If is? used lower-bound intersection, (positivep Integer) would incorrectly report to never return True, since the lower-bound intersection of Integer and Positive would be Never. For this reason, upper-bound intersection (and for the same reason, subtraction) is necessary to guarantee that type-narrowing does not lie to us.