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.

## 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.