GHC.Proof

This module supports the accompanying GHC plugin GHC.Proof.Plugin and adds to GHC the ability to verify simple program equations.

Synopis

Consider this module:

{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
module Simple where

import GHC.Proof
import Data.Maybe

my_proof1 :: (a -> b) -> Maybe a -> Proof
my_proof1 f x = isNothing (fmap f x)
            === isNothing x

my_proof2 :: a -> Maybe a -> Proof
my_proof2 d x = fromMaybe d x
            === maybe d id x

Compiling it will result in this output:

$ ghc Simple.hs
[1 of 1] Compiling Simple           ( Simple.hs, Simple.o )
GHC.Proof: Proving my_proof1 …
GHC.Proof: Proving my_proof2 …
GHC.Proof proved 2 equalities

Usage

To use this plugin, you have to

• Make sure you load the plugin GHC.Proof.Plugin, either by passing -fplugin GHC.Proof.Plugin to GHC or, more conveniently, using the OPTIONS_GHC pragma as above.
• Import the GHC.Proof module.

• Define proof obligations using the proof function or, equilvalently, the === operator. Type signatures are optional.

  These proof obligation must occur direclty on the right-hand side of a top-level definition, where all parameters (if any) are plain variables. For example, this would (currently) not work:

  not_good (f,x) = isNothing (fmap f x) === isNothing x

  If your module has an explicit export list, then these functions need to be exported (otherwise the compiler deletes them too quickly).

• Compile. If all proof obligations can be proven, compilation continues as usual; otherwise it aborts.

What can I prove this way?

Who knows... but generally you can only expect interesting results when you use functions that are either non-recursive, or have an extensive rewrite rule setup (such as lists). See the examples/ directory for some examples of what works.

Documentation

data Proof

A dummy data type, to give proof a nicely readable type signature.

Constructors

Proof

proof :: a -> a -> Proof

Instructs the compiler to see if it can prove the two arguments to proof to be equivalent.

(===) :: a -> a -> Proof infix 0

Infix operator for proof.

non_proof :: a -> a -> Proof

Instructs the compiler to try to prove the two arguments to proof to be equivalent, but do not abort if it fails.

This is useful to document equalities that you would like to be proven, but where ghc-proofs does not work well enough.

(=/=) :: a -> a -> Proof infix 0

Infix operator for non_proof.