Refinement Reflection:

or, how to turn Haskell into a Theorem Prover



Niki Vazou

(UC San Diego)














Simple Refinement Types


Refinement Types = Types + Predicates













Example: Integers equal to 0


{-@ type Zero = {v:Int | v = 0} @-}
{-@ zero :: Zero @-}
zero     =  0
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Refinement types via special comments {-@ ... @-}













Example: Natural Numbers


{-@ type Nat = {v:Int | 0 <= v} @-}
{-@ nats :: [Nat]               @-}
nats     =  [0, 1, 2, 3]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














Exercise: Positive Integers


{-@ type Pos = {v:Int | 0 <= v} @-}
{-@ poss :: [Pos]               @-}
poss     =  [0, 1, 2, 3]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: First, can you fix Pos so poss is rejected?


Q: Next, can you modify poss so it is accepted?













Type Checking

{-@ type Pos = {v:Int | 0 < v} @-}

{-@ poss :: [Pos]               @-}
poss     =  [1, 2, 3]


Type Checking Via Implication Checking. 

v = 1 => 0 < v 
v = 2 => 0 < v 
v = 3 => 0 < v













SMTs to Automate Type Checking


{-@ type Pos = {v:Int | 0 < v} @-}


Refinements Drawn from Decidable logics.


For automatic, decidable (and thus predictable) SMT type checking.











Refinement Reflection



Goal: Arbitrary (terminating) Haskell expressions into refinements, ...


... while preserving decidable type checking.















Theorems about Haskell functions


A. Farmer et al: Reasoning with the HERMIT

Hermit Laws


















Theorems about Haskell functions




Can we express the above theorems 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 _ = ()
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















Make the theorems even prettier!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


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


















Use more SMT knowledge


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


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


















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:Int -> Int @-}
fib i | i == 0    = 0 
      | i == 1    = 1 
      | otherwise = fib (i-1) + fib (i-2)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


... and nothing else


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
















Reflection at Result Type


The type of fib connects logic & Haskell implementation 

fib :: i:Nat 
    -> {v:Nat |  v == fib i 
              && v == 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 _ = let f1 = fib 1 -- f1:: {f1 == fib 1 && f1 == 1} 
          in [f1] *** QED 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX



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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















Paper & Pencil style 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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















Another Paper & Pencil like Proof

Can you fix the prove that fib is monotonic?

{-@ fibMonotonic :: x:Nat -> y:{Nat | x < y }  
     -> {fib x <= fib y}  @-}
fibMonotonic x y 
  | y == x + 1 
  =   fib x 
  <=. fib (x+1) ? fibUp x 
  <=. fib y 
  *** QED  
  | x < y - 1 
  =   fib x 
  <=. fib (y-1) 
  <=. fib y     ? fibUp (y-1) 
  *** QED   
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX



Note: Totality checker should be on for valid proofs
{-@ LIQUID "--totality"        @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX






















Generalizing monotonicity proof

Increasing implies monotonic in general!

{-@ 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 x   <=. f (x + 1) ? fUp x
          ==. f y       
          *** QED
  | x + 1 < y
  = f x   <=. f (y-1)   ? fMono f fUp x (y-1)
          <=. f y       ? fUp (y-1)
          *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


















Theorem Application



fib is monotonic!

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


















Application



Case Study: MapReduce: Program Properties that matter!