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