commit 35c7900463b28c093b06c9ec73a1193c31c1242a
parent 3c769179eb62be822ff55c1a1475736803d7727e
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 20 Jun 2016 15:25:13 -0400
implement sysf and fsub with typed-lang-builder
Diffstat:
4 files changed, 127 insertions(+), 3 deletions(-)
diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../fsub.rkt"
+#lang s-exp "../typed-lang-builder/fsub.rkt"
(require "rackunit-typechecking.rkt")
;; examples from tapl ch26, bounded quantification
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../sysf.rkt"
+#lang s-exp "../typed-lang-builder/sysf.rkt"
(require "rackunit-typechecking.rkt")
(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
@@ -27,7 +27,7 @@
(typecheck-fail
(inst 1 Int)
#:with-msg
- "Expected expression 1 to have ∀ type, got: Int")
+ "Expected ∀ type, got: Int")
;; polymorphic arguments
(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))
diff --git a/tapl/typed-lang-builder/fsub.rkt b/tapl/typed-lang-builder/fsub.rkt
@@ -0,0 +1,92 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+reco+sub.rkt" #:except +)
+(require (rename-in (only-in "sysf.rkt" ∀? ∀ ~∀) [~∀ ~sysf:∀] [∀ sysf:∀]))
+
+;; System F<:
+;; Types:
+;; - types from sysf.rkt and stlc+reco+sub
+;; - extend ∀ with bounds
+;; Terms:
+;; - terms from sysf.rkt and stlc+reco+sub
+;; - extend Λ and inst
+;; - redefine + with Nat
+;; Other
+;; - current-promote, expose
+;; - extend current-sub? to call current-promote
+
+(define-primop + : (→ Nat Nat Nat))
+
+; can't just call expose in type-eval,
+; otherwise typevars will have bound as type, rather than instantiated type
+; only need expose during
+; 1) subtype checking
+; 2) pattern matching -- including base types
+(begin-for-syntax
+ (define (expose t)
+ (cond [(identifier? t)
+ (define sub (typeof t #:tag '<:))
+ (if sub (expose sub) t)]
+ [else t]))
+ (current-promote expose)
+ (define stlc:sub? (current-sub?))
+ (define (sub? t1 t2)
+ (stlc:sub? ((current-promote) t1) t2))
+ (current-sub? sub?)
+ (current-typecheck-relation (current-sub?)))
+
+; quasi-kind, but must be type constructor because its arguments are types
+(define-type-constructor <: #:arity >= 0)
+(begin-for-syntax
+ (current-type? (λ (t) (or (type? t) (<:? (typeof t))))))
+
+;; Type annotations used in two places:
+;; 1) typechecking the body of
+;; 2) instantiation of ∀
+;; Problem: need type annotations, even in expanded form
+;; Solution: store type annotations in a (quasi) kind <:
+(define-typed-syntax ∀ #:datum-literals (<:)
+ [(∀ ([tv:id <: τ:type] ...) τ_body) ▶
+ --------
+ ; eval first to overwrite the old #%type
+ [⊢ [[_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body))] ⇒ (: (<: τ.norm ...))]]])
+(begin-for-syntax
+ (define-syntax ~∀
+ (pattern-expander
+ (syntax-parser #:datum-literals (<:) #:literals (...)
+ [(_ ([tv:id <: τ_sub] ooo:...) τ)
+ #'(~and ∀τ
+ (~parse (~sysf:∀ (tv ooo) τ) #'∀τ)
+ (~parse (~<: τ_sub ooo) (typeof #'∀τ)))]
+ [(_ . args)
+ #'(~and ∀τ
+ (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
+ (~parse (~<: τ_sub (... ...)) (typeof #'∀τ))
+ (~parse args #'(([tv τ_sub] (... ...)) τ)))])))
+ (define-syntax ~∀*
+ (pattern-expander
+ (syntax-parser #:datum-literals (<:)
+ [(_ . args)
+ #'(~or
+ (~∀ . args)
+ (~and any (~do
+ (type-error
+ #:src #'any
+ #:msg "Expected ∀ type, got: ~a" #'any))))]))))
+
+(define-typed-syntax Λ #:datum-literals (<:)
+ [(Λ ([tv:id <: τsub:type] ...) e) ▶
+ ;; NOTE: store the subtyping relation of tv and τsub in the
+ ;; environment with a syntax property using another tag: '<:
+ ;; The "expose" function looks for this tag to enforce the bound,
+ ;; as in TaPL (fig 28-1)
+ [([tv : #%type <: τsub ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+ --------
+ [⊢ [[_ ≫ e-] ⇒ (: (∀ ([tv- <: τsub] ...) τ_e))]]])
+(define-typed-syntax inst
+ [(inst e τ:type ...) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~∀ ([tv <: τ_sub] ...) τ_body))]]
+ [τ.norm τ⊑ τ_sub] ...
+ [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
+ --------
+ [⊢ [[_ ≫ e-] ⇒ (: τ_inst)]]])
+
diff --git a/tapl/typed-lang-builder/sysf.rkt b/tapl/typed-lang-builder/sysf.rkt
@@ -0,0 +1,32 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+lit.rkt")
+(reuse #:from "stlc+rec-iso.rkt") ; want this type=?
+
+;; System F
+;; Type relation:
+;; - extend type=? with ∀
+;; Types:
+;; - types from stlc+lit.rkt
+;; - ∀
+;; Terms:
+;; - terms from stlc+lit.rkt
+;; - Λ and inst
+
+(define-type-constructor ∀ #:bvs >= 0)
+
+(define-typed-syntax Λ
+ [(Λ (tv:id ...) e) ▶
+ [([tv : #%type ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ (: τ)]]
+ --------
+ [⊢ [[_ ≫ e-] ⇒ (: (∀ (tv- ...) τ))]]])
+
+(define-typed-syntax inst
+ [(inst e τ:type ...) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~∀ tvs τ_body))]]
+ [#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)]
+ --------
+ [⊢ [[_ ≫ e-] ⇒ (: τ_inst)]]]
+ [(inst e) ▶
+ --------
+ [_ ≻ e]])
+
