Catch: Case Totality Checker for Haskell
A Haskell program may fail at runtime with a pattern-match error if the program has any incomplete (non-exhaustive) patterns in definitions or case alternatives. The Catch tool is a static checker that allows non-exhaustive patterns to exist, yet ensures that a pattern-match error does not occur.
Unfortunately version incompatiblities mean that currently its very difficult to get Catch to compile. Hopefully at some point Catch can be ported to work on GHC Core, and Catch can be used on any programs which are compiled by GHC.
The following programs and libraries have all had some of their source code verified by Catch. If you verify a released Haskell project with Catch, please let me know your experiences. To indicate that you have taken the time to ensure pattern match safety, you may use the following "Checked with Catch" logo.
- XMonad - the StackSet module has been verified several times, as the design changes - see this blog post for the first instance.
- System.FilePath - see this blog post.
- Data.FiniteMap - see the Haskell Symposium 2008 paper.
- HsColour - see the Haskell Symposium 2008 paper.
- ESC/Haskell, by Dana Xu - explicit pre/post condition annotations.
- Non-empty lists - moving the safety into the types.
- darcs get --lazy http://community.haskell.org/~ndm/darcs/catch
- Related blog posts
- Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching - from Haskell Symposium 2008 (abstract) (bibtex)
- Detecting Pattern-Match Failures in Haskell - from The Oxford Centre for Metacomputation (bibtex)
- A Static Checker for Safe Pattern Matching in Haskell - from TFP 2005 post proceedings (abstract) (bibtex)
- Catch, A Practical Tool - from BCTCS 2006 (bibtex)
- Unfailing Haskell: A Static Checker for Pattern Matching - from TFP 2005 (abstract) (bibtex)