Refinement types for Haskell
- 19 August 2014
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 49 (9), 269-282
- https://doi.org/10.1145/2692915.2628161
Abstract
SMT-based checking of refinement types for call-by-value languages is a well-studied subject. Unfortunately, the classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking an expression, such systems implicitly assume that all the free variables in the expression are bound to values. This property is trivially guaranteed by eager, but does not hold under lazy, evaluation. Thus, to be sound and precise, a refinement type system for Haskell and the corresponding verification conditions must take into account which subset of binders actually reduces to values. We present a stratified type system that labels binders as potentially diverging or not, and that (circularly) uses refinement types to verify the labeling. We have implemented our system in LIQUIDHASKELL and present an experimental evaluation of our approach on more than 10,000 lines of widely used Haskell libraries. We show that LIQUIDHASKELL is able to prove 96% of all recursive functions terminating, while requiring a modest 1.7 lines of termination-annotations per 100 lines of code.Keywords
Funding Information
- Microsoft Research
- Division of Computing and Communication Foundations (CCF-1018672, CCF-1218344)
- Division of Computer and Network Systems (CNS-0964702, CNS-1223850)
This publication has 31 references indexed in Scilit:
- Refinement types for secure implementationsACM Transactions on Programming Languages and Systems, 2011
- Automated termination proofs for haskell by term rewritingACM Transactions on Programming Languages and Systems, 2011
- Hybrid type checkingACM Transactions on Programming Languages and Systems, 2010
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- General Recursion via Coinductive TypesLogical Methods in Computer Science, 2005
- Simplify: a theorem prover for program checkingJournal of the ACM, 2005
- Termination Analysis of the Untyped λ-CalculusLecture Notes in Computer Science, 2004
- Type-based termination of recursive definitionsMathematical Structures in Computer Science, 1999
- Subtypes for specifications: predicate subtyping in PVSIEEE Transactions on Software Engineering, 1998
- Procedures and parameters: An axiomatic approachLecture Notes in Mathematics, 1971