1#lang racket/base
2
3(require redex/reduction-semantics
4         (only-in redex/private/generate-term pick-an-index)
5         racket/bool
6         racket/match
7         racket/contract
8         redex/tut-subst)
9
10(provide (all-defined-out))
11
12(define-language poly-stlc
13  (M N ::=
14     (λ (x σ) M)
15     (M N)
16     C
17     integer
18     x)
19  (C ::=
20     [C @ σ]
21     c)
22  (σ τ ::=
23     int
24     (σ → τ)
25     (list σ))
26  (γ ::=
27     int
28     (γ → γ)
29     (list γ)
30     α)
31  (Γ ::=
32     (x σ Γ)
33     •)
34  (Σ Y ::=
35     (∀ α Σ)
36     γ)
37  (x y ::= variable-not-otherwise-mentioned)
38  (α β ::= variable-not-otherwise-mentioned)
39  (c d ::=
40     map nil +
41     cons hd tl)
42
43  (v (λ (x τ) M)
44     C
45     integer
46     (+ v)
47     ([cons @ τ] v)
48     (([cons @ τ] v) v)
49     ([[map @ τ_1] @ τ_2] v))
50  (E hole
51     (E M)
52     (v E)))
53
54;; overlaps: random seed 35
55
56(define-judgment-form poly-stlc
57  #:mode (typeof I I O)
58
59  [---------------------
60   (typeof Γ number int)]
61
62  [(typeof-C C τ)
63   --------------
64   (typeof Γ C τ)]
65
66  [(where τ (lookup Γ x))
67   ----------------------
68   (typeof Γ x τ)]
69
70  [(typeof (x σ Γ) M σ_2)
71   --------------------------------
72   (typeof Γ (λ (x σ) M) (σ → σ_2))]
73
74  [(typeof Γ M (σ → σ_2)) (typeof Γ M_2 σ)
75   ----------------------
76   (typeof Γ (M M_2) σ_2)])
77
78(define-judgment-form poly-stlc
79  #:mode (typeof-C I O)
80
81  [(where (∀ α γ) (const-type c))
82   (where σ (t-subst γ α τ))
83   ------------------------------
84   (typeof-C [c @ τ] σ)]
85
86  [(where (∀ α (∀ β γ)) (const-type c))
87   (where γ_1 (t-subst γ β τ_2))
88   (where σ (t-subst γ_1 α τ_1))
89   ------------------------------
90   (typeof-C [[c @ τ_1] @ τ_2] σ)]
91
92  [(where γ (const-type c))
93   ------------------------------
94   (typeof-C c γ)])
95
96(define-extended-judgment-form poly-stlc typeof
97  #:mode (typ-ind I I O)
98  [(where (∀ α σ_c) (const-type c))
99   (where (σ → τ) (t-subst σ_c α σ_1))
100   (typ-ind Γ M σ)
101   -----------------------------------
102   (typ-ind Γ ([c @ σ_1] M) τ)])
103
104(define-metafunction poly-stlc
105  lookup : Γ x -> σ or #f
106  [(lookup (x σ Γ) x)
107   σ]
108  [(lookup (x σ Γ) x_2)
109   (lookup Γ x_2)]
110  [(lookup • x)
111   #f])
112
113(define-metafunction poly-stlc
114  const-type : c -> Σ
115  [(const-type nil)
116   (∀ b (list b))]
117  [(const-type cons)
118   (∀ a (a → ((list a) → (list a))))]
119  [(const-type hd)
120   (∀ a ((list a) → a))]
121  [(const-type tl)
122   (∀ a ((list a) → (list a)))]
123  [(const-type map)
124   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
125  [(const-type +)
126   (int → (int → int))])
127
128(define-metafunction poly-stlc
129  t-subst : γ α τ -> γ
130  [(t-subst int α τ)
131   int]
132  [(t-subst α α τ)
133   τ]
134  [(t-subst α β τ)
135   α]
136  [(t-subst (list γ) α τ)
137   (list (t-subst γ α τ))]
138  [(t-subst (γ → γ_2) α τ)
139   ((t-subst γ α τ) → (t-subst γ_2 α τ))])
140
141(define red
142  (reduction-relation
143   poly-stlc
144   (--> (in-hole E ((λ (x τ) M) v))
145        (in-hole E (subst M x v))
146        "βv")
147   (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2)))
148        (in-hole E v_1)
149        "hd")
150   (--> (in-hole E ((tl @ τ) (((cons @ τ) v_1) v_2)))
151        (in-hole E v_2)
152        "tl")
153   (--> (in-hole E ((((map @ τ_1) @ τ_2) v) (nil @ τ_1)))
154        (in-hole E (nil @ τ_2))
155        "map-nil")
156   (--> (in-hole E ((((map @ τ_1) @ τ_2) v) (((cons @ τ_1) v_1) v_2)))
157        (in-hole E (((cons @ τ_2) (v v_1)) ((((map @ τ_1) @ τ_2) v) v_2)))
158        "map-cons")
159   (--> (in-hole E ((hd @ τ) (nil @ τ)))
160        "error"
161        "hd-err")
162   (--> (in-hole E ((tl @ τ) (nil @ τ)))
163        "error"
164        "tl-err")
165   (--> (in-hole E ((+ integer_1) integer_2))
166        (in-hole E (Σ integer_1 integer_2))
167        "+")))
168
169(define-metafunction poly-stlc
170  [(Σ integer_1 integer_2) ,(+ (term integer_1) (term integer_2))])
171
172(define M? (redex-match poly-stlc M))
173(define/contract (Eval M)
174  (-> M? (or/c M? "error"))
175  (define M-t (judgment-holds (typeof • ,M τ) τ))
176  (unless (pair? M-t)
177    (error 'Eval "doesn't typecheck: ~s" M))
178  (define res (apply-reduction-relation* red M))
179  (unless (= 1 (length res))
180    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
181  (define ans (car res))
182  (if (equal? "error" ans)
183      "error"
184      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
185        (unless (equal? M-t ans-t)
186          (error 'Eval "internal error: type soundness fails for ~s" M))
187        ans)))
188
189(define x? (redex-match poly-stlc x))
190(define-metafunction poly-stlc
191  subst : M x M -> M
192  [(subst M x N)
193   ,(subst/proc x? (term (x)) (term (N)) (term M))])
194
195(define v? (redex-match? poly-stlc v))
196(define τ? (redex-match? poly-stlc τ))
197(define/contract (type-check M)
198  (-> M? (or/c τ? #f))
199  (define M-t (judgment-holds (typeof • ,M τ) τ))
200  (cond
201    [(null? M-t)
202     #f]
203    [(null? (cdr M-t))
204     (car M-t)]
205    [else
206     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
207
208(module+ test
209
210  (test-equal (judgment-holds (typeof • 5 τ) τ)
211              (list (term int)))
212  (test-equal (judgment-holds (typeof • [nil @ int] τ) τ)
213              (list (term (list int))))
214  (test-equal (judgment-holds (typeof • ([cons @ int] 1) τ) τ)
215              (list (term ((list int) → (list int)))))
216  (test-equal (judgment-holds (typeof • (([cons @ int] 1) [nil @ int]) τ) τ)
217              (list (term (list int))))
218  (test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
219              (list (term (int → int))))
220  (test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
221              (list (term ((int → int) → (int → (int → int))))))
222  (test-equal (judgment-holds
223               (typeof •
224                       ([tl @ int]
225                        ([hd @ (list int)]
226                         ((λ (l (list (list int)))
227                            (([cons @ (list int)] (([cons @ int] 1) [nil @ int]))
228                             l))
229                          [nil @ (list int)])))
230                       τ)
231               τ)
232              (list (term (list int))))
233  (test-equal (judgment-holds
234               (typeof •
235                       (([[map @ int] @ (list int)]
236                         (λ (x int) (([cons @ int] x) [nil @ int])))
237                        (([cons @ int] 2)
238                         (([cons @ int] 4)
239                          [nil @ int])))
240                       τ)
241               τ)
242              (list (term (list (list int)))))
243
244  (test-->> red (term ((λ (x int) x) 7)) (term 7))
245  (test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
246  (test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
247  (test-->> red
248            (term ((λ (x int) (([cons @ int] x) [nil @ int])) 11))
249            (term (([cons @ int] 11) [nil @ int])))
250  (test-->> red
251            (term ((λ (x int) (([cons @ int] x) [nil @ int])) 11))
252            (term (([cons @ int] 11) [nil @ int])))
253  (test-->> red
254            (term (([cons @ int] ((λ (x int) x) 11)) [nil @ int]))
255            (term (([cons @ int] 11) [nil @ int])))
256  (test-->> red
257            (term ([cons @ int] ((λ (x int) x) 1)))
258            (term ([cons @ int] 1)))
259  (test-->> red
260            (term (([cons @ int] ((λ (x int) x) 1)) [nil @ int]))
261            (term (([cons @ int] 1) [nil @ int])))
262  (test-->> red
263            (term ([hd @ int] ((λ (x int) (([cons @ int] x) [nil @ int])) 11)))
264            (term 11))
265  (test-->> red
266            (term ([tl @ int] ((λ (x int) (([cons @ int] x) [nil @ int])) 11)))
267            (term [nil @ int]))
268  (test-->> red
269            (term ([tl @ int] [nil @ int]))
270            "error")
271  (test-->> red
272            (term ([hd @ int] [nil @ int]))
273            "error")
274  (test-->> red
275            (term ((λ (f (int → (list int))) (f 3)) ([cons @ int] 1)))
276            (term (([cons @ int] 1) 3)))
277  (test-->> red
278            (term
279             ([tl @ int]
280              ([hd @ (list int)]
281               ((λ (l (list (list int)))
282                  (([cons @ (list int)] (([cons @ int] 1) [nil @ int]))
283                   l))
284                [nil @ (list int)]))))
285            (term [nil @ int]))
286
287  (test-->> red
288            (term (([[map @ int] @ (list int)]
289                    (λ (x int) (([cons @ int] x) [nil @ int])))
290                   (([cons @ int] 2)
291                    (([cons @ int] 4)
292                     [nil @ int]))))
293            (term (((cons @ (list int)) (((cons @ int) 2) (nil @ int)))
294                   (((cons @ (list int)) (((cons @ int) 4) (nil @ int)))
295                    (nil @ (list int))))))
296  (test-equal (Eval (term ((λ (x int) x) 3)))
297              (term 3))
298
299
300  (test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
301              (list (term int)))
302  (test-->> red
303            (term ((+ 1) ([hd @ int] [nil @ int])))
304            "error")
305  (test-->> red
306            (term ((+ ((+ 1) 2)) ((+ 3) 4)))
307            (term 10))
308  (test-->> red
309            (term ((λ (f (int → int)) (f 3)) (+ 1)))
310            (term 4))
311
312  (test-results))
313
314