Constraint Handling Rules

SCL embeds a CHR (Constraint Handling Rules) engine: a forward-chaining rule system that works on a constraint store, a bag of facts. You declare the shapes of facts, write rules that match facts and produce new ones, and the engine runs the rules to exhaustion. It is the right tool for fixpoint computations, graph traversal, and anything naturally expressed as "whenever these facts are present, do this".

This is an advanced feature. Nothing here is needed for ordinary SCL programming.

A first example

slowSum :: [Integer] -> <Proc> Integer
slowSum list = getRef answer
  where
    answer = ref 0

    constraint El Integer

    ?x <- list      =>  El ?x
    -El ?x, -El ?y  =>  El (?x + ?y)
    El ?x           =>  answer := ?x

main = slowSum [1, 6, 9]      // 16

Read the three rules as:

1. for every ?x in list, add the fact El ?x to the store;
2. whenever two El facts are present, remove both and add their sum;
3. whenever an El fact is present, write its value to answer.

The engine runs until no rule can fire. Rule 2 keeps collapsing pairs until one El is left, and rule 3 has been writing every intermediate value to answer along the way, so the last value written is the total.

Where rules may be written

A CHR rule is a statement, so rules live in a block:

All the rules in one block share one constraint store, and the store lives exactly as long as one evaluation of that block. Two blocks never share constraints, even if they declare the same names:

f = ()
  where
    constraint A Integer
    True => A 1

g = ()
  where
    True => A 2          // a different, independently inferred A
    A ?x => print ?x     // prints 2, never 1

For a store that outlives a single call, see Rulesets.

No module header is required. constraint, =>, when/then, include and the ?x variable syntax are always available. The features = [chr] header flag does something narrower than its name suggests — see What the chr feature actually changes.

Constraints

A constraint declaration names a kind of fact and gives the types of its arguments:

constraint Edge Integer Integer
constraint Visited Integer
constraint Done                        // no arguments

Constraints may be polymorphic in the block's type variables:

uniq :: [a] -> <Proc> [a]
uniq l = MList.freeze answer
  where
    answer = MList.create ()

    constraint El a

    ?x <- l         =>  El ?x
    -El ?x, El ?x   =>  True
    El ?x           =>  MList.add answer ?x

Declaring a constraint is optional. An undeclared name used in a rule is inferred as a new constraint of that block, with argument types taken from its uses:

topologicalSort :: [(a,a)] -> <Proc> [a]
topologicalSort dependencies = MList.freeze answer
  where
    answer = MList.create ()

    (?x,?y) <- dependencies           =>  Dep ?x ?y, InDegree ?x 0, InDegree ?y 1
    -InDegree ?x ?a, -InDegree ?x ?b  =>  InDegree ?x (?a + ?b)
    InDegree ?x 0                     =>  AdjustInDegrees ?x, MList.add answer ?x
    AdjustInDegrees ?x, Dep ?x ?y     =>  InDegree ?y (-1)

Declaring them is still worth it: a declaration fixes the arity and types, so a typo becomes Constraint is applied with wrong number of parameters instead of a second, silently unrelated constraint.

Record constraints

A constraint can name its arguments instead of taking them positionally:

constraint Person { name :: String, age :: Integer }

True                           =>  Person { name = "Ann", age = 30 }
Person { ?name, ?age }, ?age > 10  =>  print "\(?name) is \(?age)"

Every field must be given when the fact is created — a missing one is Field y not defined. In a rule head you may mention only the fields you need. Record syntax requires a declaration; using it on an inferred constraint is Relation must be declared if record syntax is used, and using it on a positional one is Relation V does not define field names.

A constraint may also carry an ordinary record value, in which case the pattern applies to that value:

data V = V { x :: Double, y :: Double }

constraint X V

X V { ?x }  =>  print ?x
True        =>  X V { x = 1.0, y = 2.0 }

Rules

The basic form is

head  =>  body

where the head is a comma-separated conjunction of literals and the body is a comma-separated sequence of constraints to add and expressions to evaluate. The rule fires once for every combination of facts matching the head.

Head literals

- is what makes CHR terminate. A rule whose head only keeps facts and whose body adds new ones will loop forever unless a guard stops it:

constraint A Integer
True           =>  A 1
A ?x, ?x < 3   =>  print "kept \(?x)", A (?x+1)     // prints 1, 2 and stops

A rule that removes its inputs makes progress by construction:

constraint A Integer
True      =>  A 1, A 2, A 3
-A ?x     =>  print "consumed \(?x)"                // fires three times, then stops

Variables

?x introduces an existential variable, scoped to the rule. Ordinary SCL names in scope may be used as usual — they are values, not patterns:

isReachable edges a b = getRef answer
  where
    answer = ref False

    constraint Edge Integer Integer
    constraint Reachable Integer

    (?x,?y) <- edges          =>  Edge ?x ?y
    True                      =>  Reachable a        // a is a function parameter
    Reachable ?x, Edge ?x ?y  =>  Reachable ?y
    Reachable b               =>  answer := True

A ? variable that occurs only once is almost always a mistake, so the compiler warns: Existential variable ?y is referred only once. Replace by _ if this is a wildcard. Use _ when you genuinely do not care:

constraint A Integer Integer
A ?x _  =>  print ?x

New existential variables may appear only in a head. A ?x first mentioned in a body is New existential variables can be defined only in queries.

Bodies

A body may add constraints and evaluate effectful expressions, in any mix:

