1c0fa751d6
- document #:arg-variances and variances; #:arr - fixes #36 - start to split type constructor macro into (not working yet) - ty-: expands to expanded type representation - ty: performs kindchecking and expands to ty- - this makes it easier for programmers to implement their own kind system, but still get some turnstile conveniences like pat expanders
72 lines
2.5 KiB
Racket
72 lines
2.5 KiB
Racket
#lang turnstile/lang
|
|
(extends "stlc+reco+var.rkt")
|
|
|
|
;; existential types
|
|
;; Types:
|
|
;; - types from stlc+reco+var.rkt
|
|
;; - ∃
|
|
;; Terms:
|
|
;; - terms from stlc+reco+var.rkt
|
|
;; - pack and open
|
|
|
|
(provide ∃ pack open)
|
|
|
|
(define-binding-type ∃ #:bvs = 1)
|
|
|
|
(define-typed-syntax (pack (τ:type e) as ∃τ:type) ≫
|
|
#:with (~∃ (τ_abstract) τ_body) #'∃τ.norm
|
|
#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)
|
|
[⊢ e ≫ e- ⇐ τ_e]
|
|
--------
|
|
[⊢ e- ⇒ ∃τ.norm])
|
|
|
|
(define-typed-syntax (open [x:id (~datum <=) e_packed (~datum with) X:id] e) ≫
|
|
;; The subst below appears to be a hack, but it's not really.
|
|
;; It's the (TaPL) type rule itself that is fast and loose.
|
|
;; Leveraging the macro system's management of binding reveals this.
|
|
;;
|
|
;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366:
|
|
;; Γ ⊢ e_packed : {∃X,τ_body}
|
|
;; Γ,X,x:τ_body ⊢ e : τ_e
|
|
;; ------------------------------
|
|
;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e
|
|
;;
|
|
;; There's *two* separate binders, the ∃ and the let,
|
|
;; which the rule conflates.
|
|
;;
|
|
;; Here's the rule rewritten to distinguish the two binding positions:
|
|
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
|
;; Γ,X_???,x:τ_body ⊢ e : τ_e
|
|
;; ------------------------------
|
|
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
|
;;
|
|
;; The X_1 binds references to X in T_12.
|
|
;; The X_2 binds references to X in t_2.
|
|
;; What should the X_??? be?
|
|
;;
|
|
;; A first guess might be to replace X_??? with both X_1 and X_2,
|
|
;; so all the potentially referenced type vars are bound.
|
|
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
|
;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e
|
|
;; ------------------------------
|
|
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
|
;;
|
|
;; But this example demonstrates that the rule above doesnt work:
|
|
;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2]
|
|
;; ((λ ([y : X_2]) y) x)
|
|
;; Here, x has type X_1, y has type X_2, but they should be the same thing,
|
|
;; so we need to replace all X_1's with X_2
|
|
;;
|
|
;; Here's the fixed rule, which is implemented here
|
|
;;
|
|
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
|
;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e
|
|
;; ------------------------------
|
|
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
|
;;
|
|
[⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)]
|
|
#:with τ_x (subst #'X #'Y #'τ_body)
|
|
[([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
|
|
--------
|
|
[⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])
|