# Haskell as a Theorem Prover

We've taught LiquidHaskell a new trick that we call ``Refinement Reflection'' which lets us turn Haskell into a theorem prover capable of proving arbitrary properties of code. The key idea is to reflect the code of the function into its output type, which lets us then reason about the function at the (refinement) type level. Lets see how to use refinement types to express a theorem, for example that fibonacci is a monotonically increasing function, then write plain Haskell code to reify a paper-and-pencil-style proof for that theorem, that can be machine checked by LiquidHaskell.

## Shallow vs. Deep Specifications¶

Up to now, we have been using Liquid Haskell to specify and verify "shallow" specifications that abstractly describe the behavior of functions. For example, below, we specify and verify that `fib`restricted to natural numbers, always terminates returning a natural number.

```70: {-@ fib :: i:Nat -> Nat / [i] @-}
71: {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib {v : GHC.Types.Int | v >= 0}i | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0    = 0
72:       | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1    = 1
73:       | otherwise = {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
```

In this post we present how refinement reflection is used to verify "deep" specifications that use the exact definition of Haskell functions. For example, we will prove that the Haskell `fib` function is increasing.

## Propositions¶

To begin with, we import ProofCombinators, a (Liquid) Haskell library that defines and manipulates logical proofs.

```89: import Language.Haskell.Liquid.ProofCombinators
```

A `Proof` is a data type that carries no run time information

```95: type Proof = ()
```

but can be refined with desired logical propositions. For example, the following type states that `1 + 1 == 2`

```102: {-@ type OnePlusOne = {v: Proof | 1 + 1 == 2} @-}
```

Since the `v` and `Proof` are irrelevant, we may as well abbreviate the above to

```109: {-@ type OnePlusOne' = { 1 + 1 == 2 } @-}
```

As another example, the following function type declares that for each `x` and `y` the plus operator commutes.

```117: {-@ type PlusComm = x:Int -> y:Int -> {x + y == y + x} @-}
```

## Trivial Proofs¶

We prove the above theorems using Haskell programs. The `ProofCombinators` module defines the `trivial` proof

```129: trivial :: Proof
130: trivial = ()
```

and the "casting" operator `(***)` that makes proof terms look nice:

```137: data QED = QED
138:
139: (***) :: a -> QED -> Proof
140: _ *** _ = ()
```

Using the underlying SMT's knowledge on linear arithmetic, we can trivially prove the above propositions.

```147: {-@ propOnePlueOne :: _ -> OnePlusOne @-}
148: () -> {VV : () | 1 + 1 == 2}propOnePlueOne _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
149:
150: {-@ propPlusComm :: PlusComm @-}
151: x1:GHC.Types.Int -> x2:GHC.Types.Int -> {VV : () | x1 + x2 == x2 + x1}propPlusComm _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
```

We saw how we use SMT's knowledge on linear arithmetic to trivially prove arithmetic properties. But how can we prove ``deep'' properties on Haskell's functions?

## Refinement Reflection¶

Refinement Reflection allows deep specification and verification by reflecting the code implementing a Haskell function into the function’s output refinement type.

Refinement Reflection proceeds in 3 steps: definition, reflection, and application. Consider reflecting the definition of `fib` into the logic

```171: {-@ reflect fib @-}
```

then the following three reflection steps will occur.

## Step 1: Definition¶

Reflection of the Haskell function `fib` defines in logic an uninterpreted function `fib` that satisfies the congruence axiom.

In the logic the function `fib` is defined.

```185: fib :: Int -> Int
```

SMT only knows that `fib` satisfies the congruence axiom.

```191: {-@ fibCongruence :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-}
192: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 == x2 => fib x1 == fib x2}fibCongruence _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
```

Other than congruence, SMT knowns nothing for the function `fib`, until reflection happens!

## Step 2: Reflection¶

As a second step, Liquid Haskell connects the Haskell function `fib` with the homonymous logical function, by reflecting the implementation of `fib` in its result type.

The result type of `fib` is automatically strengthened to the following.

```210: fib :: i:Nat -> {v:Nat | v == fib i && v = fibP i }
```

That is, the result satisfies the `fibP` predicate exactly reflecting the implementation of `fib`.

```217: fibP i = if i == 0 then 0 else
218:          if i == 1 then 1 else
219:          fin (i-1) + fib (i-2)
```

## Step 3: Application¶

With the reflected refinement type, each application of `fib` automatically unfolds the definition of `fib` once. As an example, applying `fib` to `0`, `1`, and `2` allows us to prove that `fib 2 == 1`:

```231: {-@ fibTwo :: _ -> { fib 2 == 1 } @-}
232: () -> {VV : () | fib 2 == 1}fibTwo _ = {v : [GHC.Types.Int] | null v <=> false}[{v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2] *** QED
```

