Copyright | (c) Joachim Breitner 2017 |
---|---|
License | MIT |
Maintainer | mail@joachim-breitner.de |
Portability | GHC specifc |
Safe Haskell | Safe |
Language | Haskell2010 |
GHC.Proof
Description
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 theOPTIONS_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
proof :: a -> a -> Proof Source #
Instructs the compiler to see if it can prove the two arguments to proof
to be equivalent.