Tutorial_03_Basic.lhs

Refinement Types
================

\begin{comment}
\begin{code}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
module Tutorial_03_Basic where

import Prelude hiding (abs)
divide  :: Int -> Int -> Int
die     :: String -> a

-- {-@ fail nonsense  @-}
-- {-@ fail canDie    @-}
-- {-@ fail divide'   @-}
-- {-@ fail avg       @-}
-- {-@ ignore lAssert @-}

\end{code}
\end{comment}

\newthought{What is a Refinement Type?} In a nutshell,

 > *Refinement Types* = *Types* + *Predicates*


\noindent
That is, refinement types allow us to decorate types with
*logical predicates*, which you can think of as *boolean-valued*
Haskell expressions, that constrain the set of values described
by the type. This lets us specify sophisticated invariants of
the underlying values.

Defining Types {#definetype}
--------------

Let us define some refinement types:^[You can read the type of `Zero` as:
"`v` is an `Int` *such that* `v` equals `0`" and `NonZero` as : "`v` is
an `Int` *such that* `v` does not equal `0`"]

\begin{code}
{-@ type Zero    = {v:Int | v == 0} @-}
{-@ type NonZero = {v:Int | v /= 0} @-}
\end{code}

\newthought{The Value Variable} `v` denotes the set of valid inhabitants
of each refinement type. Hence, `Zero` describes the *set of* `Int` values
that are equal to `0`, that is, the singleton set containing just `0`, and
`NonZero` describes the set of `Int` values that are *not* equal to `0`,
that is, the set `{1, -1, 2, -2, ...}` and so on.
^[We will use `@`-marked comments to write refinement
type annotations in the Haskell source file, making these
types, quite literally, machine-checked comments!]

\newthought{To use} these types we can write:

\begin{code}
{-@ zero :: Zero @-}
zero  = 0 :: Int

{-@ one, two, three :: NonZero @-}
one   = 1 :: Int
two   = 2 :: Int
three = 3 :: Int
\end{code}

Errors
------

If we try to say nonsensical things like:

\begin{code}
nonsense :: Int
nonsense = one'
  where
  {-@ one' :: Zero @-}
  one' = 1 
\end{code}

\noindent
LiquidHaskell will complain with an error message:

~~~~~{.sh}
../liquidhaskell-tutorial/src/03-basic.lhs:72:3-6: Error: Liquid Type Mismatch

72 |   one' = 1 :: Int
       ^^^^

  Inferred type
    VV : {VV : Int | VV == (1 : int)}

  not a subtype of Required type
    VV : {VV : Int | VV == 0}
~~~~~

\noindent
The message says that the expression `1 :: Int` has the type

~~~~~{.sh}
    {v:Int | v == 1}
~~~~~

\noindent
which is *not* (a subtype of) the *required* type

~~~~~{.sh}
    {v:Int | v == 0}
~~~~~

\noindent
as `1` is not equal to `0`.

Subtyping
---------

What is this business of *subtyping*? Suppose we have some more refinements of `Int`

\begin{code}
{-@ type Nat   = {v:Int | 0 <= v}        @-}
{-@ type Even  = {v:Int | v mod 2 == 0 } @-}
{-@ type Lt100 = {v:Int | v < 100}       @-}
\end{code}

\newthought{What is the type of} `zero`? `Zero` of course, but also `Nat`:

\begin{code}
{-@ zero' :: Nat @-}
zero'     = zero
\end{code}

\noindent
and also `Even`:

\begin{code}
{-@ zero'' :: Even @-}
zero''     = zero
\end{code}

\noindent
and also any other satisfactory refinement,
such as ^[We use a different names `zero'`,
`zero''` etc. as (currently) LiquidHaskell
supports *at most* one refinement type
for each top-level name.]


\begin{code}
{-@ zero''' :: Lt100  @-}
zero'''     = zero
\end{code}

\newthought{Subtyping and Implication}
`Zero` is the most precise type for `0::Int`, as it is a *subtype* of `Nat`,
`Even` and `Lt100`. This is because the set of values defined by `Zero`
is a *subset* of the values defined by `Nat`, `Even` and `Lt100`, as
the following *logical implications* are valid:

+ $v = 0 \Rightarrow 0 \leq v$
+ $v = 0 \Rightarrow v \ \mbox{mod}\ 2 = 0$
+ $v = 0 \Rightarrow v < 100$

\begin{comment}
Chris Tetreault: I believe that this whole section (within this comment block)
can be eliminated. It should be clear to anybody who's still following at this
point that if I can make a small boolean expression (Nat, Even, Lt100), that
I can make a massive boolean expression (Nat && Even && Lt100). I fell that this
section just uses a bunch of math runes to confuse us mere mortals, but doesn't
really add much.

\newthought{Composing Refinements}
If $P \Rightarrow Q$ and $P \Rightarrow R$ then $P \Rightarrow Q \wedge R$.
Thus, when a term satisfies multiple refinements, we can compose those
refinements with `&&`:

\begin{code}
{-@ zero'''' :: {v:Int | 0 <= v && v mod 2 == 0 && v < 100} @-}
zero'''' :: Int
zero''''     = 0
\end{code}
\end{comment}

\begin{comment}
ES: this is confusingly worded
\end{comment}

\newthought{In Summary} the key points about refinement types are:

1. A refinement type is just a type *decorated* with logical predicates.
2. A term can have *different* refinements for different properties.
3. When we *erase* the predicates we get the standard Haskell types.^[Dually, a
standard Haskell type has the trivial refinement `true`. For example, `Int` is
equivalent to `{v:Int|true}`.]

Writing Specifications
----------------------

Let's write some more interesting specifications.

\newthought{Typing Dead Code} We can wrap the usual `error`
function in a function `die` with the type:

\begin{code}
{-@ die :: {v:String | false} -> a  @-}
die msg = error msg
\end{code}

The interesting thing about `die` is that the input type has the
refinement `false`, meaning the function must only be called with
`String`s that satisfy the predicate `false`.
This seems bizarre; isn't it *impossible* to satisfy `false`?
Indeed! Thus, a program containing `die` typechecks *only* when
LiquidHaskell can prove that `die` is *never called*. For example, LiquidHaskell will *accept*

\begin{code}
cannotDie = if 1 + 1 == 3
              then die "horrible death"
              else ()
\end{code}

\noindent
by inferring that the branch condition is always `False` and so `die`
cannot be called. However, LiquidHaskell will *reject*

\begin{code}
canDie = if 1 + 1 == 2
           then die "horrible death"
           else ()
\end{code}

\noindent
as the branch may (will!) be `True` and so `die` can be called.




Refining Function Types: Pre-conditions
--------------------------------------

Let's use `die` to write a *safe division* function that
*only accepts* non-zero denominators.

\begin{code}
divide'     :: Int -> Int -> Int
divide' n 0 = die "divide by zero"
divide' n d = n `div` d
\end{code}

From the above, it is clear to *us* that `div` is only
called with non-zero divisors. However, LiquidHaskell reports an
error at the call to `"die"` because, what if `divide'`
is actually invoked with a `0` divisor?

We can specify that will not happen, with a *pre-condition*
that says that the second argument is non-zero:

\begin{code}
{-@ divide :: Int -> NonZero -> Int @-}
divide _ 0 = die "divide by zero"
divide n d = n `div` d
\end{code}

\newthought{To Verify} that `divide` never calls `die`, LiquidHaskell infers
that `"divide by zero"` is not merely of type `String`, but in fact
has the the refined type `{v:String | false}` *in the context* in
which the call to `die` occurs. LiquidHaskell arrives at this conclusion by
using the fact that in the first equation for `divide` the
*denominator* is in fact

~~~~~{.sh}
    0 :: {v: Int | v == 0}
~~~~~

\noindent
which *contradicts* the pre-condition (i.e. input) type.
Thus, by contradiction, LiquidHaskell deduces that the first equation is
*dead code* and hence `die` will not be called at run-time.

\newthought{Establishing Pre-conditions}
The above signature forces us to ensure that that when we
*use* `divide`, we only supply provably `NonZero` arguments.
Hence, these two uses of `divide` are fine:

\begin{code}
avg2 x y   = divide (x + y) 2
avg3 x y z = divide (x + y + z) 3
\end{code}

<div class="hwex" id="List Average">
Consider the function `avg`:

1. Why does LiquidHaskell flag an error at `n` ?
2. How can you change the code so LiquidHaskell verifies it?

</div>

\begin{code}
avg       :: [Int] -> Int
avg xs    = divide total n
  where
    total = sum xs
    n     = length xs
\end{code}


Refining Function Types: Post-conditions
---------------------------------------

Next, let's see how we can use refinements to describe the *outputs* of a
function. Consider the following simple *absolute value* function

\begin{code}
abs           :: Int -> Int
abs n
  | 0 < n     = n
  | otherwise = 0 - n
\end{code}

We can use a refinement on the output type to specify that the function
returns non-negative values

\begin{code}
{-@ abs :: Int -> Nat @-}
\end{code}

LiquidHaskell *verifies* that `abs` indeed enjoys the
above type by deducing that `n` is trivially non-negative
when `0 < n` and that in the `otherwise` case,
the value `0 - n` is indeed non-negative. ^[LiquidHaskell
is able to automatically make these arithmetic deductions
by using an [SMT solver][smt-wiki] which has built-in
decision procedures for arithmetic, to reason about the
logical refinements.]

Testing Values: Booleans and Propositions {#propositions}
-----------------------------------------

In the above example, we *compute* a value that is guaranteed to be a `Nat`.
Sometimes, we need to *test* if a value satisfies some property, e.g., is `NonZero`.
For example, let's write a command-line *calculator*:

\begin{code}
calc = do putStrLn "Enter numerator"
          n <- readLn
          putStrLn "Enter denominator"
          d <- readLn
          putStrLn (result n d)
          calc
\end{code}

\noindent which takes two numbers and divides them.
The function `result` checks if `d` is strictly positive
(and hence, non-zero), and does the division, or otherwise
complains to the user:

\begin{code}
result n d
  | isPositive d = "Result = " ++ show (n `divide` d)
  | otherwise    = "Humph, please enter positive denominator!"
\end{code}

Finally, `isPositive` is a test that returns a `True` if
its input is strictly greater than `0` or `False` otherwise:

\begin{code}
isPositive :: Int -> Bool
isPositive x = x > 0
\end{code}

\newthought{To verify} the call to `divide` inside `result`
we need to tell LiquidHaskell that the division only happens with a `NonZero`
value `d`. However, the non-zero-ness is established via the *test*
that occurs inside the guard `isPositive d`. Hence, we require a
*post-condition* that states that `isPositive` only returns `True`
when the argument is positive:

\begin{code}
{-@ isPositive :: x:Int -> {v:Bool | v <=> x > 0} @-}
\end{code}

In the above signature, the output type (post-condition)
states that `isPositive x` returns `True` if and only if
`x` was in fact strictly greater than `0`. In other words,
we can write post-conditions for plain-old `Bool`-valued *tests*
to establish that user-supplied values satisfy some desirable
property (here, `Pos` and hence `NonZero`) in order to then
safely perform some computation on it.

<div class="hwex" id="Propositions">
What happens if you *delete* the type for `isPositive` ?
Can you *change* the type for `isPositive` (i.e. write some other type)
while preserving safety?
</div>

<div class="hwex" id="Assertions">
Consider the following [assert][hoogle-assert] function, and two use sites.
Write a suitable refinement type signature for `lAssert` so that
`lAssert` and `yes` are accepted but `no` is rejected.
</div>

\begin{code}
{-@ lAssert  :: Bool -> a -> a @-}
lAssert True  x = x
lAssert False _ = die "yikes, assertion fails!"

yes = lAssert (1 + 1 == 2) ()
no  = lAssert (1 + 1 == 3) ()
\end{code}

\hint You need a pre-condition that `lAssert` is only called with `True`.

Putting It All Together
-----------------------

Let's wrap up this introduction with a simple `truncate` function
that connects all the dots.

\begin{code}
truncate :: Int -> Int -> Int
truncate i max
  | i' <= max' = i
  | otherwise  = max' * (i `divide` i')
    where
      i'       = abs i
      max'     = abs max
\end{code}

\noindent
The expression `truncate i n` evaluates to `i` when the absolute value
of `i` is less than the upper bound `max`, and otherwise *truncates* the value
at the maximum `n`. LiquidHaskell verifies that the use of `divide` is
safe by inferring that:

1. `max' < i'` from the branch condition,
2. `0 <= i'`   from the `abs` post-condition, and
3. `0 <= max'` from the `abs` post-condition.

From the above, LiquidHaskell infers that `i' /= 0`. That is, at the
call site `i' :: NonZero`, thereby satisfying the pre-condition
for `divide` and verifying that the program has no pesky
divide-by-zero errors.


Recap
-----

This concludes our quick introduction to Refinement Types and
LiquidHaskell. Hopefully you have some sense of how to

1. **Specify** fine-grained properties of values by decorating their
   types with logical predicates.
2. **Encode** assertions, pre-conditions, and post-conditions with suitable
   function types.
3. **Verify** semantic properties of code by using automatic logic engines
   (SMT solvers) to track and establish the key relationships between
   program values.