scheme-pearls/typechecker.rkt at main · evalwhen/scheme-pearls · GitHub

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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
#lang racket


(define ext-env
  (lambda (name value env)
    (cons (cons name value) env)))

(define ext-env*
  (lambda (names values env)
    (cond
      [(and (null? names) (null? values))
       env]
      [(and (pair? names) (pair? values))
       (ext-env*
        (cdr names)
        (cdr values)
        (ext-env (car names) (car values) env))]
      [else
       (error "number of names and values don't match")])))

(define env0
  `((+ . ,+)
    (- . ,-)
    (* . ,*)
    (/ . ,/)))

(define interp1
  (lambda (exp env)
    (match exp
      [(? number? exp)
       exp]
      [(? symbol? exp)
       (let ([p (assq exp env)])
         (cond
           [(not p)
            (error "Unbound variable: " exp)]
           [else
            (cdr p)]))]
      [`(lambda (,params ...) ,body)
       `(closure ,exp ,env)]
      [`(,op ,args ...)
       (let ([op-value (interp1 op env)]
             [arg-values (map (lambda (a) (interp1 a env)) args)])
         (match op-value
           [(? procedure? proc)
            (apply proc arg-values)]
           [`(closure (lambda (,params ...) ,body) ,closure-env)
            (let ([new-env (ext-env* params arg-values closure-env)])
              (interp1 body new-env))]
           [_
            (error "Calling non-function: " op)]))])))

(define interp
  (lambda (exp)
    (interp1 exp env0)))


;; -------- tests --------

(interp '(+ 1 (* 2 3)))

(interp '((lambda (x) (* x x)) 3))

(interp '((lambda (x y) (* x y)) 3 4))


;; -------- type checker --------

(define type-env0
  `((+ . (-> int int int))
    (- . (-> int int int))
    (* . (-> int int int))
    (/ . (-> int int int))))

(define typecheck1
  (lambda (exp env)
    (match exp
      [(? number? exp)
       'int]
      [(? boolean? exp)
       'bool]
      [(? symbol? exp)
       (let ([p (assq exp env)])
         (cond
           [(not p)
            (error "Unbound variable: " exp)]
           [else
            (cdr p)]))]
      [`(lambda (,params : ,in-types) ... : ,out-type
          ,body)
       (let* ([env1 (ext-env* params in-types env)]
              [actual (typecheck1 body env1)])
         (cond
           [(equal? actual out-type)
            `(-> ,@in-types ,out-type)]
           [else
            (error "expected output type: " out-type ", but got: " actual)]))]
      [`(,op ,args ...)
       (let ([op-type (typecheck1 op env)]
             [arg-types (map (lambda (a) (typecheck1 a env)) args)])
         (match op-type
           [`(-> ,in-types ... ,out-type)
            (cond
              [(equal? arg-types in-types)
               out-type]
              [else
               (error "expected input type: " in-types ", but got: " arg-types)])]
           [_
            (error "Calling non-function: " op)]))])))

(define typecheck
  (lambda (exp)
    (typecheck1 exp type-env0)))


(typecheck 2)
(typecheck #f)

(typecheck '(lambda (x : int) : int
              x))

(typecheck '((lambda (x : int) : int
               (* x x)) 3))

(typecheck '(lambda (x : int) (y : int) : int
              (+ 1 (* x y))))

(typecheck '((lambda (x : int) (y : int) : int
               (+ 1 (* x y)))
             2 3))


;(typecheck '(lambda (n : nat) : (vec atom n)
;              ...))
;
;(typecheck '(lambda (n : nat) (v : (vec atom n)) (index : nat) : atom
;              ...))
;