Type systems have been successfully used to statically catch errors, like dividing an integer with a boolean. Still, well typed programs can go wrong, for example, with a division by zero resulting in a run-time exception!
Liquid Types enrich existing type systems with logical predicates and let you specify and automatically verify semantic properties of your code.
Structural vs. Semantics Properties
Most type systems reason about the structure of program values. integers and booleans have different structure, i.e., they are usually internally represented in different ways and they can be used with a different set of operations: integers can be divided and booleans can be conjuncted.
Other than the structure, values also have semantics. Liquid Types
enrich existing type systems with logical predicates and let you
specify semantic properties of values. For example, the Int type, can
be refined with logical predicates to describe integer values
different than 0:
{v:Int | v /= 0}
or natural numbers:
{v:Int | v >= 0}
Since with Liquid Types we are able to talk about semantics of values, we can also statically catch semantic type errors, like division by zero.
Tracking division by zero by Specifications
A type for the divisor operator states that given two integers, you will get back an integer.
div :: Int -> Int -> Int
This type effectively specifies the structure of the operator. If
your program compiles you can rest assured that all the arguments to
div are integers and not, say, booleans.
Using Liquid Types we can refine the above type to describe semantic properties
of the operator, specifically that the divisor should never be 0.
div :: Int -> {v:Int | v /= 0} -> Int
The above type provides a specification for the div operator. If
your program liquid-typechecks, the system has verified that the
second argument of div is different than 0, thus no
division-by-zero run-time exception will ever occur. Next let’s see how
this verification happens.
Verification of Specifications
Verification is a process that given your code and some specifications, here in the form of liquid-type signatures, decides whether the code satisfies the specifications.
Consider three uses of the div operator, the good, the bad, and the imprecise:
good = div 42 one -- OK
bad = div 42 zero -- type error
impr = div 42 nat -- type error
one :: { v:Int | 0 < v }
one = 1
zero :: { v:Int | 0 == v }
zero = 0
nat :: { v:Int | 0 <= v }
nat = 42
Verification will decide that only good is a good use of div, as follows.
First, it fires subtyping queries.
t1 is a subtype of t2, written t1 <: t2 iff
each expression that has type t1 also has type t2.
In our case, subtyping will check that at each call of div
the type of the divisor, is a subtype of the second argument of
the specification, namely {v:Int | v /= 0}.
For example, good will fire the following subtyping query:
{v:Int | 0 < v} <: {v:Int | 0 /= v}
Then, subtyping queries are discharged, via implication checking.
{v:Int | p } <: {v:Int | q } holds if p ⟹ q. For example:
{v:Int | 0 < v} <: {v:Int | 0 /= v}
∀ v. 0 < v ⟹ 0 ≠ vThus, verification of good succeeds as 0 < v ⟹ 0
≠ v, but verification of bad and impr fails as neither
0 = v ⟹ 0 ≠ v, nor 0 ≤
v ⟹ 0 ≠ v.
Note that types provide an abstraction of your program.
When we defined nat we abstracted the value 42 as a natural number,
nat :: {v:Int | 0 <= v}.
This is a proper specification for 42 but imprecise, as it misses the information
that 42 is not 0, thus it is a good divisor.
In short, our analysis is not complete in that it may create type errors
that are not true errors.
On the good side, our analysis is sound in that if it says OK
there cannot be a violation of a specification.
The Liquid Story (Further Reading)
Liquid Types (Logically Qualified Data Types) were introduced in 2008 by Rondon, Kawaguchi and Jhala at the ProgSys groups of UCSD. Since then they have been used to specify and verify ML, C, and Haskell.
Liquid Types are dependent types, i.e., types that depend on arbitrary program expressions like the ones we see in Coq, Agda, etc.
Liquid Types are refinement types, that is types that are refined with logical predicates that cannot be arbitrary expressions (like dependent types) but are expressions drawn from a sublanguage. Example of refinement type systems include DML, Sage, F*, etc.
Liquid Types are a constraint form of refinement types in that logical predicates come from a decidable sublanguage, that is a logical language for which implication checking is decidable. Examples of such decidable languages are quantifier-free theories as arrays, integer linear, set theory etc.
On one hand, the decidable constraint allows us to predictably use SMT solvers to decide implication checking. As we discussed earlier, type checking reduces to implication checking, thus liquid types allow decidable type checking, and type inference!
On the other hand, the decidable constraint syntactically restricts the specification language. What kind of specifications can be expressed using a decidable logic? This is still an open question, but using tricks like Abstract or Bounded Refinement Types we can express sophisticated properties using only decidable logics.
In few words
Liquid Types provide a means to specify and automatically verify semantic properties of your code. They are a constraint form of dependent types where the specification language is decidable thus leading to a highly automated type system with low requirement of type annotations.
