Skip to content

Refinement Reflection on ADTs

Lists are Monoids

Previously we saw how Refinement Reflection can be used to write Haskell functions that prove theorems about other Haskell functions. Today, we will see how Refinement Reflection works on recursive data types. As an example, we will prove that lists are monoids (under nil and append).

Lets see how to express the monoid laws as liquid types, and then prove the laws by writing plain Haskell functions that are checked by LiquidHaskell.


Recursion
Recursive Paper and Pencil Proofs. "Drawing Hands" by Escher.

Lists

First, lets define the List a data type

66: data List a = N | C a (List a)

Induction on Lists

As we will see, proofs by structural induction will correspond to programs that perform recursion on lists. To keep things legit, we must verify that those programs are total and terminating.

To that end, lets define a length function that computes the natural number that is the size of a list.

81: {-@ measure length               @-}
82: {-@ length      :: List a -> Nat @-}
83: x1:(StructuralInduction.List a) -> {v : GHC.Types.Int | v >= 0
                                                        && v == length x1}length N        = 0
84: length (C x xs) = {v : GHC.Types.Int | v == (1 : int)}1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : GHC.Types.Int | v >= 0
                     && v == length xs
                     && v == length xs}length xs

We lift length in the logic, as a measure.

We can now tell Liquid Haskell that when proving termination on recursive functions with a list argument xs, it should check whether the length xs is decreasing.

94: {-@ data List [length] a = N | C {hd :: a, tl :: List a} @-}

Reflecting Lists into the Logic

To talk about lists in the logic, we use the annotation

104: {-@ LIQUID "--exact-data-cons" @-}

which automatically derives measures for

  • testing if a value has a given data constructor, and
  • extracting the corresponding field's value.

For our example, LH will automatically derive the following functions in the refinement logic.

116: isN :: L a -> Bool         -- Haskell's null
117: isC :: L a -> Bool         -- Haskell's not . null
118: 
119: select_C_1 :: L a -> a     -- Haskell's head
120: select_C_2 :: L a -> L a   -- Haskell's tail

A programmer never sees the above operators; they are internally used by LH to reflect Haskell functions into the refinement logic, as we shall see shortly.

Defining the Monoid Operators

A structure is a monoid, when it has two operators:

  • the identity element empty and
  • an associative operator <>.

Lets define these two operators for our List.

  • the identity element is the empty list, and
  • the associative operator <> is list append.
141: {-@ reflect empty @-}
142: empty  :: List a
143: {VV : (StructuralInduction.List a) | VV == empty
                                     && VV == StructuralInduction.N}empty  = N
144: 
145: {-@ infix   <> @-}
146: {-@ reflect <> @-}
147: (<>)           :: List a -> List a -> List a
148: N        x1:(StructuralInduction.List a) -> x2:(StructuralInduction.List a) -> {VV : (StructuralInduction.List a) | VV == <> x1 x2
                                                                                                           && VV == (if is_N x1 then x2 else StructuralInduction.C (select_C_1 x1) (<> (select_C_2 x1) x2))}<> (StructuralInduction.List a)ys = ys
149: (C x xs) <> ys = x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x ({VV : (StructuralInduction.List a) | VV == <> xs ys
                                     && VV == (if is_N xs then ys else StructuralInduction.C (select_C_1 xs) (<> (select_C_2 xs) ys))
                                     && VV == <> xs ys}xs <> ys)

LiquidHaskell automatically checked that the recursive (<>) is terminating, by checking that the length of its first argument is decreasing. Since both the above operators are provably terminating, LH lets us reflect them into logic.

As with our previous fibonacci example, reflection of a function into logic, means strengthening the result type of the function with its implementation.

Thus, the automatically derived, strengthened types for empty and (<>) will be

166: empty   :: {v:List a | v == empty && v == N }
167: 
168: (<>) :: xs:List a -> ys:List a
169:      -> {v:List a | v == xs <> ys &&
170:                     v == if isN xs then ys else
171:                          C (select_C_1 xs) (select_C_2 xs <> ys)
172:         }

In effect, the derived checker and selector functions are used to translate Haskell to logic. The above is just to explain how LH reasons about the operators; the programmer never (directly) reads or writes the operators isN or select_C_1 etc.

Proving the Monoid Laws

Finally, we have set everything up, (actually LiquidHaskell did most of the work for us) and we are ready to prove the monoid laws for the List.

First we prove left identity of empty.

