ea4a2720a1cba99abdeb79a1bdf63ae2c8d896a1 — Ashton Wiersdorf 6 months ago 668fe5d
Add type checker, applications section
2 files changed, 75 insertions(+), 0 deletions(-)

A type_checking.rkt
M README.org => README.org +24 -0
@@ 128,6 128,30 @@ I've added some rudimentary predicate checking to the ~unify~ function:
'(42 (? . #<procedure:even?>))

* Applications

** Family tree relationships

The classic example. See [[./relations_playground.rkt]]. Because of how the relations are defined, this will print out an infinite list of relations if you try to run certain queries, so best use the ~run~ function with some finite (and preferably small number; it doesn't take much to cover the whole space at least once) bound, as opposed to just running ~run*~.

** Type checking

See [[./type_checking.rkt]] for an implementation of a simple type checker/inference algorithm. Here is how you check the type of a program:

#+begin_src racket
> (run* (type) (type-for '((lambda x x) 2) '() type))

> (run* (type) (type-for '((lambda x (zero? x)) 2) '() type))

> (run* (type) (type-for '((lambda x (zero? x)) #f) '() type))
'()  ;; type error

> (run* (type) (type-for '(lambda x x) '() type))
'((_.5 . _.5)) ;; generic type: a -> a

* 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.

A type_checking.rkt => type_checking.rkt +51 -0
@@ 0,0 1,51 @@
#lang racket/base

(require "kanren.rkt")

;;; Environment functions
(define (Γ-lookup Γ x τ)
  ;; The environment is modeled as a simple assoc list, mapping
  ;; variables to types. The lookup function works by relating a
  ;; variable and its environment with a type by first checking if the
  ;; first thing in the assoc list matches the variable, and if not,
  ;; proceeding recursively down the list.
  (disj (fresh (Γ*) (== Γ (cons (cons x τ) Γ*)))
        (fresh (Γ* x* τ*)
               (conj (== Γ (cons (cons x* τ*) Γ*))
                     (Γ-lookup Γ* x τ)))))

(define (Γ-extend Γ x τ Γ*)
  ;; This slaps a new pair on the front of the environment assoc list.
  (== (cons (cons x τ) Γ) Γ*))

;;; Type checker core
(define (type-for expr Γ t)
   [(== (cons '? number?) expr) (== t 'number)]
   [(== (cons '? boolean?) expr) (== t 'boolean)]
   [(== (cons '? symbol?) expr) (Γ-lookup Γ expr t)]
   [(fresh (op)
           (== expr `(zero? ,op))
           (type-for op Γ 'number)
           (== t 'boolean))]
   [(fresh (c t-case f-case arm-type)
           (== expr `(if ,c ,t-case ,f-case))
           (type-for c Γ 'boolean)
           (type-for t-case Γ arm-type)
           (type-for f-case Γ arm-type)
           (== t arm-type))]
   [(fresh (op1 op2)
           (== expr `(+ ,op1 ,op2))
           (type-for op1 Γ 'number)
           (type-for op2 Γ 'number)
           (== t 'number))]
   [(fresh (arg body arg-type Γ* body-type)
           (conj+ (== `(lambda ,arg ,body) expr)
                  (Γ-extend Γ arg arg-type Γ*)
                  (type-for body Γ* body-type)
                  (== t (cons arg-type body-type))))]
   [(fresh (fexpr arg arg-type body-type)
           (conj+ (== expr `(,fexpr ,arg))
                  (type-for fexpr Γ (cons arg-type body-type))
                  (type-for arg Γ arg-type)
                  (== t body-type)))]))