content:  {#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="https://liquidhaskell.goto.ucsd.edu/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="https://liquidhaskell.goto.ucsd.edu/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="https://liquidhaskell.goto.ucsd.edu/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="https://liquidhaskell.goto.ucsd.edu/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>
  