Lambda the Ultimate

Dependent typing is very interesting, although perhaps it can be pretty complicated to understand and use and implement? An alterantive, from Rondon, Kawaguchi, Jhala: Liquid Types.

We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without paying the heavy price of of manual annotation.