content:   {#abstractrefinements}
  ========================
  
  <div class="hidden">
  
  \begin{code}
  module AbstractRefinements where
  
  import Prelude 
  import Language.Haskell.Liquid.Prelude
  {-@ LIQUID "--no-termination" @-}
  
  -- o,no        :: Int
  maxInt       :: Int -> Int -> Int
  \end{code}
  </div>
  
  
  Abstract Refinements
  --------------------
  
  Abstract Refinements
  ====================
  
  A Pervasive Problem
  --------------------
  
  <br>
  
  <div class="fragment">
  
  Cannot use *context-independent* specifications.
  
  </div>
  
  <br>
  
  <div class="fragment">
  
  Lets distill it to a simple example...
  
  </div>
  
  
  A Pervasive Problem
  --------------------
  
  
  <br>
  
  (First, a few aliases)
  
  <br>
  
  \begin{code}
  {-@ type Odd  = {v:Int | (v mod 2) = 1} @-}
  {-@ type Even = {v:Int | (v mod 2) = 0} @-}
  \end{code}
  
  
  
  Example: `maxInt` 
  -----------------
  
  Compute the larger of two `Int`s:
  
  \begin{spec} <br> 
  maxInt     :: Int -> Int -> Int 
  maxInt x y = if y <= x then x else y
  \end{spec}
  
  
  
  Example: `maxInt` 
  -----------------
  
  Has **many incomparable** refinement types/summaries
  
  \begin{spec}<br>
  maxInt :: Nat  -> Nat  -> Nat
  maxInt :: Even -> Even -> Even
  maxInt :: Odd  -> Odd  -> Odd 
  \end{spec}
  
  <br>
  
  <div class="fragment">*Which* should we use?</div>
  
  
  Refinement Polymorphism 
  -----------------------
  
  `maxInt` returns **one of** its two inputs `x` and `y` 
  
  <div class="fragment">
  
  <div align="center">
  
  <br>
  
  ---------   ---   -------------------------------------------
     **If**    :    the *inputs* satisfy a property  
  
   **Then**    :    the *output* satisfies that property
  ---------   ---   -------------------------------------------
  
  <br>
  
  </div>
  </div>
  
  <div class="fragment">Above holds **for all properties**!</div>
  
  <br>
  
  <div class="fragment"> 
  
  **Need to abstract properties over types**
  
  </div>
  
  Parametric Refinements 
  ----------------------
  
  Enable *quantification over refinements* ...
  
  <br>
  
  <div class="fragment">
  \begin{code}
  {-@ maxInt :: forall <p :: Int -> Prop>. 
                  Int<p> -> Int<p> -> Int<p>  @-}
  
  maxInt x y = if x <= y then y else x 
  \end{code}
  </div>
  
  <br>
  
  <div class="fragment">Type says: **for any** `p` that is a property of `Int`, </div>
  
  - <div class="fragment">`max` **takes** two `Int`s that satisfy `p`,</div>
  
  - <div class="fragment">`max` **returns** an `Int` that satisfies `p`.</div>
  
  Parametric Refinements 
  ----------------------
  
  Enable *quantification over refinements* ...
  
  <br>
  
  \begin{spec}<div/>
  {-@ maxInt :: forall <p :: Int -> Prop>. 
                  Int<p> -> Int<p> -> Int<p>  @-}
  
  maxInt x y = if x <= y then y else x 
  \end{spec}
  
  <br>
  
  [Key idea: ](http://goto.ucsd.edu/~rjhala/papers/abstract_refinement_types.html)
  &nbsp; `Int<p>` &nbsp; is just  &nbsp; $\reft{v}{\Int}{p(v)}$ 
  
  <br>
  
  Abstract Refinement is **uninterpreted function** in SMT logic
  
  Parametric Refinements 
  ----------------------
  
  \begin{spec}<br>
  {-@ maxInt :: forall <p :: Int -> Prop>. 
                  Int<p> -> Int<p> -> Int<p>  @-}
  
  maxInt x y = if x <= y then y else x 
  \end{spec}
  
  <br>
  
  **Check Implementation via SMT**
  
  Parametric Refinements 
  ----------------------
  
  \begin{spec}<br>
  {-@ maxInt :: forall <p :: Int -> Prop>. 
                  Int<p> -> Int<p> -> Int<p>  @-}
  
  maxInt x y = if x <= y then y else x 
  \end{spec}
  
  <br>
  
  **Check Implementation via SMT**
  
  <br>
  
  $$\begin{array}{rll}
  \ereft{x}{\Int}{p(x)},\ereft{y}{\Int}{p(y)} & \vdash \reftx{v}{v = y} & \subty \reftx{v}{p(v)} \\
  \ereft{x}{\Int}{p(x)},\ereft{y}{\Int}{p(y)} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{p(v)} \\
  \end{array}$$
  
  Parametric Refinements 
  ----------------------
  
  \begin{spec}<br>
  {-@ maxInt :: forall <p :: Int -> Prop>. 
                  Int<p> -> Int<p> -> Int<p>  @-}
  
  maxInt x y = if x <= y then y else x 
  \end{spec}
  
  <br>
  
  **Check Implementation via SMT**
  
  <br>
  
  $$\begin{array}{rll}
  {p(x)} \wedge {p(y)} & \Rightarrow {v = y} & \Rightarrow {p(v)} \\
  {p(x)} \wedge {p(y)} & \Rightarrow {v = x} & \Rightarrow {p(v)} \\
  \end{array}$$
  
  
  Using Abstract Refinements
  --------------------------
  
  - <div class="fragment">**If** we call `maxInt` with args satisfying *common property*,</div>
  - <div class="fragment">**Then** `p` instantiated property, *result* gets same property.</div>
  
  <br>
  
  <div class="fragment">
  
  \begin{code}
  {-@ xo :: Odd  @-}
  xo = maxInt 3 7     -- p := \v -> Odd v 
  
  {-@ xe :: Even @-}
  xe = maxInt 2 8     -- p := \v -> Even v 
  \end{code}
  
  </div>
  
  <br>
  
  <div class="fragment">
  **Automatically Infer Instantiation by Liquid Typing**
  <!-- CUT At call-site, instantiate `p` with unknown $\kvar{p}$ and solve! -->
  
  </div>
  
  Using Abstract Refinements
  --------------------------
  
  <br>
  <br>
  <br>
  
  [DEMO 02_AbstractRefinements.hs](../hs/02_AbstractRefinements.hs)
  
  
  Recap
  -----
  
  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Strengthened Constructors
  4. **Abstract Refinements** over functions 
  
  <br>
  <br>
  
  <div class="fragment">
    Abstract Refinements decouple invariants from **code** ...
  <br>
  
  <a href="06_Inductive.lhs.slides.html" target="_blank">[continue]</a>
  </div>
  
  