I've been thinking for a while about something like an "assertion based type system." Rather than types being variants of other types, types can be described as other types + restrictions. Functions take variables with types but also come with a list of assertions. For example, it is sometimes useful in graphics to differentiate, in the type system, a 3D vector and a normalized vector (e.g. separate Vec3 and Norm3 types) but there is nothing you can do to actually put this into the type system. In some assertion based system, you would write something like: `type Norm3 = Vec3 v given(len(v) == 1)`. You could cast a Vec3 to a Norm3 which would run the assertion at run time, or you could write a function like `normalize` which always returns a Norm3 (maybe even it comes with its own assertion that len(v) != 0). Then you can safely pass your Norm3s to functions that expect normalized vectors. It's always recommended to make bad states unrepresentable, but it's weird how no language has ever given you a system like this.