1 files changed, 46 insertions(+), 0 deletions(-)

A type_checking_with_errors.rkt

@@ 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))))]))