Deriving Law-Abiding Instances

TL;DR

This paper introduces a datatype-generic programming technique for Liquid Haskell's refinement reflection, enabling automatic proof generation and reducing boilerplate and proof complexity in verifying algebraic datatypes.

Contribution

It presents a novel approach leveraging datatype-generic programming to automate and simplify proofs in Liquid Haskell, improving scalability and reducing manual effort.

Findings

Automated proof generation for algebraic datatypes.

Reduction of proof complexity through datatype isomorphisms.

Enhanced scalability of proofs in Liquid Haskell.

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.