19:00 - 20:00
The Java type system gives useful guarantees about your software, but there are many properties that cannot be expressed: that a string contains only a name, only an address, or only sanitized HTML; the range of an integer; the units of measurement of a value. Optional type systems allow developers to improve the quality of their software by encoding additional properties as optional type systems and enforcing these properties at compile time. Extending the type checker might seem scary at first, but is really simple and only requires four components: the extended types, their subtyping relationships, rules for what type each expression in a program has, and rules to decide what operations are legal.
Starting from nothing, we will create a full-fledged type-checker for Java that detects real errors in real programs. Our type system will detect errors in the use of the Optional type that the Java compiler permits and that would go undetected until runtime. You will also be ready to write your own checkers and use the dozens of available optional type systems that others have already implemented. Companies such as Amazon, Google, and Uber use these tools to improve their code quality and you can learn all about them!