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]])
|
|
|