chrKanren

This is chrKanren, an implementation of miniKanren with support for the Constraint Handling Rules (CHR) language for defining constraints. It is currently a work in progress! The primary goals of this implementation are (in order of priority): Extensibility, User Experience, Performance, Novelty, and Simplicity of Implementation.

The implementation will be written in pure, standards-abiding R6RS scheme. This means most of the code in the project is within R6RS libraries. The primary targets are racket and chez scheme, which run such programs, but other R6RS schemes should be able to run it without issue. In order to avoid re-inventing the wheel, chrKanren uses a number of SRFIs (generally, ones which do not change reader syntax or heavily effect program behavior).

Installation

The project puts the following constraints on the scheme implementation:

• It must map libraries locally onto the file-system
• It must have SRFI N available as the library (srfi :N)

Racket

One can install chrKanren as a local library using raco pkg install, then reference it from either R6RS or racket (note: R6RS ~list~​s → Racket ~mlist~​s) without issue. The SRFIs required are all packaged correctly in the srfi library, which is shipped with racket.

Chez Scheme

The necessary SRFIs are defined in the chez-srfi project. To use this, both this project and an installation of chez-srfi (named srfi) must be in one of Chez’s library-directories (which can be modified by calling chez with the --libdirs option or by setting the CHEZSCHEMELIBDIRS environment variable). One easy way to do this is to clone chez-srfi, rename the directory to srfi, then run the included link-dirs.chezscheme-sps script:

# Enter one of the library directories
cd "$SOMEWHERE_IN_CHEZSCHEMELIBDIRS"
# Clone into chez-srfi, then enter it
git clone https://github.com/arcfide/chez-srfi srfi
cd srfi
# Link the relevant files in-place
chezscheme --script link-dirs.chezscheme.sps
# Install chrKanren in the same directory
cd ..
git clone https://github.com/rvs314/chrKanren

Other Schemes

Other R6RS Scheme implementations (such as Ikarus, IronScheme or GNU Guile) may also work, but have not been tested extensively and may not have all the relevant SRFI implementations. If one can work with minimal additions, please send a PR!

Testing

The implementation of chrKanren has a number of tests in the tests/ directory, which are each top-level scheme programs. When evaluated, these programs run the tests contained within, printing the result of each test and the cause of any errors, should they occur.

Racket

To run all tests sequentially using Racket, execute the following command:

raco test -e -c chrKanren

To run them in parallel, only showing tests which fail, execute the following:

raco test --drdr -c chrKanren

Chez Scheme (or other implementations)

To run all tests sequentially using Chez, run the included shell script:

sh ./run-tests.sh

Setting the SCHEME_CMD environment variable will change the implementation used to run the tests, so the following runs the tests in a hypothetical example scheme:

SCHEME_CMD="my_cool_scheme --run-as-script" ./run_tests.sh

Contract Checking

The chrKanren implementation uses runtime contract checking to help with debugging; it’s turned on by default, but can be disabled by setting the environment variable DEBUG to OFF when compiling/running the code. This makes the code significantly faster, and should be done whenever performance tests are being run.

Constraint Handling Rules API

Constraints must initially be declared using the define-constraint form:

(define-constraint (symbolo obj))

Once they have been declared, they can be referenced in normal clauses, which will add them as constraints:

(run* (p) (symbolo p))
;; => (((_.0) (symbolo _.0)))

They can also be given simplification procedures using rules:

(define-constraint (non-symbolo o))

(define-rules
  (forall (o) (symbolo o) (ground symbol? o) => succeed)
  (forall (o) (symbolo o) (ground (negate symbol?) o) => fail)
  (forall (o) (non-symbolo o) (ground symbol? o) => fail)
  (forall (o) (non-symbolo o) (ground (negate symbol?) o) => succeed)
  (forall (o) (symbolo o) (non-symbolo o) => fail))

(run* (p)
  (symbolo p)
  (conde [(== "one" p)]
         [(non-symbolo p)]
         [(== p 'two)]))
;; => (((two)))