~ashton314/microKanren

microKanren/type_checking_with_errors.rkt -rw-r--r-- 1.9 KiB
1430db53Ashton Wiersdorf Trying out some type checking with errors 4 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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))))]))