Deriving Law-Abiding Instances

preprint
Authors
Affiliations

Ryan Scott

Indiana University, USA

Vikraman Choudhury

Indiana University, USA

Ryan Newton

Indiana University, USA

Niki Vazou

University of Maryland, USA

Ranjit Jhala

University of California at San Diego, USA

Published

January 1, 2017

Doi

10.48550/arXiv.1708.02328

Abstract

Liquid Haskell’s refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. But many of these proofs require routine, boilerplate code that is tedious to write. Moreover, many such proofs do not scale well, as the size of proof terms can grow superlinearly with the size of the datatypes involved in the proofs. We present a technique for programming with refinement reflection which solves this problem by leveraging datatype-generic programming. Our observation is that we can take any algebraic datatype, generate an equivalent representation type, and have Liquid Haskell automatically construct (and prove) an isomorphism between the original type and the representation type. This reduces many proofs down to easy theorems over simple algebraic “building block” types, allowing programmers to write generic proofs cheaply and cheerfully.

Back to top

Citation

BibTeX citation:
@misc{scott2017,
  author = {Scott, Ryan and Choudhury, Vikraman and Newton, Ryan and
    Vazou, Niki and Jhala, Ranjit},
  title = {Deriving {Law-Abiding} {Instances}},
  date = {2017},
  url = {https://doi.org/10.48550/arXiv.1708.02328},
  doi = {10.48550/arXiv.1708.02328},
  langid = {en},
  abstract = {Liquid Haskell’s refinement-reflection feature augments
    the Haskell language with theorem proving capabilities, allowing
    programmers to retrofit their existing code with proofs. But many of
    these proofs require routine, boilerplate code that is tedious to
    write. Moreover, many such proofs do not scale well, as the size of
    proof terms can grow superlinearly with the size of the datatypes
    involved in the proofs. We present a technique for programming with
    refinement reflection which solves this problem by leveraging
    datatype-generic programming. Our observation is that we can take
    any algebraic datatype, generate an equivalent representation type,
    and have Liquid Haskell automatically construct (and prove) an
    isomorphism between the original type and the representation type.
    This reduces many proofs down to easy theorems over simple algebraic
    “building block” types, allowing programmers to write generic proofs
    cheaply and cheerfully.}
}
For attribution, please cite this work as:
Scott, Ryan, Vikraman Choudhury, Ryan Newton, Niki Vazou, and Ranjit Jhala. 2017. “Deriving Law-Abiding Instances.” Preprint. https://doi.org/10.48550/arXiv.1708.02328.