1#lang racket
2(require redex)
3(provide λ λv red typeof)
4
5(define-language λ
6  (e (e e)
7     x
8     (λ (x τ) e)
9     (if0 e e e)
10     (+ e e)
11     number)
12  (τ (τ -> τ) num)
13  (x variable-not-otherwise-mentioned))
14
15(define-extended-language λv λ
16  (v (λ (x τ) e) number)
17  (E hole
18     (v E) (E e)
19     (if0 E e e)
20     (+ E e) (+ v E))
21  (Γ · (x τ Γ)))
22
23(define red
24  (reduction-relation
25   λv
26   (--> (in-hole E (+ number_1 number_2))
27        (in-hole E (Σ number_1 number_2))
28        "+")
29   (--> (in-hole E (if0 0 e_1 e_2))
30        (in-hole E e_1)
31        "if0t")
32   (--> (in-hole E (if0 number e_1 e_2))
33        (in-hole E e_2)
34        "if0f"
35        (side-condition
36          (not (= 0 (term number)))))
37   (--> (in-hole E ((λ (x τ) e) v))
38        (in-hole E (subst x v e))
39        "βv")))
40
41(define-metafunction λv
42  Σ : number number -> number
43  [(Σ number_1 number_2)
44   ,(+ (term number_1) (term number_2))])
45
46(define-metafunction λv
47  subst : x any any -> any
48  ;; 1. x_1 bound, so don't continue in λ body
49  [(subst x_1 any_1 (λ (x_1 τ_1) any_2))
50   (λ (x_1 τ_1) any_2)]
51  ;; 2. general purpose capture avoiding case
52  [(subst x_1 any_1 (λ (x_2 τ_2) any_2))
53   (λ (x_new τ_2)
54     (subst x_1 any_1
55            (subst-var x_2 x_new
56                       any_2)))
57   (where (x_new)
58          ,(variables-not-in
59            (term (x_1 any_1 any_2))
60            (term (x_2))))]
61  ;; 3. replace x_1 with e_1
62  [(subst x_1 any_1 x_1) any_1]
63  ;; 4. x_1 and x_2 are different, so don't replace
64  [(subst x_1 any_1 x_2) x_2]
65  ;; the last cases cover all other expressions
66  [(subst x_1 any_1 (any_2 ...))
67   ((subst x_1 any_1 any_2) ...)]
68  [(subst x_1 any_1 any_2) any_2])
69
70(define-metafunction λv
71  subst-var : x any any -> any
72  [(subst-var x_1 any_1 x_1) any_1]
73  [(subst-var x_1 any_1 (any_2 ...))
74   ((subst-var x_1 any_1 any_2) ...)]
75  [(subst-var x_1 any_1 any_2) any_2])
76
77(define-judgment-form λv
78  #:mode (typeof I I O)
79  #:contract (typeof Γ e τ)
80
81  [---------------------
82   (typeof Γ number num)]
83
84  [(typeof Γ e_1 num)
85   (typeof Γ e_2 num)
86   --------------------------
87   (typeof Γ (+ e_1 e_2) num)]
88
89  [(typeof Γ e_1 num)
90   (typeof Γ e_2 τ)
91   (typeof Γ e_3 τ)
92   ------------------------------
93   (typeof Γ (if0 e_1 e_2 e_3) τ)]
94
95  [(where τ (lookup Γ x))
96   ----------------------
97   (typeof Γ x τ)]
98
99  [(typeof Γ e_1 (τ_2 -> τ))
100   (typeof Γ e_2 τ_2)
101   --------------------------
102   (typeof Γ (e_1 e_2) τ)]
103
104  [(typeof (x_1 τ_1 Γ) e τ)
105   ----------------------------------------
106   (typeof Γ (λ (x_1 τ_1) e) (τ_1 -> τ))])
107
108(define-metafunction λv
109  lookup : Γ x -> τ or #f
110  [(lookup (x τ Γ) x) τ]
111  [(lookup (x_1 τ Γ) x_2) (lookup Γ x_2)]
112  [(lookup · x) #f])
113
114
115;; remove this #; to run an example
116#;
117(traces red
118        (term
119         (+ ((λ (n num)
120               (if0 n
121                    1
122                    0))
123             (+ 2 2))
124            2)))
125
126;; remove this #; to generate a random well-typed term
127#;
128(generate-term λv #:satisfying (typeof · e num) 5)
129
130
131(define (preservation e)
132  (define types (judgment-holds (typeof · ,e τ) τ))
133  (unless (null? types)
134    (unless (= 1 (length types)) (error 'preservation "multiple types! ~s" e)))
135  (cond
136    [(null? types) #t]
137    [else
138     (for/and ([v (apply-reduction-relation* red e)])
139       (equal? (judgment-holds (typeof · ,v τ) τ)
140               types))]))
141
142(define (try-it)
143  (redex-check λv
144               #:satisfying (typeof · e num)
145               (preservation (term e))))
146
147(test-->> red (term ((λ (x num) x) 1)) 1)
148(test-->> red (term (((λ (x num) (λ (y num) x)) 1) 2)) 1)
149(test-->> red (term (((λ (x num) (λ (y num) y)) 1) 2)) 2)
150(test-->> red (term (((λ (x num) (λ (x num) x)) 1) 2)) 2)
151(test-->> red (term (((λ (x num) (λ (y num) x)) 1) 2)) 1)
152(test-->> red (term ((λ (x num) (+ x x)) 2)) 4)
153(test-->> red (term ((λ (x num) (if0 x x (+ x 1))) 2)) 3)
154(test-->> red (term ((λ (x num) (if0 x x (+ x 1))) 0)) 0)
155(test-->> red
156          (term (((λ (x num) (λ (y num) (λ (z num) x))) 1) 2))
157          (term (λ (z num) 1)))
158(test-->> red
159          (term (+ (+ 1 2) (+ 3 4)))
160          (term 10))
161
162(test-equal (term (subst x y x)) (term y))
163(test-equal (term (subst x y z)) (term z))
164(test-equal (term (subst x y (x (y z)))) (term (y (y z))))
165(test-equal (term (subst x y ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z)))))
166            (term ((λ (x num) x) ((λ (y2 num) y2) (λ (x num) z)))))
167(test-equal (term (subst x y (if0 (+ 1 x) x x)))
168            (term (if0 (+ 1 y) y y)))
169(test-equal (term (subst x (λ (z num) y) (λ (y num) x)))
170            (term (λ (y1 num) (λ (z num) y))))
171(test-equal (term (subst x 1 (λ (y num) x)))
172            (term (λ (y num) 1)))
173(test-equal (term (subst x y (λ (y num) x)))
174            (term (λ (y1 num) y)))
175(test-equal (term (subst x (λ (y num) y) (λ (z num) (z2 z))))
176            (term (λ (z1 num) (z2 z1))))
177(test-equal (term (subst x (λ (z num) z) (λ (z num) (z1 z))))
178            (term (λ (z2 num) (z1 z2))))
179(test-equal (term (subst x z (λ (z num) (z1 z))))
180            (term (λ (z2 num) (z1 z2))))
181(test-equal (term (subst x3 5 (λ (x2 num) x2)))
182            (term (λ (x1 num) x1)))
183(test-equal (term (subst z * (λ (z num) (λ (x num) 1))))
184            (term (λ (z num) (λ (x num) 1))))
185(test-equal (term (subst q (λ (x num) z) (λ (z num) (λ (x num) q))))
186            (term (λ (z1 num) (λ (x1 num) (λ (x num) z)))))
187(test-equal (term (subst x 1 (λ (x num) (λ (x num) x))))
188            (term (λ (x num) (λ (x num) x))))
189
190(define (typecheck G e)
191  (match (judgment-holds (typeof ,G ,e τ) τ)
192    [(list) #f]
193    [(list t) t]
194    [_ (error 'typecheck
195              "multiple typing derivations for term ~a in environment ~a"
196              e G)]))
197
198(test-equal (typecheck (term ·) (term 1))
199            (term num))
200(test-equal (typecheck (term ·) (term (1 1)))
201            #f)
202(test-equal (typecheck (term (x num ·)) (term x))
203            (term num))
204(test-equal (typecheck (term ·) (term x))
205            #f)
206(test-equal (typecheck (term ·) (term ((λ (x num) x) 1)))
207            (term num))
208(test-equal (typecheck (term ·) (term (((λ (x num) x) 1) 2)))
209            #f)
210(test-equal (typecheck (term ·)
211                       (term (((λ (f (num -> num))
212                                 (λ (x num)
213                                   (f x)))
214                               (λ (x num) x))
215                              1)))
216            (term num))
217(test-equal (typecheck (term ·)
218                       (term (((λ (f (num -> num))
219                                 (λ (x num)
220                                   (f x)))
221                               1)
222                              (λ (x num) x))))
223            #f)
224(test-equal (typecheck (term ·) (term (+ (+ 1 2) 3)))
225            (term num))
226(test-equal (typecheck (term ·) (term (if0 1 (λ (x num) x) 3)))
227            #f)
228(test-equal (typecheck (term ·) (term (if0 1 2 3)))
229            (term num))
230(test-equal (typecheck (term ·) (term (λ (x num) (x 2))))
231            #f)
232(test-equal (typecheck (term ·)
233                       (term (λ (x num)
234                               (λ (x (num -> num))
235                                 (x 0)))))
236            (term (num -> ((num -> num) -> num))))
237(test-equal (typecheck (term ·)
238                       (term (λ (x (num -> num))
239                               (λ (x num)
240                                 (x 0)))))
241            #f)
242
243(test-results)
244