fomega3.rkt (1341B)
1 #lang s-exp macrotypes/typecheck 2 (extends "fomega.rkt" #:except tyapp tyλ) 3 4 ;; NOTE 2017-02-03: currently not working 5 6 ; same as fomega2.rkt --- λ and #%app works as both regular and type versions, 7 ; → is both type and kind --- but reuses parts of fomega.rkt, 8 ; ie removes the duplication in fomega2.rkt 9 10 ;; System F_omega 11 ;; Type relation: 12 ;; - redefine current-kind? and current-type so #%app and λ 13 ;; work for both terms and types 14 ;; Types: 15 ;; - types from fomega.rkt 16 ;; - String from stlc+reco+var 17 ;; Terms: 18 ;; - extend ∀ Λ inst from fomega.rkt 19 ;; - #%datum from stlc+reco+var 20 21 ;; types and kinds are now mixed, due to #%app and λ 22 (begin-for-syntax 23 (define old-kind? (current-kind?)) 24 (current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k))))) 25 ;; Try to keep "type?" backward compatible with its uses so far, 26 ;; eg in the definition of λ or previous type constuctors. 27 ;; (However, this is not completely possible, eg define-type-alias) 28 ;; So now "type?" no longer validates types, rather it's a subset. 29 ;; But we no longer need type? to validate types, instead we can use 30 ;; (kind? (typeof t)) 31 (current-type? (λ (t) (or (type? t) 32 (let ([k (typeof t)]) 33 (or (★? k) (∀★? k))) 34 ((current-kind?) t)))))