Programming Language designed for Program Synthesis with SMT-validation.
The curated LiquidHaskell tutorial ports
cover arithmetic, inductive datatypes, recursion, measures, FFI trust boundaries,
refinement inference, and diagnostics. They are ordinary .ae programs, not
a separate DSL or a Python implementation of the algorithms.
Advanced cases include polymorphic lists and Maybe, generic higher-order map with a dependent length contract, set-of-elements plus length measures, sorted-list insertion, and explicitly quantified abstract refinements. Each area has executable accepted cases and deliberately invalid controls.
The manifest records upstream files/symbols at a pinned revision (or the separately attributed official abstract-refinement article), adaptations, expected acceptance/rejection, and stable/experimental/research status. Positive programs run normally and with runtime verification. Negatives require the intended compiler error and source location; native cases distinguish static trust from checked execution.
uv run pytest tests/liquidhaskell_compatibility_test.py -q
This is a regression contract for selected semantic fragments, not Haskell source compatibility or complete LiquidHaskell parity. The suite README lists differences and excluded chapters, including monomorphic/specialized ports, constructor measure invariants, explicit metrics, unreachable branches, integer semantics, and FFI trust.