Haskell Rules: Embedding Rule Systems in Haskell
Version: June 2006
Ukrainian translation by Domri team
Haskell Rules is a domain-specific embedded language that allows semantic
rules to be expressed as Haskell functions. This DSEL provides logical
variables, unification, substitution, non-determinism, and backtracking. It
also allows Haskell functions to be lifted to operate on logical variables.
These functions are automatically delayed so that the substitutions can be
The rule DSEL allows various kinds of logical embedding, for example,
including logical variables within a data structure or wrapping a data
structure with a logical wrapper.
-- embed logical variables into a data structure
data Type = TInt | TBool | TFun Type Type | TVar MVar
-- wrap a pre-existing structure with logical variable, e.g. L [a]
data L a = LV MVar | V a
We can devise rules that match the semantic rules for a given problem,
such as type inference. Below is an example that shows how to express
the type checking rule for applications.
The DSEL provides a built-in inference function which runs the rule system on
a given input, returning all possible successful matches of the rules.
app (env, (App e1 e2)) = do [a,b] <- newVars 2
(env, e1) .>. Fun a b
(env, e2) .>. a
> infer ( :: Env, Lam "x" (Var "x"))
[Fun (TVar (MVar 2)) (TVar (MVar 2))]
To use the DSEL:
More examples are included in the paper listed below.
- Download HaskellRules-jun06.tar.gz
Gunzip and untar the archive. This will create a directory
Change to that directory.
- Start GHC and load an example file.
You must use GHC 6.2 or 6.4 If you are using GHC 6.2, first read the
file readme.txt for a small change to TypeGU.hs.
Note that you have to use the flag -fglasgow-exts.
ghci -fglasgow-exts TypeLam.hs
Formulate queries. For example,
What is the type of the expression λ x . λ y . x y?
*TypeLam> infer (::Env, Lam "x" (Lam "y" (App (Var "x") (Var "y"))))
[Fun (Fun (TVar (MVar 5)) (TVar (MVar 6))) (Fun (TVar (MVar 5)) (TVar (MVar 6)))]
Haskell Rules: Embedding Rule Systems in Haskell,
Steve Kollmansberger and Martin Erwig, Draft Paper, June 2006
For more information, please contact: