# Refinement Reflection:

## Simple Refinement Types

Refinement Types = Types + Predicates

## Example: Integers equal to 0

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

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

## Example: Natural Numbers

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

## Exercise: Positive Integers

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

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.

A. Farmer et al: Reasoning with the HERMIT

Can we express the above theorems in Liquid Haskell?

• Express & Prove Theorems in Haskell ...

## Types As Theorems

• Liquid Types express theorems, and

{-@ 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 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

Can we express them in Liquid Haskell?

• Express & Prove Theorems in Haskell...

## 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)

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 == 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

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

## 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

## 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

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

## 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

## Theorem Application

fib is monotonic!

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

## Application

Case Study: MapReduce: Program Properties that matter!