Abstract Refinements

5: module AbstractRefinements where
6: 
7: import Prelude hiding (max)
8: import Language.Haskell.Liquid.Prelude
9: {-@ LIQUID "--no-termination" @-}

Polymorphic Max Function

Consinder a polymorphic max function:

15: max     :: a -> a -> a
16: max x y = if x >= y then x else y

We can instantiate a with Odd

22: max     :: Odd -> Odd -> Odd
23: 
24: maxOdd :: Odd
25: maxOdd = max 3 7

Polymorphic Max in Haskell

In Haskell the type of max is

32: max     :: Ord a => a -> a -> a

We could ignore the class constraints, and procced as before:

Instantiate a with Odd

41: max     :: Odd -> Odd -> Odd
42: 
43: maxOdd :: Odd
44: maxOdd = max 3 7

Polymorphic Add in Haskell

But this can lead to unsoundness:

52: max     :: Ord a => a -> a -> a
53: (+)     :: Num a => a -> a -> a

So, ignoring class constraints allows us to: instantiate a with Odd

60: (+)     :: Odd -> Odd -> Odd
61: 
62: addOdd :: Odd
63: addOdd = 3 + 7

Polymorphism via Parametric Invariants

max 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

86: {-@ max :: forall <p :: a -> Prop>. Ord a => a<p> -> a<p> -> a<p> @-}
87: max     :: Ord a => a -> a -> a
88: forall a <p :: a-> Bool>.
(GHC.Classes.Ord a) =>
{VV : a<p> | true} -> {VV : a<p> | true} -> {VV : a<p> | true}max {VV : a | ((papp1 p VV))}x {VV : a | ((papp1 p VV))}y = if {VV : a | ((papp1 p VV)) && (VV == x)}x x1:{VV : a | ((papp1 p VV))}
-> x2:{VV : a | ((papp1 p VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | ((papp1 p VV)) && (VV == y)}y then {VV : a | ((papp1 p VV)) && (VV == y)}y else {VV : a | ((papp1 p VV)) && (VV == x)}x

Where

a is just an abbreviation for {v:a | (p v)}

This type states explicitly:

For any property p, that is a property of a,
max takes two inputs of which satisfy p,
max returns an output that satisfies p.

Using Abstract Refinements

If we call max with two arguments 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.

120: {-@ type Odd = {v:Int | (v mod 2) = 1} @-}
121: 
122: {-@ maxOdd :: Odd @-}
123: maxOdd     :: Int
124: {VV : (GHC.Types.Int) | ((VV mod 2) == 1)}maxOdd     = {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}max {VV : (GHC.Types.Int) | (VV == (3  :  int))}3 {VV : (GHC.Types.Int) | (VV == (5  :  int))}5

Abstract Refinements in Type Constructors

Types cannot track information of monomorphic arguments:

134: data F = F {{VV : (AbstractRefinements.F) | false}
-> {VV : (GHC.Types.Int) | false}w::Int}

The type F cannot give us information about the field x.

142: forall a. {VV : a | false} -> {VV : a | false}foo = let (AbstractRefinements.F)f = (GHC.Types.Int) -> (AbstractRefinements.F)F {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 in -- :: f :: F
143:       case {VV : (AbstractRefinements.F) | (VV == f)}f of 
144:       F x -> {VV : (GHC.Types.Bool) | ((Prop VV))}
-> {VV : a | false} -> {VV : a | false}liquidAssert ({VV : (GHC.Types.Int) | (VV == x)}x x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)

Abstract Refinements in Type Constructors

Abstract over the refinement you care

152: data G = G {{VV : (AbstractRefinements.G <false>) | false}
-> {VV : (GHC.Types.Int) | false}y::Int{- <p> -}}

Move it to the left-hand side

157: {-@ data G <p :: Int -> Prop> = G (y::Int<p>) @-}

The type G  now describes the field x.

163: forall a. {VV : a | false} -> {VV : a | false}bar = let (AbstractRefinements.G <(VV == 0) && (VV /= AbstractRefinements.maxOdd)>)f = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true} -> (AbstractRefinements.G <p>)G {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 in -- :: f :: G <{v = 0}>
164:       case {VV : (AbstractRefinements.G <(VV == 0) && (VV /= AbstractRefinements.maxOdd)>) | (VV == f)}f of 
165:       G x -> {VV : (GHC.Types.Bool) | ((Prop VV))}
-> {VV : a | false} -> {VV : a | false}liquidAssert ({VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}x x1:{VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}
-> x2:{VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)

Abstract Refinements in Lists

Remember increasing Lists?

172: data IL a = N | C (x :: a) (xs :: L {v:a | x <= v})

Abstract over the refinement you care

177: data L a = N | C {forall a.
{VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}
-> {VV : a | false}x :: a, forall a.
{VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}
-> {VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}xs :: L a {- v:a | p v x -}}

Move it to the left-hand side

182: {-@ data L a <p :: a -> a -> Prop> = 
183:       N 
184:     | C (x :: a) (xs :: L <p> a<p x>)  @-}

We can get back increasing Lists:

191: {-@ type IncrL a = L <{\x v -> x <= v}> a @-}

Multiple Instantiations

Now increasing lists

199: type IncrL a = L <{\x v -> x <= v}> a

Co-exist with decreasing ones

205: type DecrL a = L <{\x v -> x >= v}> a