liquidhaskell-0.8.2.0: docs/slides/flops14/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
nats :: L Int
evens :: L Int
odds :: L Int
range :: Int -> Int -> L Int
\end{code}
</div>
Simple Refinement Types
=======================
Types + Predicates
------------------
Ex: `Int`egers equal to `0`
---------------------------
<br>
\begin{code}
{-@ type EqZero = {v:Int | v = 0} @-}
{-@ zero :: EqZero @-}
zero = 0
\end{code}
<br>
<div class="fragment">
Refinement types via special comments `{-@ ... @-}`
<br>
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo</a>
</div>
Refinements Are Predicates
==========================
From A Decidable Logic
----------------------
1. Expressions
2. Predicates
Expressions
-----------
<br>
\begin{code} <div/>
e := x, y, z,... -- variable
| 0, 1, 2,... -- constant
| (e + e) -- addition
| (e - e) -- subtraction
| (c * e) -- linear multiplication
| (v e1 e2 ... en) -- uninterpreted function
\end{code}
Predicates
----------
<br>
\begin{code} <div/>
p := e -- atom
| e1 == e2 -- equality
| e1 < e2 -- ordering
| (p && p) -- and
| (p || p) -- or
| (not p) -- negation
\end{code}
Subtyping is Implication
------------------------
[PVS' Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf)
<!--
Subtyping is Implication
------------------------
<br>
<br>
-------- --- ------------------ --------- ------------------
**If** : Refinement of `S` *implies* Refinement of `T`
**Then** : `S` *subtype* `T`
-------- --- ------------------ --------- ------------------
<br>
-->
Subtyping is Implication
------------------------
<br>
<br>
--------- ------------ --------------------------
**If:** `P` `=> Q`
**Then:** `{v:t | P}` `<: {v:t | Q}`
--------- ------------ --------------------------
Example: Natural Numbers
------------------------
\begin{code} <div/>
type Nat = {v:Int | 0 <= v}
\end{code}
<br>
<div class="fragment">
------------- --------- ----------------
**By SMT:** `v = 0` `=>` `0 <= v`
**So:** `EqZero` `<:` `Nat`
------------- --------- ----------------
</div>
<br>
<div class="fragment">
Hence, we can type:
\begin{code}
{-@ zero' :: Nat @-}
zero' = zero -- zero :: EqZero <: Nat
\end{code}
</div>
{#universalinvariants}
=======================
Types = Universal Invariants
----------------------------
(Notoriously hard with *pure* SMT)
Types Yield Universal Invariants
================================
Example: Lists
--------------
<div class="hidden">
\begin{code}
infixr `C`
\end{code}
</div>
\begin{code}
data L a = N | C a (L a)
\end{code}
<br>
<div class="fragment">
*Every element* in `nats` is non-negative:
<br>
\begin{code}
{-@ nats :: L Nat @-}
nats = 0 `C` 1 `C` 3 `C` N
\end{code}
</div>
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a>
What if `nats` contained `-2`?
</div>
Example: Even/Odd Lists
-----------------------
\begin{code}
{-@ type Even = {v:Int | v mod 2 = 0} @-}
{-@ type Odd = {v:Int | v mod 2 /= 0} @-}
\end{code}
<br>
<div class="fragment">
\begin{code}
{-@ evens :: L Even @-}
evens = 0 `C` 2 `C` 4 `C` N
{-@ odds :: L Odd @-}
odds = 1 `C` 3 `C` 5 `C` N
\end{code}
</div>
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a>
What if `evens` contained `1`?
</div>
Contracts: Function Types
=========================
{#as}
------
Example: `safeDiv`
------------------
<br>
**Precondition** divisor is *non-zero*.
<br>
<div class="fragment">
\begin{code}
{-@ type NonZero = {v:Int | v /= 0} @-}
\end{code}
</div>
Example: `safeDiv`
------------------
<br>
+ **Pre-condition** divisor is *non-zero*.
+ **Input type** specifies *pre-condition*
<br>
\begin{code}
{-@ safeDiv :: Int -> NonZero -> Int @-}
safeDiv x y = x `div` y
\end{code}
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a>
What if precondition does not hold?
</div>
Example: `abs`
--------------
<br>
+ **Postcondition** result is non-negative
+ **Output type** specifies *post-condition*
<br>
\begin{code}
{-@ abs :: x:Int -> Nat @-}
abs x
| 0 <= x = x
| otherwise = 0 - x
\end{code}
{#dependentfunctions}
======================
Dependent Function Types
------------------------
<br>
Outputs **refer to** inputs
<br>
**Relational** invariants
Dependent Function Types
========================
Example: `range`
----------------
`(range i j)` returns `Int`s **between** `i` and `j`
Example: `range`
----------------
`(range i j)` returns `Int`s **between** `i` and `j`
<br>
\begin{code}
{-@ type Btwn I J = {v:_ | (I<=v && v<J)} @-}
\end{code}
Example: `range`
----------------
`(range i j)` returns `Int`s between `i` and `j`
<br>
\begin{code}
{-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
range i j = go i
where
go n | n < j = n `C` go (n + 1)
| otherwise = N
\end{code}
<br>
<div class="fragment">
**Note:** Type of `go` is automatically inferred
</div>
Example: Indexing Into List
---------------------------
\begin{code}
(!) :: L a -> Int -> a
(C x _) ! 0 = x
(C _ xs) ! i = xs ! (i - 1)
_ ! _ = liquidError "Oops!"
\end{code}
<br>
<div class="fragment">(Mouseover to view type of `liquidError`)</div>
<br>
<div class="fragment">To ensure safety, *require* `i` between `0` and list **length**</div>
<br>
<div class="fragment">Need way to **measure** the length of a list [[continue...]](02_Measures.lhs.slides.html)</div>