DataKanren, a combination of datalog and microkanren

datakanren.rkt

#lang racket

(require racket/hash) ;; hash-union

;; UNIFICATION VAR
;; symbol beginning with ?
(define (var? x) (and (symbol? x) (string-prefix? (symbol->string x) "?")))
(define/contract (var x) (-> symbol? var?)
  (string->symbol (format "?~a" x)))
(define/contract (var-name x) (-> var? symbol?)
  (string->symbol (string-replace (symbol->string x) "?" "" #:all? #f)))

;; TERM
;; only ground terms are allowed
;; TODO: check that terms are free of unification vars.
(define term? any/c)

;; ROW
;; a list of (var = term) pairs.
;; a substitution, effectively; except I think the terms are always ground?
(define row? (listof (list/c var? '= term?)))
(define/contract empty-row row? '())

(define/contract (row-extend r x t) (-> row? var? term? row?)
  (cons (list x '= t) r))
(define/contract (row-remove row x)
  (-> row? var? row?)
  (filter (lambda (e) (not (equal? x (car e)))) row))

(define/contract (row->hash row)
  (-> row? hash?)
  (for/hash ([x row]) (values (car x) (caddr x))))
(define/contract (dict->row dict)
  (-> dict? row?)
  (for/list ([(k v) dict]) `(,k = ,v)))


;; TABLE
;; a stream of lists of rows
;;
;; The stream is for laziness. At each timestep we generate a list of rows we learned
;; about in that timestep. We can choose to delay by simply generating no rows during a
;; particular timestep. This is necessary to get recursion to work.
(define table/c (stream/c (listof row?)))

(define/contract (table . xs)
  (->* () #:rest (listof row?) table/c)
  (stream xs))
(define/contract empty-table table/c '())
(define-syntax-rule (table-delay e) (stream-cons '() e))

(define/contract (table-expose s)
  (-> table/c (or/c null? (cons/c any/c table/c)))
  (match s
    [(? stream-empty?) '()]
    [(stream* '() s) (table-expose s)]
    [(stream* (cons x xs) s) (cons x (stream-cons xs s))]))

(define/contract (table->list s)
  (-> table/c list?)
  (match (table-expose s)
    ['() '()]
    [(cons x xs) (cons x (table->list xs))]))

(define/contract (table-map f t)
  (-> (-> row? row?) table/c table/c)
  (stream-lazy
   (stream-map (lambda (rs) (map f rs)) t)))

(define/contract (table-unions streams)
  (-> (listof table/c) table/c)
  (stream-lazy
   (match (filter (not/c stream-empty?) streams)
     ['() '()]
     [`(,s) s]                          ; optimization
     [nonempty-streams
      (stream-cons
       #:eager (apply append (map stream-first nonempty-streams))
       (table-unions (map stream-rest nonempty-streams)))])))


;; NATURAL JOIN / "UNIFICATION" ;;
(define (table-join2 t1 t2)
  ;; but we do this one timestep at a time, statefully.
  (stream-lazy
   (let loop ([rows1 '()]
              [rows2 '()]
              [t1 t1]
              [t2 t2])
     (if (and (stream-empty? t1) (stream-empty? t2))
         empty-stream
         (let ()
           (define-values (drows1 rest1) (table-unfold t1))
           (define-values (drows2 rest2) (table-unfold t2))
           (stream-cons
            ;; find the new tuples: (drows1 ⋈ rows2) ∪ ((rows1 ∪ drows1) ⋈ drows2)
            ;; super naive implementation: cross product followed by filter.
            ;; ideally we'd index on the join columns, but we don't know what they are!
            #:eager (append (join drows1 rows2)
                            (join (append drows1 rows1) drows2))
            (loop (append drows1 rows1) (append drows2 rows2) rest1 rest2)))))))

(define/contract (join rows1 rows2)
  (-> (listof row?) (listof row?) (listof row?))
  (for*/list ([r rows1]
              [s rows2]
              #:do [(define x (unify r s))]
              #:when x)
    x))

(define/contract (unify r s)
  (-> row? row? (or/c row? false?))
  (with-handlers ([exn:fail? (lambda (_) #f)])
    (dict->row (hash-union (row->hash r) (row->hash s)
                           #:combine (lambda (v1 v2)
                                       (if (equal? v1 v2) v1
                                           (error 'unify "Unequal values")))))))

(define/match (table-unfold t)
  [((? stream-empty?)) (values '() empty-stream)]
  [((stream* x xs)) (values x xs)])


;;; DATAKANREN PROGRAMS as TABLE CALCULUS ;;;
;;
;; A logic program is a table.

(define/contract (== x t)
  (-> var? term? table/c)
  (table (row-extend empty-row x t)))

(define (disj . Ps) (table-unions Ps))
(define (conj . Ps) (foldr table-join2 (table empty-row) Ps))

(define-syntax exists
  (syntax-rules ()
    [(_ () body ...) (conj body ...)]
    [(_ (x xs ...) body ...)
     (call/exists (lambda (x) (exists (xs ...) body ...)))]))

;; existential projection
(define (call/exists f)
  (define x (var (gensym)))
  (table-map (lambda (row) (row-remove row x))
             (f x)))

(define-syntax-rule (conde (P ...) ...)
  (disj (conj P ...) ...))

;; Necessary for recursive definitions.
(define-syntax-rule (delaye P) (table-delay P))


;;; EXAMPLES ;;;
(define (pretty t #:n [n #f])
  (let loop ([i 0] [t t])
    (if (eqv? i n) (displayln "...")
        (match (table-expose t)
          ['() (void)]
          [(cons r rs)
           (displayln r)
           (loop (+ i 1) rs)]))))

(define (edgeo x y)
  (conde
   [(== x 'a) (== y 'b)]
   [(== x 'b) (== y 'c)]
   [(== x 'a) (== y 'c)]))

;; (table->list (edgeo '?src '?dst))

(define (patho x y)
  (delaye
   (disj (edgeo x y)
         (exists (z) (edgeo x z) (patho z y)))))

;; (pretty (patho '?src '?dst) #:n 4)
;;
;; Attempts to get more than 4 results will fail to terminate.
;;
;; I believe the search strategy is complete, but will fail to terminate for essentially
;; *any* recursive definition. By contrast miniKanren's sideways information passing makes
;; many recursive definitions terminate, eg. if they are somehow "structurally inductive".