~ashton314/microKanren

4d41f61e863fcd3d17ec6c06fa4eab0f5057098d — Ashton Wiersdorf 6 months ago ea4a272
Add example of program synthesis
2 files changed, 13 insertions(+), 0 deletions(-)

M README.org
M kanren.rkt
M README.org => README.org +11 -0
@@ 152,6 152,17 @@ See [[./type_checking.rkt]] for an implementation of a simple type checker/infer
'((_.5 . _.5)) ;; generic type: a -> a
#+end_src

Here's the crazy thing: you can actually ask for programs that match a given type, since relations work both ways. Here's an example of generating five programs that are of type ~number → boolean~:

#+begin_src racket
> (run 5 (prog) (type-for prog '() (cons 'number 'boolean)))
'((lambda _.1 (? . #<procedure:boolean?>))
  (lambda _.1 (zero? (? . #<procedure:number?>)))
  (lambda (? . #<procedure:symbol?>) (zero? (? . #<procedure:symbol?>)))
  (lambda _.1 (zero? (+ (? . #<procedure:number?>) (? . #<procedure:number?>))))
  (lambda _.1 (if (? . #<procedure:boolean?>) (? . #<procedure:boolean?>) (? . #<procedure:boolean?>))))
#+end_src

* Author

I hope is /very clear/ that /I/ did /not/ write the μKanren paper. That would be Daniel P. Friedman and Jason Hemann. I merely wrote up this annotation.

M kanren.rkt => kanren.rkt +2 -0
@@ 204,6 204,8 @@

(define (call/empty-state g) (g empty-state))

;;; Use these to wrap your queries: run takes a number of n solutions
;;; to the program, while run* calls `take-all'.
(define-syntax run
  (syntax-rules ()
    [(_ n (xs ...) g gs ...)