Catch: Case Totality Checker for Haskell
This is my primary PhD topic. An initial version was presented at TFP 2005.
Abstract
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. This paper describes a static checker that allows non-exhaustive patterns to exist, yet ensures that a pattern-match error does not occur. It describes a constraint language that can be used to reason about pattern matches, along with mechanisms to propagate these constraints between program components. The checker can handle some higher-order functions.
Users
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.
- Safe
- Data.FiniteMap - see the forthcoming paper.
- HsColour - see the forthcoming paper.
Credits
The name is courtesy of Mike Dodds.
Related work
- ESC/Haskell, by Dana Xu - explicit pre/post condition annotations.
- Non-empty lists - moving the safety into the types.
Downloads
- darcs get --partial http://www.cs.york.ac.uk/fp/darcs/catch
- Catch: A User Manual - a manual
- Released version 0.1.1
- Related Blog posts
- Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching - awaiting revision
- A Static Checker for Safe Pattern Matching in Haskell - An overview of pattern match checking
- Unfailing Haskell: A static checker for pattern matching - written with Colin Runciman
- Unfailing Haskell - my Qualifying disseration