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
35 lines
1.3 KiB
Racket
35 lines
1.3 KiB
Racket
#lang turnstile/lang
|
|
(extends "fomega.rkt" #:except tyapp tyλ)
|
|
|
|
;; not current working 2017-02-03
|
|
|
|
; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
|
|
; → is both type and kind --- but reuses parts of fomega.rkt,
|
|
; ie removes the duplication in fomega2.rkt
|
|
|
|
;; System F_omega
|
|
;; Type relation:
|
|
;; - redefine current-kind? and current-type so #%app and λ
|
|
;; work for both terms and types
|
|
;; Types:
|
|
;; - types from fomega.rkt
|
|
;; - String from stlc+reco+var
|
|
;; Terms:
|
|
;; - extend ∀ Λ inst from fomega.rkt
|
|
;; - #%datum from stlc+reco+var
|
|
|
|
;; types and kinds are now mixed, due to #%app and λ
|
|
(begin-for-syntax
|
|
(define old-kind? (current-kind?))
|
|
(current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k)))))
|
|
;; Try to keep "type?" backward compatible with its uses so far,
|
|
;; eg in the definition of λ or previous type constuctors.
|
|
;; (However, this is not completely possible, eg define-type-alias)
|
|
;; So now "type?" no longer validates types, rather it's a subset.
|
|
;; But we no longer need type? to validate types, instead we can use
|
|
;; (kind? (typeof t))
|
|
(current-type? (λ (t) (or (type? t)
|
|
(let ([k (typeof t)])
|
|
(or (★? k) (∀★? k)))
|
|
((current-kind?) t)))))
|