{#abstractrefinements} ======================== Abstract Refinements -------------------- Abstract Refinements ==================== Two Problems ------------
**Problem 1:** How do we specify *both* [increasing and decreasing lists](http://web.cecs.pdx.edu/~sheard/Code/QSort.html)?

**Problem 2:** How do we specify *iteration-dependence* in higher-order functions?
Problem Is Pervasive -------------------- Lets distill it to a simple example...

(First, a few aliases) 
64: {-@ type Odd  = {v:Int | (v mod 2) = 1} @-}
65: {-@ type Even = {v:Int | (v mod 2) = 0} @-}
Example: `maxInt` ----------------- Compute the larger of two `Int`s: 
77: maxInt     :: Int -> Int -> Int 
78: maxInt x y = if y <= x then x else y
Example: `maxInt` ----------------- Has *many incomparable* refinement types 
89: maxInt :: Nat  -> Nat  -> Nat
90: maxInt :: Even -> Even -> Even
91: maxInt :: Odd  -> Odd  -> Odd

Yikes. **Which** one 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 refinements over types**
By Type Polymorphism? --------------------- 
133: max     :: α -> α -> α 
134: max x y = if y <= x then x else y
Instantiate `α` at callsites 
142: {-@ o :: Odd  @-}
143: {VV : (Int) | ((VV mod 2) == 1)}o = forall <p :: (GHC.Types.Int)-> Bool>.
{x3 : (Int)<p> | true}
-> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (3  :  int))}3 {x2 : (Int) | (x2 == (7  :  int))}7     -- α := Odd
144: 
145: {-@ e :: Even @-}
146: {VV : (Int) | ((VV mod 2) == 0)}e = forall <p :: (GHC.Types.Int)-> Bool>.
{x3 : (Int)<p> | true}
-> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (2  :  int))}2 {x2 : (Int) | (x2 == (8  :  int))}8     -- α := Even
By Type Polymorphism? --------------------- 
155: max     :: α -> α -> α 
156: max x y = if y <= x then x else y

But there is a fly in the ointment ... Polymorphic `max` in Haskell ---------------------------- In Haskell the type of max is 
167: max :: (Ord α) => α -> α -> α

Could *ignore* the class constraints, instantiate as before... 
173: {-@ o :: Odd @-}
174: o     = max 3 7  -- α := Odd
Polymorphic `(+)` in Haskell ---------------------------- ... but this is *unsound*! 
182: max :: (Ord α) => α -> α -> α
183: (+) :: (Num α) => α -> α -> α

*Ignoring* class constraints would let us "prove": 
193: {-@ no :: Odd @-}
194: {VV : (Int) | ((VV mod 2) == 1)}no     = {x2 : (Int) | (x2 == (3  :  int))}3 x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (7  :  int))}7    -- α := Odd !
Type Polymorphism? No. ----------------------
Need to try a bit harder...
By Parametric Refinements! -------------------------- That is, enable *quantification over refinements*... Parametric Refinements ---------------------- 
213: {-@ maxInt :: forall <p :: Int -> Prop>. 
214:                 Int<p> -> Int<p> -> Int<p>  @-}
215: 
216: forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (Int)<p> | true}
-> {VV : (Int)<p> | true} -> {VV : (Int)<p> | true}maxInt {VV : (Int) | ((papp1 p VV))}x {VV : (Int) | ((papp1 p VV))}y = if {x3 : (Int) | ((papp1 p x3)) && (x3 == x)}x x1:{x6 : (Int) | ((papp1 p x6))}
-> x2:{x6 : (Int) | ((papp1 p x6))}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {x3 : (Int) | ((papp1 p x3)) && (x3 == y)}y then {x3 : (Int) | ((papp1 p x3)) && (x3 == y)}y else {x3 : (Int) | ((papp1 p x3)) && (x3 == x)}x

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 ---------------------- 
232: {-@ maxInt :: forall <p :: Int -> Prop>. 
233:                 Int<p> -> Int<p> -> Int<p>  @-}
234: 
235: maxInt x y = if x <= y then y else x

[Key idea: ](http://goto.ucsd.edu/~rjhala/papers/abstract_refinement_types.html) `Int

` is `{v:Int | (p v)}`

So, Abstract Refinement is an *uninterpreted function* in SMT logic
Parametric Refinements ---------------------- 
250: {-@ maxInt :: forall <p :: Int -> Prop>. 
251:                 Int<p> -> Int<p> -> Int<p>  @-}
252: 
253: maxInt x y = if x <= y then y else x

**Check** and **Instantiate** type using *SMT & predicate abstraction* Using Abstract Refinements -------------------------- -
**When** we call `maxInt` with args with some refinement,
-
**Then** `p` instantiated with *same* refinement,
-
**Result** of call will also have concrete refinement.
272: {-@ o' :: Odd  @-}
273: {VV : (Int) | ((VV mod 2) == 1)}o' = forall <p :: (GHC.Types.Int)-> Bool>.
{x3 : (Int)<p> | true}
-> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (3  :  int))}3 {x2 : (Int) | (x2 == (7  :  int))}7     -- p := \v -> Odd v 
274: 
275: {-@ e' :: Even @-}
276: {VV : (Int) | ((VV mod 2) == 0)}e' = forall <p :: (GHC.Types.Int)-> Bool>.
{x3 : (Int)<p> | true}
-> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (2  :  int))}2 {x2 : (Int) | (x2 == (8  :  int))}8     -- p := \v -> Even v
Using Abstract Refinements -------------------------- Or any other property 
289: {-@ type RGB = {v:_ | (0 <= v && v < 256)} @-}
290: 
291: {-@ rgb :: RGB @-}
292: {v : (Int) | (v < 256) && (0 <= v)}rgb = forall <p :: (GHC.Types.Int)-> Bool>.
{x3 : (Int)<p> | true}
-> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (56  :  int))}56 {x2 : (Int) | (x2 == (8  :  int))}8
Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4.
**Abstract:** Refinements over Type Signatures