Abstract Refinements
Two Problems
Problem 1:
How to specify increasing and decreasing lists?
Problem 2:
How to specify iteration-dependence in higher-order functions?
Problem Is Pervasive
Lets distill it to a simple example...
(First, a few aliases)
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 Int
s:
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
Oh no! 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 properties over types
Parametric Refinements
Enable quantification over refinements ...
Type says: for any p
that is a property of Int
,
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
Key idea: Int<p>
is just \(\reft{v}{\Int}{p(v)}\)
Abstract Refinement is uninterpreted function in SMT logic
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.
Infer Instantiation by Liquid Typing
At call-site, instantiate
p
with unknown
\(\kvar{p}\) and solve!
Recap
- Refinements: Types + Predicates
- Subtyping: SMT Implication
- Measures: Strengthened Constructors
- Abstract Refinements over Types
Abstract Refinements are
very expressive ...
[continue]