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.

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

• Released version
  • Catch: A User Manual (bibtex)(hide bibtex)
    @manual{mitchell:catch_manual
        ,title          = "Catch: A User Manual"
        ,author         = "Neil Mitchell"
        ,url            = "\verb'http://www.cs.york.ac.uk/fp/darcs/catch/catch.htm'"
    }
    
  • darcs get --partial http://www.cs.york.ac.uk/fp/darcs/catch
  • Bug tracker
• Related blog posts
• Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching - from Haskell Symposium 2008 (abstract)(hide abstract)
  We describe an automated analysis of Haskell 98 programs to check statically that, despite the possible use of partial (or nonexhaustive) pattern matching, no pattern-match failure can occur. Our method is an iterative backward analysis using a novel form of pattern-constraint to represent sets of data values. The analysis is defined for a core first-order language to which Haskell 98 programs are reduced. Our analysis tool has been successfully applied to a range of programs, and our techniques seem to scale well. Throughout the paper, methods are represented much as we have implemented them in practice, again in Haskell.
  (bibtex)(hide bibtex)
  @inproceedings{mitchell:catch_2008_9_25
      ,title          = "Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching"
      ,author         = "Neil Mitchell and Colin Runciman"
      ,year           = "2008"
      ,month          = "September"
      ,day            = "25"
      ,booktitle      = "Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell"
      ,pages          = "49--60
      ,location       = "Victoria, BC, Canada"
      ,doi            = "http://doi.acm.org/10.1145/1411286.1411293"
      ,publisher      = "ACM"
      ,isbn           = "978-1-60558-064-7"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/paper-not_all_patterns_but_enough-25_sep_2008.pdf'"
  }
  
  • Not All Patterns, But Enough - from Haskell Symposium 2008
  • Not All Patterns, But Enough
• Detecting Pattern-Match Failures in Haskell - from The Oxford Centre for Metacomputation (bibtex)(hide bibtex)
  @misc{mitchell:catch_2007_11_26
      ,title          = "Detecting Pattern-Match Failures in {Haskell}"
      ,author         = "Neil Mitchell"
      ,year           = "2007"
      ,month          = "November"
      ,day            = "26"
      ,note           = "Presentation from The Oxford Centre for Metacomputation"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-detecting_pattern_match_failures_in_haskell-26_nov_2007.pdf'"
  }
  
• A Static Checker for Safe Pattern Matching in Haskell - from TFP 2005 post proceedings (abstract)(hide 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.
  (bibtex)(hide bibtex)
  @inproceedings{mitchell:catch_2007_2_1
      ,title          = "A Static Checker for Safe Pattern Matching in {Haskell}"
      ,author         = "Neil Mitchell and Colin Runciman"
      ,year           = "2007"
      ,month          = "February"
      ,day            = "1"
      ,publisher      = "Intellect"
      ,booktitle      = "Trends in Functional Programming"
      ,volume         = "6"
      ,isbn           = "978-1-84150-176-5"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/paper-a_static_checker_for_safe_pattern_matching_in_haskell-01_feb_2007.pdf'"
  }
  
• Catch, A Practical Tool - from BCTCS 2006 (bibtex)(hide bibtex)
  @misc{mitchell:catch_2006_4_6
      ,title          = "Catch, A Practical Tool"
      ,author         = "Neil Mitchell"
      ,year           = "2006"
      ,month          = "April"
      ,day            = "6"
      ,note           = "Presentation from BCTCS 2006"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-catch-06_apr_2006.pdf'"
  }
  
• Unfailing Haskell: A Static Checker for Pattern Matching - from TFP 2005 (abstract)(hide 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.
  (bibtex)(hide bibtex)
  @inproceedings{mitchell:catch_2005_9_24
      ,title          = "Unfailing {Haskell}: A Static Checker for Pattern Matching"
      ,author         = "Neil Mitchell and Colin Runciman"
      ,year           = "2005"
      ,month          = "September"
      ,day            = "24"
      ,booktitle      = "Proceedings of the Sixth Symposium on Trends in Functional Programming"
      ,pages          = "313--328
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/paper-unfailing_haskell_a_static_checker_for_pattern_matching-24_sep_2005.pdf'"
  }
  
  • Unfailing Haskell: A Static Checker for Pattern Matching - from TFP 2005

Tags: haskell phd popular program tags yhc