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 `impr`ecise:

``````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 ≠ v``

Thus, 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.

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.