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
28 lines
559 B
Racket
28 lines
559 B
Racket
#lang turnstile/lang
|
|
(extends "stlc+lit.rkt")
|
|
|
|
;; System F
|
|
;; Types:
|
|
;; - types from stlc+lit.rkt
|
|
;; - ∀
|
|
;; Terms:
|
|
;; - terms from stlc+lit.rkt
|
|
;; - Λ and inst
|
|
|
|
(provide (type-out ∀) Λ inst)
|
|
|
|
(define-binding-type ∀)
|
|
|
|
(define-typed-syntax (Λ (tv:id ...) e) ≫
|
|
[[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ]
|
|
--------
|
|
[⊢ e- ⇒ (∀ (tv- ...) τ)])
|
|
|
|
(define-typed-syntax inst
|
|
[(_ e τ:type ...) ≫
|
|
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
|
|
--------
|
|
[⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
|
|
[(_ e) ≫ --- [≻ e]])
|
|
|