Haskell Rules: Embedding Rule Systems in Haskell

Haskell Rules: Embedding Rule Systems in Haskell
Version: June 2006

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 applied. 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.

app (env, (App e1 e2)) = do [a,b] <- newVars 2
                            (env, e1) .>. Fun a b
                            (env, e2) .>. a
                            return b

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.

> infer ([] :: Env, Lam "x" (Var "x"))
[Fun (TVar (MVar 2)) (TVar (MVar 2))]

To use the DSEL:

Download HaskellRules-jun06.tar.gz
Gunzip and untar the archive. This will create a directory HaskellRules-jun06. 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)))]

More examples are included in the paper listed below.

Further Information

Haskell Rules: Embedding Rule Systems in Haskell, Steve Kollmansberger and Martin Erwig, Draft Paper, June 2006

Contact

For more information, please contact: Martin Erwig

last change: January 20, 2013

Martin Erwig erwig@eecs.oregonstate.edu