exist.rkt (2676B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+reco+var.rkt") 3 4 ;; existential types 5 ;; Types: 6 ;; - types from stlc+reco+var.rkt 7 ;; - ∃ 8 ;; Terms: 9 ;; - terms from stlc+reco+var.rkt 10 ;; - pack and open 11 12 (provide ∃ pack open) 13 14 (define-binding-type ∃ #:bvs = 1) 15 16 (define-typed-syntax pack 17 [(_ (τ:type e) as ∃τ:type) 18 #:with (~∃ (τ_abstract) τ_body) #'∃τ.norm 19 #:with [e- τ_e] (infer+erase #'e) 20 #:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body)) 21 (⊢ e- : ∃τ.norm)]) 22 23 (define-typed-syntax open #:datum-literals (<=) 24 [(_ [x:id <= e_packed with X:id] e) 25 ;; The subst below appears to be a hack, but it's not really. 26 ;; It's the (TaPL) type rule itself that is fast and loose. 27 ;; Leveraging the macro system's management of binding reveals this. 28 ;; 29 ;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366: 30 ;; Γ ⊢ e_packed : {∃X,τ_body} 31 ;; Γ,X,x:τ_body ⊢ e : τ_e 32 ;; ------------------------------ 33 ;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e 34 ;; 35 ;; There's *two* separate binders, the ∃ and the let, 36 ;; which the rule conflates. 37 ;; 38 ;; Here's the rule rewritten to distinguish the two binding positions: 39 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 40 ;; Γ,X_???,x:τ_body ⊢ e : τ_e 41 ;; ------------------------------ 42 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 43 ;; 44 ;; The X_1 binds references to X in T_12. 45 ;; The X_2 binds references to X in t_2. 46 ;; What should the X_??? be? 47 ;; 48 ;; A first guess might be to replace X_??? with both X_1 and X_2, 49 ;; so all the potentially referenced type vars are bound. 50 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 51 ;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e 52 ;; ------------------------------ 53 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 54 ;; 55 ;; But this example demonstrates that the rule above doesnt work: 56 ;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2] 57 ;; ((λ ([y : X_2]) y) x) 58 ;; Here, x has type X_1, y has type X_2, but they should be the same thing, 59 ;; so we need to replace all X_1's with X_2 60 ;; 61 ;; Here's the fixed rule, which is implemented here 62 ;; 63 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 64 ;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e 65 ;; ------------------------------ 66 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 67 ;; 68 #:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed) 69 #:with τ_x (subst #'X #'Y #'τ_body) 70 #:with [(_ x-) e- τ_e] (infer/ctx+erase #'(X [x : τ_x]) #'e) 71 (⊢ (let- ([x- e_packed-]) e-) : τ_e)])