MK-design-recipe.md

Design Recipe for Relations:

1. Add another argument to the function to represent the output of the relation, add -o to function name
2. Replace each cond with conde
3. Whenever you return a value, instead bind that value to out
4. Rewrite all function calls to their relational equivalents.
5. Unnest all nested relational functions, use fresh to bind their output to some other variable and replace.
6. Move goals such that the recursive call happens last if possible.

#lang racket
(require minikanren)
(require rackunit)

; This is append written in BSL, lets translate it into a relation.
(define (append l1 l2)
  (cond
    [(empty? l1) l2]
    [else (cons (first l1) (append (rest l1) l2))]))

(check-equal? (append '(1 2 3) '(4 5 6)) '(1 2 3 4 5 6))
(check-equal? (append '(1 2 3) '()) '(1 2 3))
(check-equal? (append '() '(4 5 6)) '(4 5 6))

;; Step 1: Rewrite Signature
; (define (append l1 l2)
; =>
; (define (appendo l1 l2 out)

;; Step 2: Rewrite Cond
; (cond
; =>
; (conde

;; Step 3: Bind to "out"
#|
(define (appendo l1 l2 out)
  (conde
    [(empty? l1) (== out l2)]
    [else (== out (cons (first l1) (append (rest l1) l2)))]))
|#

;; Step 4: Rewrite Functions to Relations
#|
(define (appendo l1 l2 out)
  (conde
    [(emptyo l1) (== out l2)]
    [else (== out (conso (firsto l1) (appendo (resto l1) l2)))]))
|#

;; Step 5-1: Unnest nested relations
#|
(define (appendo l1 l2 out)
  (conde
    [(emptyo l1) (== out l2)]
    [(firsto l1)
     (resto l1)
     (appendo (resto l1) l2)
     (conso (firsto l1) (appendo (resto l1) l2)))
     (== out ???)]))
|#
;; Step 5-2: Declare and bind fresh variables if needed
#|
(define (appendo l1 l2 out)
  (conde
    [(emptyo l1) (== out l2)]
    [(fresh (a d res)
         (firsto l1 a)
         (resto l1 d)
         (appendo d l2 res)
         (conso a res out))]))
|#
;; Step 6: Make recursive calls last

(define (appendo l1 l2 out)
  (conde
    [(emptyo l1) (== out l2)]
    [(fresh (a d res)
         (firsto l1 a)
         (resto l1 d)
         (conso a res out)
         (appendo d l2 res))]))
         
; And we're done!
 
(run* (a b) (appendo a b '(1 2 3))) 

---------------------------------------------------------------------------------------------------------------

Helpers

; Predicate relation 'succeeds' when l is empty, fails when it is not. Predicates dont need an 'out' argument.
(define (emptyo l)
  (== l '()))

; same as caro
(define (firsto l out)
  (fresh (a d)
         (== (cons a d) l)
         (== out a)))

; same as cdro
(define (resto l out)
  (fresh (a d)
         (== (cons a d) l)
         (== out d)))

; cons is the only 'function' you can use inside a relation
(define (conso a d out)
   (== (cons a d) out))

Testing: Check-expects don’t exist in regular Racket. We use rackunit instead. Instead of check-expect, write check-equal? If the test passes, nothing happens! If the test fails, the failing test will appear in the interactions window.