# Abstract Refinements

```7: module AbstractRefinements where
```

# Abstract Refinements

Consider the following function
```17: maxInt     :: Int -> Int -> Int
18: maxInt x y = if x <= y then y else x
```

We can give `maxInt` many (incomparable) refinement types:
```24: maxInt :: Nat -> Nat -> Nat
25:
26: maxInt :: Even -> Even -> Even
27:
28: maxInt :: Prime -> Prime -> Prime
```

But which is the right type?

# Parametric Invariants

`maxInt` returns one of its two inputs `x` and `y`.

• If both inputs satisfy a property

• Then output must satisfy that property

This holds, regardless of what that property was!

• That is, we can abstract over refinements

• Or, parameterize a type over its refinements.

# Parametric Invariants

```53: {-@ maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p> @-}
54: maxInt     :: Int -> Int -> Int
55: forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | ((papp1 p VV))}x {VV : (GHC.Types.Int) | ((papp1 p VV))}y = if {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == x)}x x:{VV : (GHC.Types.Int) | ((papp1 p VV))}
-> y:{VV : (GHC.Types.Int) | ((papp1 p VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == y)}y then {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == y)}y else {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == x)}x
```

Where

• `Int<p>` is just an abbreviation for `{v:Int | (p v)}`

This type states explicitly:

• For any property `p`, that is a property of `Int`,

• `maxInt` takes two inputs of which satisfy `p`,

• `maxInt` returns an output that satisfies `p`.

# Parametric Invariants via Abstract Refinements

We type `maxInt` as
```78: maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p>
```

We call `p` an an abstract refinement

In the refinement logic,

• abstract refinements are uninterpreted function symbols

• which (only) satisfy the congruence axiom: forall x, y. x = y => (p x) = (p y)

# Using Abstract Refinements

• If we call `maxInt` with two `Int`s with the same concrete refinement,

• Then the `p` will be instantiated with that concrete refinement,

• The output of the call will also enjoy the concrete refinement.

For example, the refinement is instantiated with `\v -> v >= 0`

```104: {-@ maxNat :: Nat @-}
105: maxNat     :: Int
106: {VV : (GHC.Types.Int) | (VV >= 0)}maxNat     = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | (VV == (2  :  int))}2 {VV : (GHC.Types.Int) | (VV == (5  :  int))}5
```

# Using Abstract Refinements

• If we call `maxInt` with two `Int`s with the same concrete refinement,

• Then the `p` will be instantiated with that concrete refinement,

• The output of the call will also enjoy the concrete refinement.

Or any other property

```121: {-@ type RGB = {v: Int | ((0 <= v) && (v < 256)) } @-}
```

to verify

```127: {-@ maxRGB :: RGB @-}
128: maxRGB     :: Int
129: {VV : (GHC.Types.Int) | (VV < 256) && (0 <= VV)}maxRGB     = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | (VV == (56  :  int))}56 {VV : (GHC.Types.Int) | (VV == (8  :  int))}8
```