The Lattice Type System

I'm making very bad videos. Here's an intro to wombat2:

Here's the the one on wombat2's type system:

Proposition types complement subtyping

The way wombat2 works, both at compile time and runtime, is that actions are taken to move an expression's known type down the hierarchy. When we get to a type restricted to a single value then we have evaluated the expression. When we get down to a type restricted to the empty set of values, then expression evaluation has failed.

A natural question is: why do we have types representing propositions, such as:  x <% y. Why not just simple boolean expressions.

Suppose we have a type Dog, and it's a subtype of Animal. We have a value x of type Animal, and we have some proposition about it: say hasTail(x). Moving down the subtyping hierarchy can't invalidate a witness of this, or a witness of its negation. But if we can't decide until we've moved to a more specific subtype then the proposition and its negation both stay empty. Propositions can be evaluated at the right level of generality.

Wombat reborn ... as Wombat2

 I've decided to bring back the wombat name. Except that it is now wombat2 - no space before the 2. This will hopefully be easier to search for.

Future posts back at https://wombatlang.blogspot.com/.

Also: I've started posting videos on my PLodicy youtube channel: https://www.youtube.com/@RobertSmart/.