115aae8e73
Previously, "type" functions were reused a lot to manipulate kinds, and other metadata defined via `define-syntax-category`, but this meant it was impossible to define separate behavior for some type and kind operations, e.g., type=? and kind=?. This commit defines a separate api for each `define-syntax-category` declaration. Also, every `define-syntax-category` defines a new `define-NAMEd-syntax` form, which implicitly uses the proper parameters, e.g., `define-kinded-syntax` uses `kindcheck?`, `current-kind-eval`, and the ':: kind key by default (whereas before, it was using typecheck?, type-eval, etc). This commit breaks backwards compatibility. The most likely breakage results from using a different default key for kinds. It used to be ':, the same as types, but now the default is '::. This commit also generalizes the contexts used with `define-NAMEd-syntax` and `infer`. - all contexts now accept arbitrary key-values associated with a variable - all contexts use let* semantics, where a binding is in scope for subsequent bindings; this means that one environment is sufficient in most scenarioes, e.g., type and term vars can be mixed (if properly ordered) - environments allow lone identifiers, which are treated as type variables by default
71 lines
2.5 KiB
Racket
71 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)]
|
|
[X [x ≫ x- : #,(subst #'X #'Y #'τ_body)] ⊢ e ≫ e- ⇒ τ_e]
|
|
--------
|
|
[⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])
|