-Degree ?x ?a, -Edge ?x ?x  =>  Degree ?x (?a - 2), print "Remove loop (\(?x),\(?x))"

Bodies run for their effects, so a rule body typically writes to a Ref, an MList or the console. A block whose rule bodies are all pure needs no Proc effect; one that prints or mutates does, exactly like ordinary SCL code.

when / then

The same rule can be written in a layout-based form, with one literal per line. It is easier to read for rules with many literals:

when Foo ?x
     ?x < 5
then print ?x
     Foo (?x + 1)

when/then is equivalent to => with one extra capability: the body may introduce local bindings, which the comma-separated body of => cannot.

when Foo ?x
then y = ?x + 1
     print y

Like =>, it needs no module header.

Execution model

• Each rule gets a priority from its position in the block: earlier rules fire first. In this block the output is A1 A2 B1 B2 C1 C2, because every rule matching A fires in source order before -A => B finally removes A:

    constraint A
    constraint B
    constraint C
  
    A => add "A1"
    B => add "B1"
    C => add "C1"
    A => add "A2"
    B => add "B2"
    C => add "C2"
  
    True => A
    -A   => B
    -B   => C
  

• Rules from an included ruleset have higher priority than the block's own rules, so an included invariant gets a chance to fire before local rules see the fact.

• A rule fires once per distinct combination of matching facts, and never twice for the same combination.

• The engine runs to exhaustion: the block's value is computed after no rule can fire.

• The order in which several facts of the same constraint are tried is not specified. It is currently last-added-first, which is why ?x <- [10,20,30] => A ?x followed by A ?x => print ?x prints 30 20 10. Do not depend on it; sort the result if order matters.

Rulesets

A block's constraint store disappears when the block finishes. A ruleset is a store that lives in a value, so several calls can add to and query the same store.

Ruleset declarations are the one part of CHR that does need the header flag:

module {
    features = [chr]
}
import "StandardLibrary"

ruleset IntegerSet where
    constraint Element Integer
    -Element ?x, Element ?x  =>  print "duplicate \(?x)"

ruleset Name where ... declares two things:

createName takes no argument — write s = createIntegerSet, not createIntegerSet ().

A block joins an existing store with the include statement, after which it can match and add that ruleset's constraints:

addTo :: IntegerSet -> Integer -> <Proc> ()
addTo set e = ()
  where
    include IntegerSet set
    True => Element e

dump :: IntegerSet -> <Proc> ()
dump set = ()
  where
    include IntegerSet set
    Element ?x => print "have \(?x)"

main = ()
  where
    s = createIntegerSet
    addTo s 1
    addTo s 2
    addTo s 1          // prints "duplicate 1"
    dump s             // prints "have 2", "have 1"

The ruleset's own rules — here the duplicate check — run whenever any block that includes it adds a matching fact, not only inside the declaring module. A block may add rules of its own on top of the included ones.

Only the ruleset declaration needs features = [chr]. A module that merely imports a ruleset and uses include, createName and the constraints needs no header at all.

CHR queries

With features = [chr], select is compiled by the CHR engine instead of the ordinary SCL query engine. It can then query the enclosing block's constraint store:

module {
    features = [chr]
}
import "StandardLibrary"

main =
    select (?a,?b) where
        Foo ?a
        Bar ?b
  where
    True => Foo 1
    True => Foo 2
    True => Bar 3
    True => Bar 4

A CHR select is a pure expression — it needs no Proc effect — and select first works as usual, returning one solution rather than a list.

A select may also appear inside a rule head, which is the idiomatic way to express "… and there is no fact such that …" in the absence of real negation:

when -Edge ?x ?y
     [] = select ?z where
         Edge ?z ?x
then print "removed \(?x) \(?y)"

What the chr feature actually changes

features = [chr] does not switch CHR on — rules work without it. What it does is swap the meaning of four words in the lexer:

Two consequences are easy to trip over. First, turning the feature on removes the rule and transformation declarations from the module, so a module cannot mix CHR rulesets with mapping rules. Second, select changes engine, and with it the order of the results:

select (?a,?b) where
    ?a <- [1,2,3]
    ?b <- [2,3]

// without chr:  [(1,2), (2,2), (3,2), (1,3), (2,3), (3,3)]
// with chr:     [(1,2), (1,3), (2,2), (2,3), (3,2), (3,3)]

The results are the same set in a different order. If a module's existing select expressions depend on that order, adding chr to its header will change their behaviour.

Diagnostics

Limitations

Negation is not implemented. not Foo ?x in a head is rejected with CHR negation is not yet supported. Use an empty nested select instead, as shown under CHR queries.

Constraints take no annotations. @private and friends in front of a constraint are a syntax error.

CHR does not work outside module compilation. Rules written in an SCL script, in the SCL Console, or in any other expression evaluated through ExpressionEvaluator parse and type check, and then fail during code generation:

> True => Foo 1
  Foo ?x => print ?x
InternalCompilerError: Didn't find type constructor Expression$1/CHR$1.

A CHR block compiles to a generated runtime class that belongs to the enclosing module, and an expression compiled on its own has no module to put it in. Put CHR rules in a module function and call that function from the script. This is tracked as issue #1426; see also 1.18 Modules vs. scripts.

Fact ordering is unspecified, as noted under Execution model.

Further examples

The compiler's own regression fixtures are the most complete set of working CHR programs in the repository, covering sums, gcd, reachability, primes, topological sort, graph simplification, rulesets and CHR queries:

tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/scl/CHR*.scl

Each file contains the module text, a -- separator and the expected output.