Abstract Refinements

Two Problems

Problem Is Pervasive

Lets distill it to a simple example...

67: {-@ type Odd  = {v:Int | (v mod 2) = 1} @-}
68: {-@ type Even = {v:Int | (v mod 2) = 0} @-}

Example: maxInt

Compute the larger of two Ints:

80: maxInt     :: Int -> Int -> Int 
81: maxInt x y = if y <= x then x else y

Example: maxInt

Has many incomparable refinement types

92: maxInt :: Nat  -> Nat  -> Nat
93: maxInt :: Even -> Even -> Even
94: maxInt :: Odd  -> Odd  -> Odd 

Refinement Polymorphism

maxInt returns one of its two inputs x and y

Parametric Refinements

Enable quantification over refinements ...

222: {-@ maxInt :: forall <p :: Int -> Prop>. 
223:                 Int<p> -> Int<p> -> Int<p>  @-}
224: 
225: 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:Int -> x2:Int -> {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 

• max takes two Ints that satisfy p,
• max returns an Int that satisfies p.

Parametric Refinements

Enable quantification over refinements ...

245: {-@ maxInt :: forall <p :: Int -> Prop>. 
246:                 Int<p> -> Int<p> -> Int<p>  @-}
247: 
248: maxInt x y = if x <= y then y else x 

Parametric Refinements

264: {-@ maxInt :: forall <p :: Int -> Prop>. 
265:                 Int<p> -> Int<p> -> Int<p>  @-}
266: 
267: maxInt x y = if x <= y then y else x 

Check Implementation via SMT

Parametric Refinements

278: {-@ maxInt :: forall <p :: Int -> Prop>. 
279:                 Int<p> -> Int<p> -> Int<p>  @-}
280: 
281: maxInt x y = if x <= y then y else x 

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

299: {-@ maxInt :: forall <p :: Int -> Prop>. 
300:                 Int<p> -> Int<p> -> Int<p>  @-}
301: 
302: maxInt x y = if x <= y then y else x 

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

• When we call maxInt with args with some refinement,
• Then p instantiated with same refinement,
• Result of call will also have same concrete refinement.

331: {-@ o' :: Odd  @-}
332: {v : Int | ((v 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 
333: 
334: {-@ e' :: Even @-}
335: {v : Int | ((v 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 

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Strengthened Constructors
4. Abstract Refinements over Types