Though valid, the above `fibTwo` proof is not pretty!

## Structuring Proofs¶

To make our proofs look nice, we use combinators from the `ProofCombinators` library, which exports a family of operators `(*.)` where `*` comes from the theory of linear arithmetic and the refinement type of `x *. y`

• requires that `x *. y` holds and
• ensures that the returned value is equal to `x`.

For example, `(==.)` and `(<=.)` are predefined in `ProofCombinators` as

```252: (==.) :: x:a -> y:{a| x==y} -> {v:a| v==x}
253: x ==. _ = x
254:
255: (<=.) :: x:a -> y:{a| x<=y} -> {v:a| v==x}
256: x <=. _ = x
```

Using these predefined operators, we construct paper and pencil-like proofs for the `fib` function.

```263: {-@ fibTwoPretty :: { fib 2 == 1 } @-}
264: {VV : () | fib 2 == 1}fibTwoPretty
265:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2
266:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0
267:   *** QED
```

## Because operator¶

To allow the reuse of existing proofs, `ProofCombinators` defines the because operator `(∵)`

```279: (∵) :: (Proof -> a) -> Proof -> a
280: f ∵ y = f y
```

For example, `fib 3 == 2` holds because `fib 2 == 1`:

```286: {-@ fibThree :: _ -> { fib 3 == 2 } @-}
287: () -> {VV : () | fib 3 == 2}fibThree _
288:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 3
289:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1
290:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int==. GHC.Types.Int1     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1      ∵ fibTwoPretty
291:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. 2
292:   *** QED
```

## Proofs by Induction (i.e. Recursion)¶

Next, combining the above operators we specify and prove that `fib` is increasing, that is for each natural number `i`, `fib i <= fib (i+1)`.

We specify the theorem as a refinement type for `fubUp` and use Haskell code to persuade Liquid Haskell that the theorem holds.

```309: {-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-}
310: x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp {v : GHC.Types.Int | v >= 0}i
311:   | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0
312:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1
313:   *** QED
314:
315:   | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1
316:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2
317:   *** QED
318:
319:   | otherwise
320:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i
321:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
322:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2) ∵ x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
323:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) ∵ x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
324:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+1)
325:   *** QED
```

The proof proceeds by induction on `i`.

• The base cases `i == 0` and `i == 1` are represented as Haskell's case splitting.

• The inductive hypothesis is represented by recursive calls on smaller inputs.

Finally, the SMT solves arithmetic reasoning to conclude the proof.

## Higher Order Theorems¶

Refinement Reflection can be used to express and verify higher order theorems! For example, `fMono` specifies that each locally increasing function is monotonic!

```345: {-@ fMono :: f:(Nat -> Int)
346:           -> fUp:(z:Nat -> {f z <= f (z+1)})
347:           -> x:Nat
348:           -> y:{Nat|x < y}
349:           -> {f x <= f y} / [y]
350:   @-}
351: x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : GHC.Types.Int | v >= 0} -> GHC.Types.Intf x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | f x1 <= f (x1 + 1)}thm {v : GHC.Types.Int | v >= 0}x {v : GHC.Types.Int | v >= 0
&& x < v}y
352:   | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== y
353:   = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1)
354:          GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int>. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x       ∵ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x
355:         *** QED
356:
357:   | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 < x2}< y
358:   = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x
359:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<.  {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)         ∵ x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
360:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<.  {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y             ∵ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
361:   *** QED
```

Again, the recursive implementation of `fMono` depicts the paper and pencil proof of `fMono` by induction on the decreasing argument `/ [y]`.

Since `fib` is proven to be locally increasing by `fUp`, we use `fMono` to prove that `fib` is monotonic.

```371: {-@ fibMono :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m} @-}
372: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0
&& x1 < v} -> {VV : () | fib x1 <= fib x2}fibMono = {v : x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {v : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {v : () | x1 x5 <= x1 x6} | v == RefinementReflection.fMono}fMono {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | fib x1 <= fib (x1 + 1)} | v == RefinementReflection.fibUp}fibUp
```

## Conclusion¶

We saw how refinement reflection turns Haskell into a theorem prover by reflecting the code implementing a Haskell function into the function’s output refinement type.

Refinement Types are used to express theorems, Haskell code is used to prove such theorems expressing paper pencil proofs, and Liquid Haskell verifies the validity of the proofs!

Proving `fib` monotonic is great, but this is Haskell! Wouldn’t it be nice to prove theorems about inductive data types and higher order functions? Like fusions and folds? Or program equivalence on run-time optimizations like map-reduce?

Stay tuned!

Even better, if you happen you be in Nara for ICFP'16, come to my CUFP tutorial for more!

Niki Vazou
2016-09-18