TypedRedex is a Haskell library for defining Redex-style judgments, reduction rules, and semantic relations as a typed AST.
The pitch is simple:
- the Redex workflow, but embedded in Haskell
- rules represented as a typed AST
- multiple interpreters over the same rule definition
- better failure information when a derivation gets stuck
A more motivating introduction can be found on this slides .
PLT Redex is a great environment for prototyping programming-language semantics, but in practice some common pain points remain:
- many mistakes are discovered only at runtime
- arity, mode, and contract issues are easy to encode accidentally
- failures can collapse to "no answers", it can be hard to inspect where a derivation stopped
TypedRedex keeps the same general workflow while leaning on Haskell's type system and tooling.
TypedRedex provides:
- typed judgments with type-level names, modes, and argument types
- reusable interpreters over the same rule AST
- partial derivation trees for failed queries
- mode checking for scheduling and output-discipline issues
- customizable rule rendering for papers and notes
- nominal support for binders and freshness constraints
- natural integration with QuickCheck and ordinary Haskell code
A typical workflow looks like this:
- Define object-language syntax as ordinary Haskell data types.
- Define judgments and rules with
TypedRedex.DSL. - Build queries with fresh logic variables.
- Choose an interpreter depending on whether you want answers, traces, typeset rules, or mode analysis.
The STLC example in this repository defines typing as a typed judgment:
typeof :: Judgment "typeof" '[I, I, O] '[Env, Tm, Ty]
typeof = judgment $
format (\env tm ty -> env <+> " ⊢ " <+> tm <+> " : " <+> ty)
>> rules
[ rule "T-Var" $ do
(env, x, ty) <- fresh
prem $ lookupVar env x ty
concl $ typeof env (var x) ty
, rule "T-Abs" $ do
(env, x, tyA, body, tyB) <- fresh
prem $ typeof (ebind x tyA env) body tyB
concl $ typeof env (lam tyA x body) (tarr tyA tyB)
, rule "T-App" $ do
(env, t1, t2, tyA, tyB) <- fresh
prem $ typeof env t1 (tarr tyA tyB)
prem $ typeof env t2 tyA
concl $ typeof env (app t1 t2) tyB
]TypedRedex ships with several interpreters over the same rule AST.
| Module | Purpose |
|---|---|
TypedRedex.Backend.Eval |
Run queries and collect answers |
TypedRedex.Interp.Trace |
Return successful or failing derivation trees |
TypedRedex.Interp.Typeset |
Render rules for notes and papers |
TypedRedex.Interp.MCheck |
Analyze mode discipline and scheduling |
The repository currently includes two runnable examples.
STLC: simply typed lambda calculus with tracing and QuickCheck propertiesLCTI: a larger type inference algorithm study with a regression suite. For essential logics, compare original haskell impl and typeredex-version to feel the lightweightness of the logic implementation.
Run them with:
cabal run example-stlc
cabal run example-lctiTypedRedex is currently intended to be used from a source checkout.
cabal update
cabal buildTo build the library and the included executables:
cabal build allTypedRedex.DSL: user-facing DSL for judgments and rulesTypedRedex.Backend.*: query construction and evaluation backendTypedRedex.Interp.*: tracing, typesetting, and mode checkingTypedRedex.Nominal*: binder-oriented utilities and nominal supportTypedRedex.Core.*: internal typed AST and supporting infrastructure
- Use Template Haskell to generate routine syntax definitions automatically, while still letting users define binder-heavy or otherwise non-standard cases by hand.
- Add an interactive front end for building derivations by selecting rules, in the spirit of Hazel Deriver. This would support reasoning with rule systems that are not purely algorithmic, and would likely take the form of a new interpreter.
TypedRedex is currently experimental.
The implementation is usable and the examples are non-trivial, but the public API should still be treated as evolving.
Contribution guidelines live in CONTRIBUTING.md.
TypedRedex is released under the MIT License. See LICENSE.