exist.rkt (2514B)
1 #lang turnstile/lang 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 (τ:type e) as ∃τ:type) ≫ 17 #:with (~∃ (τ_abstract) τ_body) #'∃τ.norm 18 #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body) 19 [⊢ e ≫ e- ⇐ τ_e] 20 -------- 21 [⊢ e- ⇒ ∃τ.norm]) 22 23 (define-typed-syntax (open [x:id (~datum <=) e_packed (~datum with) X:id] e) ≫ 24 ;; The subst below appears to be a hack, but it's not really. 25 ;; It's the (TaPL) type rule itself that is fast and loose. 26 ;; Leveraging the macro system's management of binding reveals this. 27 ;; 28 ;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366: 29 ;; Γ ⊢ e_packed : {∃X,τ_body} 30 ;; Γ,X,x:τ_body ⊢ e : τ_e 31 ;; ------------------------------ 32 ;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e 33 ;; 34 ;; There's *two* separate binders, the ∃ and the let, 35 ;; which the rule conflates. 36 ;; 37 ;; Here's the rule rewritten to distinguish the two binding positions: 38 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 39 ;; Γ,X_???,x:τ_body ⊢ e : τ_e 40 ;; ------------------------------ 41 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 42 ;; 43 ;; The X_1 binds references to X in T_12. 44 ;; The X_2 binds references to X in t_2. 45 ;; What should the X_??? be? 46 ;; 47 ;; A first guess might be to replace X_??? with both X_1 and X_2, 48 ;; so all the potentially referenced type vars are bound. 49 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 50 ;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e 51 ;; ------------------------------ 52 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 53 ;; 54 ;; But this example demonstrates that the rule above doesnt work: 55 ;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2] 56 ;; ((λ ([y : X_2]) y) x) 57 ;; Here, x has type X_1, y has type X_2, but they should be the same thing, 58 ;; so we need to replace all X_1's with X_2 59 ;; 60 ;; Here's the fixed rule, which is implemented here 61 ;; 62 ;; Γ ⊢ e_packed : {∃X_1,τ_body} 63 ;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e 64 ;; ------------------------------ 65 ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e 66 ;; 67 [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)] 68 [X [x ≫ x- : #,(subst #'X #'Y #'τ_body)] ⊢ e ≫ e- ⇒ τ_e] 69 -------- 70 [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])