Refinement Types For Haskell

Ranjit Jhala, UCSD

We present LiquidHaskell, a dependent type-based verifier for Haskell. LiquidHaskell uses "Refinement types", a restricted form of dependent types where relationships between values are encoded by decorating types with logical predicates drawn from an efficiently SMT decidable theory (of arithmetic and uninterpreted functions.)

This talk will start with a quick overview of refinement types, SMT solver based (decidable) subtyping, and inference. Decidability is achieved by eschewing the use of arbitrary terms inside types, and the use of indices to encode rich properties of data.

Next, we will show how to recover some of the lost expressiveness with two new techniques: "measures" which encode computable properties of values and "abstract refinements" which enable generalization over invariants.

Finally, we will conclude by comparing refinements with other approaches, with a view towards stimulating discussion about identifying ways to combine the automation of the former with the expressiveness of the latter.