190: {-@ leftId  :: x:List a -> { empty <> x == x } @-}
191: x1:(StructuralInduction.List a) -> {VV : () | <> empty x1 == x1}leftId (StructuralInduction.List a)x
192:    =   (StructuralInduction.List a)empty <> x
193:    (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. (StructuralInduction.List a)N <> x
194:    (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. x
195:    *** QED

This proof was trivial, because left identity is satisfied by the way we defined (<>).

Next, we prove right identity of empty.

204: {-@ rightId  :: x:List a -> { x <> empty  == x } @-}
205: x1:(StructuralInduction.List a) -> {VV : () | <> x1 empty == x1}rightId N
206:    =   (StructuralInduction.List (GHC.Prim.Any *))N <> empty
207:    (StructuralInduction.List (GHC.Prim.Any *)) -> (StructuralInduction.List (GHC.Prim.Any *)) -> (StructuralInduction.List (GHC.Prim.Any *))==. N
208:    *** QED
209: 
210: rightId (C x xs)
211:    =   (StructuralInduction.List a)(x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x xs) <> empty
212:    (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x ((StructuralInduction.List a)xs <> empty)
213:    (StructuralInduction.List a) -> (StructuralInduction.List a) -> () -> (StructuralInduction.List a)==. x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x xs         {VV : () | <> xs empty == xs}rightId xs
214:    *** QED

This proof is more tricky, as it requires structural induction which is encoded in LH proofs simply as recursion. LH ensures that the inductive hypothesis is appropriately applied by checking that the recursive proof is total and terminating. In the rightId case, for termination, Liquid Haskell checked that length xs < length (C x xs).

It turns out that we can prove lots of properties about lists using structural induction, encoded in Haskell as

  • case splitting,
  • recursive calls, and
  • rewriting,

To see a last example, lets prove the associativity of (<>).

233: {-@ associativity :: x:List a -> y:List a -> z:List a
234:                   -> { x <> (y <> z) == (x <> y) <> z } @-}
235: x1:(StructuralInduction.List a) -> x2:(StructuralInduction.List a) -> x3:(StructuralInduction.List a) -> {VV : () | <> x1 (<> x2 x3) == <> (<> x1 x2) x3}associativity N (StructuralInduction.List a)y (StructuralInduction.List a)z
236:   =   (StructuralInduction.List a)N <> ({v : (StructuralInduction.List a) | v == <> y z
                                    && v == (if is_N y then z else StructuralInduction.C (select_C_1 y) (<> (select_C_2 y) z))
                                    && v == <> y z}y <> z)
237:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. {v : (StructuralInduction.List a) | v == <> y z
                                    && v == (if is_N y then z else StructuralInduction.C (select_C_1 y) (<> (select_C_2 y) z))
                                    && v == <> y z}y <> z
238:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. (StructuralInduction.List a)((StructuralInduction.List a)N <> y) <> z
239:   *** QED
240: 
241: associativity (C x xs) y z
242:   =  (StructuralInduction.List a)(x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x xs) <> ({v : (StructuralInduction.List a) | v == <> y z
                                    && v == (if is_N y then z else StructuralInduction.C (select_C_1 y) (<> (select_C_2 y) z))
                                    && v == <> y z}y <> z)
243:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x ((StructuralInduction.List a)xs <> ({v : (StructuralInduction.List a) | v == <> y z
                                    && v == (if is_N y then z else StructuralInduction.C (select_C_1 y) (<> (select_C_2 y) z))
                                    && v == <> y z}y <> z))
244:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> () -> (StructuralInduction.List a)==. x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x ((StructuralInduction.List a)({v : (StructuralInduction.List a) | v == <> xs y
                                    && v == (if is_N xs then y else StructuralInduction.C (select_C_1 xs) (<> (select_C_2 xs) y))
                                    && v == <> xs y}xs <> y) <> z)  x1:(StructuralInduction.List a) -> x2:(StructuralInduction.List a) -> x3:(StructuralInduction.List a) -> {VV : () | <> x1 (<> x2 x3) == <> (<> x1 x2) x3}associativity xs y z
245:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. (StructuralInduction.List a)(x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x ({v : (StructuralInduction.List a) | v == <> xs y
                                    && v == (if is_N xs then y else StructuralInduction.C (select_C_1 xs) (<> (select_C_2 xs) y))
                                    && v == <> xs y}xs <> y)) <> z
246:   (StructuralInduction.List a) -> (StructuralInduction.List a) -> (StructuralInduction.List a)==. (StructuralInduction.List a)((StructuralInduction.List a)(x1:(StructuralInduction.List a) -> {v : (StructuralInduction.List a) | tl v == x1
                                                                       && hd v == x
                                                                       && select_C_2 v == x1
                                                                       && select_C_1 v == x
                                                                       && (is_C v <=> true)
                                                                       && (is_N v <=> false)
                                                                       && length v == 1 + length x1
                                                                       && v == StructuralInduction.C x x1}C x xs) <> y) <> z
247:   *** QED

The above proof of associativity reifies the paper and pencil proof by structural induction.

With that, we can safely conclude that our user defined list is a monoid!

Conclusion

We saw how Refinement Reflection can be used to

  • specify properties of ADTs,
  • naturally encode structural inductive proofs of these properties, and
  • have these proofs machine checked by Liquid Haskell.

Why is this useful? Because the theorems we prove refer to your Haskell functions! Thus you (or in the future, the compiler) can use properties like monoid or monad laws to optimize your Haskell code. In the future, we will present examples of code optimizations using monoid laws. Stay tuned!

Niki Vazou
2016-10-06