type-kanren ·

Logic programming in TypeScript's type system. A compile-time implementation of miniKanren.

Usage

import { Eval, Eq, Conj, Disj } from 'type-kanren';

// Unification
type R1 = Eval<number, Eq<'X', 5>>;
const r1: R1 = [{ X: 5 }];

// Conjunction (AND)
type R2 = Eval<number, Conj<Eq<'X', 'Y'>, Eq<'Y', 5>>>;
const r2: R2 = [{ X: 5, Y: 5 }];

// Disjunction (OR)  
type R3 = Eval<number, Disj<Eq<'X', 1>, Eq<'X', 2>>>;
const r3: R3 = [{ X: 1 }, { X: 2 }];

Reference

Everything is parameterized by type T (the domain of values).

Terms can be:

• Variables: strings like 'X', 'Y'.
• Values: any value of type T.
• Pairs: [Term, Term] tuples.

Goals are logical statements:

• Eq<A, B> - Unify two terms.
• Conj<G1, G2> - Both goals must succeed.
• Disj<G1, G2> - Either goal can succeed.

Eval<T, Goal> runs a goal and returns all solutions that satisfy the constraints.

Examples

// Find all pairs where X ∈ {1,2} and Y ∈ {3,4}
type Result = Eval<number,
  Conj<
    Disj<Eq<'X', 1>, Eq<'X', 2>>,
    Disj<Eq<'Y', 3>, Eq<'Y', 4>>
  >
>;
const result: Result = [
  { X: 1, Y: 3 }, { X: 1, Y: 4 }, 
  { X: 2, Y: 3 }, { X: 2, Y: 4 }
];

// Occurs check prevents infinite structures  
type Impossible = Eval<number, Eq<'X', ['X', 'Y']>>;
const impossible: Impossible = []; // X can't equal something containing itself

// One branch failing doesn't affect the other
type OneSucceeds = Eval<number, 
  Disj<
    Conj<Eq<'X', 2>, Eq<'X', 3>>,  // This branch fails
    Eq<5, 'X'>                     // This branch succeeds
  >
>;
const oneSucceeds: OneSucceeds = [{ X: 5 }];

Latin 2x2 Square

For a more complex example, consider a 2x2 Latin square:

import { Eval, Eq, Conj, Disj, ConjN, UniqueSolutions } from "type-kanren";

type Value = 1 | 2;

type Diff<X, Y> =
  Disj<
    Conj<Eq<X, 1>, Eq<Y, 2>>,
    Conj<Eq<X, 2>, Eq<Y, 1>>
  >;

// https://en.wikipedia.org/wiki/Latin_square
// Finds values whose adjacent values are different
// A B
// C D
type Latin2 =
  ConjN<[
    // rows
    Diff<'A', 'B'>, Diff<'C', 'D'>,

    // cols
    Diff<'A', 'C'>, Diff<'B', 'D'>,
  ]>;

type Solutions = Eval<Value, Latin2>;
// Sometimes the solutions are not unique and you need to apply this type.
type DedupSolutions = UniqueSolutions<Value, Solutions>;
const squares: DedupSolutions = [{
  A: 1, B: 2,
  C: 2, D: 1
}, {
  A: 2, B: 1,
  C: 1, D: 2
}];

See more examples in the static tests.