Refinement types for PureScript

Say what a function must return. Have it proved.

You write ordinary PureScript. A sibling .lps file refines the types of the functions you care about. lps verify proves the refinements hold — or hands you a counterexample. No compiler fork; it reads the CoreFn the compiler already emits and discharges its obligations with Z3.

Demo.purs — ordinary PureScript

module Demo where

abs :: Int -> Int
abs n = if n > 0 then n else 0 - n

bad :: Int -> Int
bad n = n - 1

Demo.lps — the refinement layer

type Nat = { v : Int | v >= 0 }

abs :: Int -> Nat

bad :: Int -> Nat

$ lps verify --output output Demo Demo.abs ✓ SAFE Demo.bad ✗ UNSAFE at src/Demo.purs:9:9 cannot prove: ((n - 1) >= 0) counterexample: n = 0

Both functions typecheck for the compiler. Only one satisfies its refinement — and when the tool disagrees, it says exactly why, at the exact span, with a value that breaks it.

22Functions proved SAFE

4Refuted with a counterexample

4Example modules

QF_LIADecidable logic — Z3 never guesses

01What refinement types buy you

A PureScript type says a function returns an Int. A refinement type says which Int: one that is >= 0, or a valid index into an array, or a MIDI-safe 0 <= v && v < 128. The invariants you would otherwise keep in comments, tests, or your head become part of the type — and get checked on every build.

The refinements live in a separate file, so your source stays ordinary PureScript that any toolchain compiles. Refine only the functions that matter; the rest are simply unchecked.

Precise, not just present

clamp lo hi x doesn't merely return an Int — it returns one in [lo, hi], and the spec carries the dependency between arguments:

clamp :: { lo : Int }
      -> { hi : Int | hi >= lo }
      -> Int
      -> { v : Int | v >= lo && v <= hi }

A counterexample, not a scolding

When a proof fails you get a concrete input that breaks the claim — the empty array for an index that assumed non-emptiness:

Arrays.badMid ✗ UNSAFE cannot prove: (len/2 >= 0) && (len/2 < length xs) counterexample: xs = []

02What it does not claim

Honesty is a feature. This verifies a fragment: first-order Int / Boolean / measured-data code.

Everything outside the fragment reports Unsupported, never a silent pass. Higher-order functions, type classes, and row-polymorphic records are roadmap, not shipped. And an assume spec is trusted, not checked — a stated axiom for imported or FFI functions, taken on faith and marked as such wherever it appears.

03Getting started

Requirements. purs 0.15.x, spago@next, node, and a z3 binary on the PATH.

make examples   # compile examples/ to CoreFn (spago backend trick)
make verify     # verify every example module that has a .lps spec
make test       # golden test — the verdict table on this site
make bundle     # standalone bin/lps.mjs (node, no spago needed)

Direct invocation over any spago project's build output:

lps verify     --output <dir> <ModuleName> [--spec <file.lps>]
               [--include <file.lps>]... [--smt2-dir <dir>]
lps verify-all --output <dir> [--include <file.lps>]... [--smt2-dir <dir>]

--include lib/prelude.lps prepends trusted specs for min / max / abs / signum / clamp on Int. --smt2-dir dumps every obligation as a replayable .smt2 artifact.