It lives! As of Monday Raven’s types are working, in the sense that fuzzing no longer continually finds new problems. It’s been a journey; I’ve seen types you wouldn’t believe. And it’s odd to have spent nearly four months on a few hundred lines of code. But while the result is relatively simple, it’s also utterly specific, everything just so; small changes can break it in non-obvious ways, which means I had to go down a lot of blind alleys to get here.
I’ve previously explored the broad goals of the type system, so this issue I’ll go a bit more into the implementation, and some interesting edge cases and problems that come up.
To start with, we need to compare types. The most basic operator is issubset(A, B) (or A ⊂ B), which is true if all values represented by A are also a part of B. For example, 1 ⊂ Int64; 1 in this case is a singleton type, representing a particular 64-bit integer, while Int64 represents all such integers. The reverse is not true: Int64 ⊄ 1. Similarly Int64 ⊄ Float64[1] but Int64 ⊂ (Int64 | Float64). issubset has some mathematical properties like transitivity, ie A ⊂ B ⊂ C implies A ⊂ C.