~ashton314/microKanren

1430db531bebf8f7b02714286f2306f654ec55a0 — Ashton Wiersdorf 4 months ago 4458ce9 master
Trying out some type checking with errors
1 files changed, 46 insertions(+), 0 deletions(-)

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

(require "kanren.rkt")

;;; Environment functions
(define (Γ-lookup Γ x τ)
  (disj (fresh (Γ*) (== Γ (cons (cons x τ) Γ*)))
        (fresh (Γ* x* τ*)
               (conj (== Γ (cons (cons x* τ*) Γ*))
                     (Γ-lookup Γ* x τ)))))

(define (Γ-extend Γ x τ Γ*)
  (== (cons (cons x τ) Γ) Γ*))

;;; Type checker core
;; type-for :: form × type-env × (cons type reason)
(define (type-for expr Γ t)
  (conde
   [(== (cons '? number?) expr) (== t (cons 'number "literal number"))]
   [(== (cons '? boolean?) expr) (== t (cons 'boolean "litteral boolean"))]
   [(fresh (r1) (== (cons '? symbol?) expr) (Γ-lookup Γ expr (cons t r1)))]
   [(fresh (op r1)
           (== expr `(zero? ,op))
           (type-for op Γ (cons 'number r1))
           (== t (cons 'boolean "zero? expects a boolean")))]
   [(fresh (c t-case f-case arm-type r1 r2 r3)
           (== expr `(if ,c ,t-case ,f-case))
           (type-for c Γ (cons 'boolean r1))
           (type-for t-case Γ (cons arm-type r2))
           (type-for f-case Γ (cons arm-type r3))
           (== t (cons arm-type 'derived)))]
   [(fresh (op1 op2 r1 r2)
           (== expr `(+ ,op1 ,op2))
           (type-for op1 Γ (cons 'number r1))
           (type-for op2 Γ (cons 'number r2))
           (== t (cons 'number "+ expects arguments to be numbers")))]
   [(fresh (arg body arg-type Γ* body-type r1)
           (conj+ (== `(λ ,arg ,body) expr)
                  (Γ-extend Γ arg (cons arg-type 'derived) Γ*)
                  (type-for body Γ* (cons body-type r1))
                  (== t (cons (cons arg-type body-type) 'derived))))]
   [(fresh (fexpr arg arg-type body-type r1)
           (conj+ (== expr `(,fexpr ,arg))
                  (type-for fexpr Γ (cons arg-type body-type))
                  (type-for arg Γ (cons arg-type r1))
                  (== t (cons body-type 'derived))))]))