Refinement Reflection



Allow terminating Haskell functions into the logic!















Theorems about Haskell functions


A. Farmer et al: Reasoning with the HERMIT

Hermit Laws


















Theorems about Haskell functions




Can we express them in Liquid Haskell?

  • Express & Prove Theorems in Haskell ...
  • ... for Haskell functions.












Types As Theorems


  • Liquid Types express theorems, and

  • Haskell functions express proofs.


{-@ onePlusOne :: () -> {v:() | 1 + 1 == 2 } @-} onePlusOne _ = ()


















Make the theorems pretty!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


-- import Language.Haskell.Liquid.ProofCombinators {-@ propOnePlusOne :: () -> {v: Proof | 1 + 1 == 2} @-} propOnePlusOne _ = trivial


















Make the theorems even prettier!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propOnePlusOne' :: _ -> { 1 + 1 == 2 } @-} propOnePlusOne' _ = trivial *** QED


















Use all the underlying logic


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propPlusAccum :: x:Int -> y:Int -> { x + y == y + x } @-} propPlusAccum _ _ = trivial *** QED


















Theorems about Haskell functions




Can we express them in Liquid Haskell?

  • Express & Prove Theorems in Haskell...
  • ... for Haskell functions.












Refinement Reflection


Reflect terminating fib in the logic.

{-@ reflect fib @-} {-@ fib :: i:Nat -> Nat @-} fib i | i == 0 = 0 | i == 1 = 1 | otherwise = fib (i-1) + fib (i-2)


Now fib can live in the Liquid Types!
















fib is an uninterpreted function


For which logic only knows the congruence axiom...

{-@ fibCongr :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-} fibCongr _ _ = trivial *** QED


... and nothing else


{-@ fibOne :: () -> {fib 1 == 1 } @-} fibOne _ = trivial *** QED
















Reflection at Result Type


The type of fib connects logic & Haskell implementation 

fib :: i:Nat -> {v:Nat | v == fib i && v == propFib i}

propFib i = if i == 0 then 0 else   
            if i == 1 then 1 else 
            fib (i-1) + fib (i-2)



Calling fib i reveals its implementation into the logic!














Reflection at Result Type



{-@ fibEq :: () -> {fib 1 == 1 } @-} fibEq _ = [fib 1] *** QED



Q: Can you prove that fib 2 == 1?














Structuring Proofs



Using combinators from ProofCombinators!



{-@ fibTwo :: _ -> { fib 2 == 1 } @-} fibTwo _ = fib 2 ==. fib 1 + fib 0 *** QED


















Reusing Proofs: The because operator



Using combinators from ProofCombinators!



{-@ fibThree :: _ -> { fib 3 == 2 } @-} fibThree _ = fib 3 ==. fib 2 + fib 1 ==. 1 + 1 ∵ fibTwo () ==. 2 *** QED


















Pencil & Paper like Proofs

fib is increasing

{-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-} fibUp i | i == 0 = fib 0 <. fib 1 *** QED | i == 1 = fib 1 <=. fib 1 + fib 0 <=. fib 2 *** QED | otherwise = fib i ==. fib (i-1) + fib (i-2) <=. fib i + fib (i-2) ∵ fibUp (i-1) <=. fib i + fib (i-1) ∵ fibUp (i-2) <=. fib (i+1) *** QED


















Higher Order Theorems

Increasing implies monotonic!

{-@ fMono :: f:(Nat -> Int) -> fUp:(z:Nat -> {f z <= f (z+1)}) -> x:Nat -> y:{Nat|x < y} -> {f x <= f y} / [y] @-} fMono f fUp x y | x + 1 == y = f y ==. f (x + 1) >. f x ∵ fUp x *** QED | x + 1 < y = f x <. f (y-1) ∵ fMono f fUp x (y-1) <. f y ∵ fUp (y-1) *** QED


















Theorem Application



fib is monotonic!

{-@ fibMono :: n:Nat -> m:{Nat | n < m } -> {fib n <= fib m} @-} fibMono = fMono fib fibUp


















Recap



  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data
  4. Termination: Use Logic to Prove Termination
  5. Reflection: Allow Haskell functions in Logic!


Next: Case study: MapReduce: Program Properties that matter!