liquidhaskell-0.8.2.0: docs/slides/BOS14/lhs/01_SimpleRefinements.lhs
{#simplerefinements}
=======================
Simple Refinement Types
-----------------------
<div class="hidden">
\begin{code}
{-@ LIQUID "--no-termination" @-}
module SimpleRefinements where
import Language.Haskell.Liquid.Prelude
import Prelude hiding (abs, max)
-- boring haskell type sigs
zero :: Int
zero' :: Int
safeDiv :: Int -> Int -> Int
abs :: Int -> Int
\end{code}
</div>
Simple Refinement Types
=======================
Types + Predicates
------------------
Example: Integers equal to `0`
------------------------------
<br>
\begin{code}
{-@ type Zero = {v:Int | v = 0} @-}
{-@ zero :: Zero @-}
zero = 0
\end{code}
<br>
<div class="fragment">
Refinement types via special comments `{-@ ... @-}`
<br>
<div class="fragment">
[DEMO](../hs/000_Refinements.hs)
<!-- BEGIN CUT
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo</a>
-->
</div>
Refinements Are Predicates
==========================
From A Decidable Logic
----------------------
<br>
1. Expressions
2. Predicates
<br>
<div class="fragment">
**Refinement Logic: QF-UFLIA**
Quant.-Free. Uninterpreted Functions and Linear Arithmetic
</div>
Expressions
-----------
<br>
\begin{spec} <div/>
e := x, y, z,... -- variable
| 0, 1, 2,... -- constant
| (e + e) -- addition
| (e - e) -- subtraction
| (c * e) -- linear multiplication
| (f e1 ... en) -- uninterpreted function
\end{spec}
Predicates
----------
<br>
\begin{spec} <div/>
p := e -- atom
| e1 == e2 -- equality
| e1 < e2 -- ordering
| (p && p) -- and
| (p || p) -- or
| (not p) -- negation
\end{spec}
<br>
Refinement Types
----------------
<br>
\begin{spec}<div/>
b := Int
| Bool
| ... -- base types
| a, b, c -- type variables
t := {x:b | p} -- refined base
| x:t -> t -- refined function
\end{spec}
Subtyping Judgment
------------------
<br>
$$\boxed{\Gamma \vdash t_1 \preceq t_2}$$
<div class="fragment">
<br>
Where **environment** $\Gamma$ is a sequence of binders
<br>
$$\Gamma \defeq \overline{\bindx{x_i}{t_i}}$$
</div>
Subtyping is Implication
------------------------
<br>
$$\boxed{\Gamma \vdash t_1 \preceq t_2}$$
<br>
[PVS' Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf)
<br>
(For **Base** Types ...)
Subtyping is Implication
------------------------
<br>
$$\boxed{\Gamma \vdash t_1 \preceq t_2}$$
<br>
$$
\begin{array}{rl}
{\mathbf{If\ VC\ is\ Valid}} & \bigwedge_i P_i \Rightarrow Q \Rightarrow R \\
& \\
{\mathbf{Then}} & \overline{\bindx{x_i}{P_i}} \vdash \reft{v}{b}{Q} \subty \reft{v}{b}{R} \\
\end{array}
$$
Example: Natural Numbers
------------------------
<br>
\begin{spec} <div/>
type Nat = {v:Int | 0 <= v}
\end{spec}
<br>
<div class="fragment">
$$
\begin{array}{rcrccll}
\mathbf{VC\ is\ Valid:} & \True & \Rightarrow & v = 0 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\
% & & & & & \\
\mathbf{So:} & \emptyset & \vdash & \Zero & \subty & \Nat & \\
\end{array}
$$
</div>
<br>
<div class="fragment">
Hence, we can type:
\begin{code}
{-@ zero' :: Nat @-}
zero' = zero -- zero :: Zero <: Nat
\end{code}
</div>
Contracts: Function Types
=========================
{#as}
------
Pre-Conditions
--------------
<br>
\begin{code}
safeDiv n d = n `div` d -- crashes if d==0
\end{code}
<br>
<div class="fragment">
**Requires** non-zero input divisor `d`
\begin{code}
{-@ type NonZero = {v:Int | v /= 0} @-}
\end{code}
</div>
<br>
<div class="fragment">
Specify pre-condition as **input type**
\begin{code}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{code}
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{spec} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{spec}
<br>
Precondition is checked at **call-site**
\begin{code}
{-@ bad :: Nat -> Int @-}
bad n = 10 `safeDiv` n
\end{code}
<br>
<div class="fragment">
**Rejected As**
$$\bindx{n}{\Nat} \vdash \reftx{v}{v = n} \not \subty \reftx{v}{v \not = 0}$$
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{spec} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{spec}
<br>
Precondition is checked at **call-site**
\begin{code}
{-@ ok :: Nat -> Int @-}
ok n = 10 `safeDiv` (n+1)
\end{code}
<br>
<div class="fragment">
**Verifies As**
$\bindx{n}{\Nat} \vdash \reftx{v}{v = n+1} \subty \reftx{v}{v \not = 0}$
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{spec} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{spec}
<br>
Precondition is checked at **call-site**
\begin{spec} <div/>
{-@ ok :: Nat -> Int @-}
ok n = 10 `safeDiv` (n+1)
\end{spec}
<br>
**Verifies As**
$$(0 \leq n) \Rightarrow (v = n+1) \Rightarrow (v \not = 0)$$
Post-Conditions
---------------
**Ensures** output is a `Nat` greater than input `x`.
\begin{code}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{code}
<br>
<div class="fragment">
Specify post-condition as **output type**
\begin{code}
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
\end{code}
</div>
<br>
<div class="fragment">
**Dependent Function Types**
Outputs *refer to* inputs
</div>
Postcondition: `abs`
--------------------
Specify post-condition as **output type**
\begin{spec} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{spec}
<br>
Postcondition is checked at **return-site**
<br>
Postcondition: `abs`
--------------------
Specify post-condition as **output type**
\begin{spec} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{spec}
<br>
**Verified As**
<br>
$$\begin{array}{rll}
\bindx{x}{\Int},\bindx{\_}{0 \leq x} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\
\bindx{x}{\Int},\bindx{\_}{0 \not \leq x} & \vdash \reftx{v}{v = 0 - x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\
\end{array}$$
Postcondition: `abs`
--------------------
Specify post-condition as **output type**
\begin{spec} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{spec}
<br>
**Verified As**
<br>
$$\begin{array}{rll}
(0 \leq x) & \Rightarrow (v = x) & \Rightarrow (0 \leq v \wedge x \leq v) \\
(0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow (0 \leq v \wedge x \leq v) \\
\end{array}$$
Recipe Scales Up
----------------
<br>
<div class="fragment">
Define type *checker* and get *inference* for free [[PLDI 08]](http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf)
</div>
<br>
<div class="fragment">
Scales to Collections, HOFs, Polymorphism ...
</div>
<br>
<div class="fragment">
[DEMO](../hs/001_Refinements.hs)
<br>
[[continue...]](02_Measures.lhs.slides.html)
</div>