{#abstractrefinements} ======================== Abstract Refinements -------------------- Abstract Refinements ==================== A Pervasive Problem --------------------
Cannot use *context-independent* specifications.

Lets distill it to a simple example...
A Pervasive Problem --------------------
(First, a few aliases)
\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}
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}
maxInt :: Nat -> Nat -> Nat maxInt :: Even -> Even -> Even maxInt :: Odd -> Odd -> Odd \end{spec}
*Which* should we use?
Refinement Polymorphism ----------------------- `maxInt` returns **one of** its two inputs `x` and `y`

--------- --- ------------------------------------------- **If** : the *inputs* satisfy a property **Then** : the *output* satisfies that property --------- --- -------------------------------------------
Above holds **for all properties**!

**Need to abstract properties over types**
Parametric Refinements ---------------------- Enable *quantification over refinements* ...
\begin{code} {-@ maxInt :: forall

Prop>. Int

-> Int

-> Int

@-} maxInt x y = if x <= y then y else x \end{code}


Type says: **for any** `p` that is a property of `Int`,
-
`max` **takes** two `Int`s that satisfy `p`,
-
`max` **returns** an `Int` that satisfies `p`.
Parametric Refinements ---------------------- Enable *quantification over refinements* ...
\begin{spec}
{-@ maxInt :: forall

Prop>. Int

-> Int

-> Int

@-} maxInt x y = if x <= y then y else x \end{spec}
[Key idea: ](http://goto.ucsd.edu/~rjhala/papers/abstract_refinement_types.html)   `Int

`   is just   $\reft{v}{\Int}{p(v)}$
Abstract Refinement is **uninterpreted function** in SMT logic Parametric Refinements ---------------------- \begin{spec}
{-@ maxInt :: forall

Prop>. Int

-> Int

-> Int

@-} maxInt x y = if x <= y then y else x \end{spec}
**Check Implementation via SMT** Parametric Refinements ---------------------- \begin{spec}
{-@ maxInt :: forall

Prop>. Int

-> Int

-> Int

@-} maxInt x y = if x <= y then y else x \end{spec}
**Check Implementation via SMT**
$$\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}
{-@ maxInt :: forall

Prop>. Int

-> Int

-> Int

@-} maxInt x y = if x <= y then y else x \end{spec}
**Check Implementation via SMT**
$$\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 -------------------------- -

**If** we call `maxInt` with args satisfying *common property*,
-
**Then** `p` instantiated property, *result* gets same property.

\begin{code} {-@ xo :: Odd @-} xo = maxInt 3 7 -- p := \v -> Odd v {-@ xe :: Even @-} xe = maxInt 2 8 -- p := \v -> Even v \end{code}

**Automatically Infer Instantiation by Liquid Typing**
Using Abstract Refinements --------------------------


[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

Abstract Refinements decouple invariants from **code** ...
[continue]