# Abstract Refinements

## Two Problems

Problem 1:

How do we specify both increasing and decreasing lists?

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)

```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 ...

```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
```

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 ...

```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   `{v:Int | (p v)}`

i.e., Abstract Refinement is an uninterpreted function in SMT logic

## Parametric Refinements

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

Check and Instantiate

## 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.
```288: {-@ o' :: Odd  @-}
289: {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
290:
291: {-@ e' :: Even @-}
292: {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
```

## Using Abstract Refinements

Or any other property ...

```307: {-@ type RGB = {v:_ | (0 <= v && v < 256)} @-}
308:
309: {-@ rgb :: RGB @-}
310: {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   -- p := \v -> 0 <= v < 256
```

## Recap

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

Abstract Refinements are very expressive ... [continue]