How to Safely Use Extensionality in Liquid Haskell

TL;DR

This paper addresses the challenges of applying extensionality in Liquid Haskell, introduces a new propositional equality called PEq to avoid unsoundness, and demonstrates its effectiveness through case studies and formal validation.

Contribution

It presents a novel approach to equality in Liquid Haskell with PEq, ensuring soundness while enabling higher-order reasoning.

Findings

PEq avoids unsoundness in extensionality proofs

PEq enables higher-type equalities in Liquid Haskell

Metatheory of PEq validated through case studies and formal proofs

Abstract

Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs to an optimized implementation that behaves the same. Without functional extensionality, proofs must relate functions that are fully applied. When data itself has a higher-order representation, fully applied proofs face serious impediments! When working with first-order data, fully applied proofs lead to noisome duplication when using higher-order functions. While dependent type theories are typically consistent with functional extensionality axioms, refinement type systems with semantic subtyping treat naive phrasings of functional extensionality inconsistently, leading to unsoundness. We demonstrate this unsoundness and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the unsoundness while still proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a small model and developing its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub `classy induction'.