Module

Baskerville.Rule

Package
purescript-baskerville-core
Repository
afcondon/purescript-baskerville

The rule eDSL: rule bodies as nondeterministic queries over the KB that cite their premises automatically.

The ergonomic point: in prim form the author looks up and threads FactIds by hand, and a forgotten citation silently weakens the proof term. Here matches and require both test a claim and cite the fact recording it — the derivation writes itself.

absent is negation as failure: sound at the fixpoint within a stratum, and it cites nothing (there is no fact to cite — that is the nature of negative knowledge in a monotone system). Stratification checking arrives with the analyzable layer; until then the client vouches, exactly as with prim rules' read-sets.

This is the pragmatic monadic tier from the design sketch: fully expressive, not yet statically analyzable. The naive engine needs no read-sets; when the semi-naive engine lands, eDSL rules grow theirs by interpretation and prim rules keep declaring them.

#RuleM Source

newtype RuleM residue claim rule axiom a

A nondeterministic KB query accumulating the premises and anchors it touched along each branch.

Instances

#rule Source

rule :: forall residue claim rule axiom. Eq axiom => rule -> RuleM residue claim rule axiom claim -> Rule residue claim rule axiom

Seal a body into an engine rule. Each query result becomes one derivation of the returned claim, citing the deduplicated premises the branch touched.

#each Source

each :: forall residue claim rule axiom a. Array a -> RuleM residue claim rule axiom a

Enumerate a domain. Cites nothing.

#matches Source

matches :: forall residue claim rule axiom a. (claim -> Maybe a) -> RuleM residue claim rule axiom a

Match a pattern against the feed: one branch per fact whose claim projects, each citing that fact. The Datalog relation scan.

#require Source

require :: forall residue claim rule axiom. Ord claim => claim -> RuleM residue claim rule axiom Unit

The claim must already be known; cites the fact recording it. The point lookup to matches' scan.

#absent Source

absent :: forall residue claim rule axiom. Ord claim => claim -> RuleM residue claim rule axiom Unit

Negation as failure: succeed iff the claim is not on the feed.

#anchor Source

anchor :: forall residue claim rule axiom. axiom -> RuleM residue claim rule axiom Unit

Attach a non-fact anchor (an event id, a timestamp) to this branch's derivation.

#askKB Source

askKB :: forall residue claim rule axiom. RuleM residue claim rule axiom (KB residue claim rule axiom)

The raw KB — the residue reader, and the eDSL's own small escape hatch. Reads through it cite nothing.

Modules
Baskerville.Conformance
Baskerville.Engine
Baskerville.Explain
Baskerville.Kernel
Baskerville.Rule