commit 2278adcf959a1164129f99ca27da612c67c98aed
parent cb7a49ab0642db517e980c4efd8ade4cae3dbeeb
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 1 Oct 2015 16:21:29 -0400
replace provide/requires with "extends...except"/"reuse...from" forms
- introduce basic define-typed-syntax instead of define-syntax
- add fomega3 --- same as fomega2, without the duplication
- app and lam are both types and terms
- arrow is both type and kind
- same tests as fomega2
Diffstat:
20 files changed, 712 insertions(+), 504 deletions(-)
diff --git a/tapl/README.md b/tapl/README.md
@@ -9,11 +9,12 @@ A file extends its immediate parent file.
- stlc+reco+var.rkt
- stlc+cons.rkt
- stlc+box.rkt
- - stlc+rec-iso.rkt
- - exist.rkt
+ - exist.rkt (and type=? from stlc+rec-iso)
+ - stlc+rec-iso.rkt (and variants from stlc+reco+var)
- stlc+sub.rkt
- stlc+reco+sub.rkt (also pull in tup from stlc+reco+var.rkt)
- sysf.rkt
- - fsub.rkt
+ - fsub.rkt (also stlc+reco+sub)
- fomega.rkt
+ - fomega3.rkt
- fomega2.rkt
\ No newline at end of file
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -1,35 +1,29 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "stlc+reco+var.rkt" #%app λ let)
- (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let))
- (only-in "stlc+rec-iso.rkt")) ; to get current-type=?
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let))
-(provide ∃ pack open)
+(extends "stlc+reco+var.rkt")
+(reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=?
;; existential types
-;; combine type=? from sysf (for lam, ie ∃) and stlc+reco+var (for strings)
;; Types:
;; - types from stlc+reco+var.rkt
;; - ∃
;; Terms:
;; - terms from stlc+reco+var.rkt
;; - pack and open
+;; Other: type=? from stlc+rec-iso.rkt
(define-type-constructor ∃ #:arity = 1 #:bvs = 1)
-(define-syntax (pack stx)
- (syntax-parse stx
- [(_ (τ:type e) as ∃τ:type)
- #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
- #:with [e- τ_e] (infer+erase #'e)
- #:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
- (⊢ e- : ∃τ.norm)]))
+(define-typed-syntax pack
+ [(_ (τ:type e) as ∃τ:type)
+ #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
+ #:with [e- τ_e] (infer+erase #'e)
+ #:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
+ (⊢ e- : ∃τ.norm)])
-(define-syntax (open stx)
- (syntax-parse stx #:datum-literals (<=)
- [(_ ([(tv:id x:id) <= e_packed]) e)
- #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
+(define-typed-syntax open #:datum-literals (<=)
+ [(_ ([(tv:id x:id) <= e_packed]) e)
+ #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
;; Leveraging the macro system's management of binding reveals this.
@@ -73,8 +67,8 @@
;; ------------------------------
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
;;
- #:with [_ (x-) (e-) (τ_e)]
- (infer #'(e)
- #:tvctx #'([tv : #%type])
- #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
- (⊢ (let ([x- e_packed-]) e-) : τ_e)]))
-\ No newline at end of file
+ #:with [_ (x-) (e-) (τ_e)]
+ (infer #'(e)
+ #:tvctx #'([tv : #%type])
+ #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
+ (⊢ (let ([x- e_packed-]) e-) : τ_e)])
+\ No newline at end of file
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -1,17 +1,6 @@
#lang s-exp "typecheck.rkt"
-;; prefix-in an identifier if:
-;; - it will be extended, eg #%datum
-;; - want to use racket's version in implemetation (this) file, eg #%app
-(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))
- (except-in "stlc+lit.rkt" #%app #%datum))
-(provide (rename-out [datum/tc #%datum]
- [stlc:#%app #%app]
- [and/tc and] [or/tc or] [if/tc if]
- [begin/tc begin]
- [let/tc let] [let*/tc let*] [letrec/tc letrec])
- ann)
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum)
- (for-syntax current-join))
+(extends "stlc+lit.rkt" #:except #%datum)
+(provide (for-syntax current-join))
;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
;; Types:
@@ -31,11 +20,10 @@
(define-base-type Bool)
(define-base-type String)
-(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . b:boolean) (⊢ (#%datum . b) : Bool)]
- [(_ . s:str) (⊢ (#%datum . s) : String)]
- [(_ . x) #'(stlc:#%datum . x)]))
+(define-typed-syntax #%datum
+ [(_ . b:boolean) (⊢ (#%datum . b) : Bool)]
+ [(_ . s:str) (⊢ (#%datum . s) : String)]
+ [(_ . x) #'(stlc+lit:#%datum . x)])
(define-primop zero? : (→ Int Bool))
(define-primop = : (→ Int Int Bool))
@@ -44,83 +32,76 @@
(define-primop sub1 : (→ Int Int))
(define-primop not : (→ Bool Bool))
-(define-syntax (and/tc stx)
- (syntax-parse stx
- [(_ e1 e2)
- #:with e1- (⇑ e1 as Bool)
- #:with e2- (⇑ e2 as Bool)
- (⊢ (and e1- e2-) : Bool)]))
+(define-typed-syntax and
+ [(_ e1 e2)
+ #:with e1- (⇑ e1 as Bool)
+ #:with e2- (⇑ e2 as Bool)
+ (⊢ (and e1- e2-) : Bool)])
-(define-syntax (or/tc stx)
- (syntax-parse stx
- [(_ e1 e2)
- #:with e1- (⇑ e1 as Bool)
- #:with e2- (⇑ e2 as Bool)
- (⊢ (or e1- e2-) : Bool)]))
+(define-typed-syntax or
+ [(_ e1 e2)
+ #:with e1- (⇑ e1 as Bool)
+ #:with e2- (⇑ e2 as Bool)
+ (⊢ (or e1- e2-) : Bool)])
(begin-for-syntax
(define current-join (make-parameter (λ (x y) x))))
-(define-syntax (if/tc stx)
- (syntax-parse stx
- [(_ e_tst e1 e2)
- #:with e_tst- (⇑ e_tst as Bool)
- #:with (e1- τ1) (infer+erase #'e1)
- #:with (e2- τ2) (infer+erase #'e2)
- #:with τ-out ((current-join) #'τ1 #'τ2)
- #:fail-unless (and (typecheck? #'τ1 #'τ-out)
- (typecheck? #'τ2 #'τ-out))
- (format "branches have incompatible types: ~a and ~a"
- (type->str #'τ1) (type->str #'τ2))
- (⊢ (if e_tst- e1- e2-) : τ-out)]))
+(define-typed-syntax if
+ [(_ e_tst e1 e2)
+ #:with e_tst- (⇑ e_tst as Bool)
+ #:with (e1- τ1) (infer+erase #'e1)
+ #:with (e2- τ2) (infer+erase #'e2)
+ #:with τ-out ((current-join) #'τ1 #'τ2)
+ #:fail-unless (and (typecheck? #'τ1 #'τ-out)
+ (typecheck? #'τ2 #'τ-out))
+ (format "branches have incompatible types: ~a and ~a"
+ (type->str #'τ1) (type->str #'τ2))
+ (⊢ (if e_tst- e1- e2-) : τ-out)])
(define-base-type Unit)
(define-primop void : (→ Unit))
-(define-syntax (begin/tc stx)
- (syntax-parse stx
- [(_ e_unit ... e)
- #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
- #:with (e- τ) (infer+erase #'e)
- (⊢ (begin e_unit- ... e-) : τ)]))
+(define-typed-syntax begin
+ [(_ e_unit ... e)
+ #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
+ #:with (e- τ) (infer+erase #'e)
+ (⊢ (begin e_unit- ... e-) : τ)])
-(define-syntax (ann stx)
- (syntax-parse stx #:datum-literals (:)
- [(_ e : ascribed-τ:type)
- #:with (e- τ) (infer+erase #'e)
- #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
- (format "~a does not have type ~a\n"
- (syntax->datum #'e) (syntax->datum #'ascribed-τ))
- (⊢ e- : ascribed-τ)]))
+(define-typed-syntax ann
+ #:datum-literals (:)
+ [(_ e : ascribed-τ:type)
+ #:with (e- τ) (infer+erase #'e)
+ #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
+ (format "~a does not have type ~a\n"
+ (syntax->datum #'e) (syntax->datum #'ascribed-τ))
+ (⊢ e- : ascribed-τ)])
-(define-syntax (let/tc stx)
- (syntax-parse stx
- [(_ ([x e] ...) e_body)
- #:with ((e- τ) ...) (infers+erase #'(e ...))
- #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'e_body)
- (⊢ (let ([x- e-] ...) e_body-) : τ_body)]))
+(define-typed-syntax let/tc #:export-as let
+ [(_ ([x e] ...) e_body)
+ #:with ((e- τ) ...) (infers+erase #'(e ...))
+ #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'e_body)
+ (⊢ (let ([x- e-] ...) e_body-) : τ_body)])
-(define-syntax (let*/tc stx)
- (syntax-parse stx
- [(_ () e_body) #'e_body]
- [(_ ([x e] [x_rst e_rst] ...) e_body)
- #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))]))
+(define-typed-syntax let*/tc #:export-as let*
+ [(_ () e_body) #'e_body]
+ [(_ ([x e] [x_rst e_rst] ...) e_body)
+ #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))])
-(define-syntax (letrec/tc stx)
- (syntax-parse stx
- [(_ ([b:type-bind e] ...) e_body)
- #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
- (infers/ctx+erase #'(b ...) #'(e ... e_body))
- #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
- (string-append
- "type check fail, args have wrong type:\n"
- (string-join
- (stx-map
- (λ (e τ τ-expect)
- (format
- "~a has type ~a, expected ~a"
- (syntax->datum e) (type->str τ) (type->str τ-expect)))
- #'(e ...) #'(τ ...) #'(b.type ...))
- "\n"))
- (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)]))
+(define-typed-syntax letrec
+ [(_ ([b:type-bind e] ...) e_body)
+ #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
+ (infers/ctx+erase #'(b ...) #'(e ... e_body))
+ #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
+ (string-append
+ "type check fail, args have wrong type:\n"
+ (string-join
+ (stx-map
+ (λ (e τ τ-expect)
+ (format
+ "~a has type ~a, expected ~a"
+ (syntax->datum e) (type->str τ) (type->str τ-expect)))
+ #'(e ...) #'(τ ...) #'(b.type ...))
+ "\n"))
+ (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)])
\ No newline at end of file
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,38 +1,36 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
- (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
- [sysf:~∀ ~sysf:∀])
- (only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
-(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ tyλ tyapp)
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
;; System F_omega
;; Type relation:
;; Types:
;; - types from sysf.rkt
+;; - String from stlc+reco+var
;; Terms:
-;; - terms from sysf.rkt
+;; - extend ∀ Λ inst from sysf
+;; - add tyλ and tyapp
+;; - #%datum from stlc+reco+var
(define-syntax-category kind)
(begin-for-syntax
(current-kind? (λ (k) (or (#%type? k) (kind? k))))
- ;; Try to keep "type?" remain backward compatible with its uses so far,
+ ;; 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) (★? (typeof t)) (∀★? (typeof t)) #;(kind? (typeof t))))))
-; must override
+; must override, to handle kinds
(provide define-type-alias)
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
- #:with (τ- k_τ) (infer+erase #'τ)
- #:fail-unless (kind? #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
- #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
+ #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+ #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
+ #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
(begin-for-syntax
(define sysf:type-eval (current-type-eval))
@@ -60,14 +58,13 @@
(define-kind-constructor ⇒ #:arity >= 1)
(define-kind-constructor ∀★ #:arity >= 0)
-(define-syntax (∀ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx τ_body)
- ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
- #:with (tvs- τ_body- k_body)
- (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
- ; expand so kind gets overwritten
- (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
+(define-typed-syntax ∀ #:export-as ∀
+ [(_ bvs:kind-ctx τ_body)
+ ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
+ #:with (tvs- τ_body- k_body)
+ (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ ; expand so kind gets overwritten
+ (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@@ -106,53 +103,49 @@
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx e)
- #:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
- (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
+(define-typed-syntax Λ
+ [(_ bvs:kind-ctx e)
+ #:with ((tv- ...) e- τ_e)
+ (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
-(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ ...)
- #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
- #:with ([τ- k_τ] ...)
- (infers+erase #'(τ ...) #:expand (current-type-eval))
- #:when (stx-andmap
- (λ (t k) (or ((current-kind?) k)
- (type-error #:src t #:msg "not a valid type: ~a" t)))
- #'(τ ...) #'(k_τ ...))
- #:when (typechecks? #'(k_τ ...) #'(k ...))
- (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
+(define-typed-syntax inst
+ [(_ e τ ...)
+ #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
+ #:with ([τ- k_τ] ...)
+ (infers+erase #'(τ ...) #:expand (current-type-eval))
+ #:when (stx-andmap
+ (λ (t k) (or ((current-kind?) k)
+ (type-error #:src t #:msg "not a valid type: ~a" t)))
+ #'(τ ...) #'(k_τ ...))
+ #:when (typechecks? #'(k_τ ...) #'(k ...))
+ (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))])
;; TODO: merge with regular λ and app?
;; - see fomega2.rkt
-(define-syntax (tyλ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx τ_body)
- #:with (tvs- τ_body- k_body)
- (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
- #:when ((current-kind?) #'k_body)
- (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
+(define-typed-syntax tyλ
+ [(_ bvs:kind-ctx τ_body)
+ #:with (tvs- τ_body- k_body)
+ (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ #:when ((current-kind?) #'k_body)
+ (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
-(define-syntax (tyapp stx)
- (syntax-parse stx
- [(_ τ_fn τ_arg ...)
- #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'τ_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(τ_arg ...))
- (stx-map type->str #'(k_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(k_in ...)))
- (string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
-\ No newline at end of file
+(define-typed-syntax tyapp #:export-as tyapp
+ [(_ τ_fn τ_arg ...)
+ #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+ #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
+ #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
+ (string-append
+ (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'τ_fn))
+ "or wrong number of arguments:\nGiven:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(τ_arg ...))
+ (stx-map type->str #'(k_arg ...)))
+ "\n" #:after-last "\n")
+ (format "Expected: ~a arguments with type(s): "
+ (stx-length #'(k_in ...)))
+ (string-join (stx-map type->str #'(k_in ...)) ", "))
+ (⊢ (#%app τ_fn- τ_arg- ...) : k_out)])
+\ No newline at end of file
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -1,27 +1,25 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
- (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
- [sysf:~∀ ~sysf:∀])
- (only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
-(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ)
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
-; same as fomega except here λ and #%app works as both regular and type versions
-;; uses definition from stlc, but tweaks type? and kind? predicates
+; same as fomega.rkt except here λ and #%app works as both type and terms
+; - uses definition from stlc, but tweaks type? and kind? predicates
+;; → is also both type and kind
;; System F_omega
;; Type relation:
;; Types:
;; - types from sysf.rkt
+;; - String from stlc+reco+var
;; Terms:
-;; - terms from sysf.rkt
+;; - extend ∀ Λ inst from sysf
+;; - #%datum from stlc+reco+var
(define-syntax-category kind)
(begin-for-syntax
(current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
- ;; Try to keep "type?" remain backward compatible with its uses so far,
+ ;; 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.
@@ -60,16 +58,14 @@
(current-type-eval type-eval))
(define-base-kind ★)
-(define-kind-constructor ⇒ #:arity >= 1)
(define-kind-constructor ∀★ #:arity >= 0)
-(define-syntax (∀ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx τ_body)
- ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
- ; expand so kind gets overwritten
- (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
+(define-typed-syntax ∀ #:export-as ∀
+ [(_ bvs:kind-ctx τ_body)
+ ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
+ #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ ; expand so kind gets overwritten
+ (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@@ -108,20 +104,18 @@
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx e)
- #:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
- (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
+(define-typed-syntax Λ
+ [(_ bvs:kind-ctx e)
+ #:with ((tv- ...) e- τ_e)
+ (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
-(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ ...)
- #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
- #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
- #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
- (type-error #:src t #:msg "not a valid type: ~a" t)))
- #'(τ ...) #'(k_τ ...))
- #:when (typechecks? #'(k_τ ...) #'(k ...))
- (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]))
-\ No newline at end of file
+(define-typed-syntax inst
+ [(_ e τ ...)
+ #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
+ #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
+ #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
+ (type-error #:src t #:msg "not a valid type: ~a" t)))
+ #'(τ ...) #'(k_τ ...))
+ #:when (typechecks? #'(k_τ ...) #'(k ...))
+ (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))])
+\ No newline at end of file
diff --git a/tapl/fomega3.rkt b/tapl/fomega3.rkt
@@ -0,0 +1,53 @@
+#lang s-exp "typecheck.rkt"
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
+(reuse current-kind? ∀★ ∀★? ★ ★? kind? ∀ Λ inst define-type-alias #:from "fomega.rkt")
+
+; 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
+ (current-kind? (λ (k) (or (#%type? k) (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)))))
+
+;; extend to handle #%app and λ used as both terms and types
+(begin-for-syntax
+ (define sysf:type-eval (current-type-eval))
+ ;; extend type-eval to handle tyapp
+ ;; - requires manually handling all other forms
+ (define (type-eval τ)
+ (beta (sysf:type-eval τ)))
+ (define (beta τ)
+ (syntax-parse τ
+ [((~literal #%plain-app) τ_fn τ_arg ...)
+ #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
+ ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+ [((~literal #%plain-lambda) (x ...) τ_body ...)
+ #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
+ (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
+ [((~literal #%plain-app) arg ...)
+ #:with (arg+ ...) (stx-map beta #'(arg ...))
+ (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
+ [_ τ]))
+ (current-type-eval type-eval))
+\ No newline at end of file
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -1,21 +1,15 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "stlc+reco+sub.rkt" #%app λ +)
- (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ))
- (only-in "sysf.rkt" ∀?)
- (prefix-in sysf: (only-in "sysf.rkt" ∀))
- (rename-in (only-in "sysf.rkt" ~∀) [~∀ ~sysf:∀]))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+reco+sub.rkt") stlc:#%app stlc:λ)
- (except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax ~sysf:∀)))
-(provide ∀ Λ inst)
+(extends "stlc+reco+sub.rkt" #:except +)
+(reuse ∀? [∀ sysf:∀] [~∀ ~sysf:∀] #:from "sysf.rkt")
;; System F<:
;; Types:
-;; - types from sysf.rkt
+;; - types from sysf.rkt and stlc+reco+sub
;; - extend ∀ with bounds
;; Terms:
-;; - terms from sysf.rkt
+;; - 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
@@ -50,11 +44,10 @@
;; 2) instantiation of ∀
;; Problem: need type annotations, even in expanded form
;; Solution: store type annotations in a (quasi) kind <:
-(define-syntax ∀
- (syntax-parser #:datum-literals (<:)
- [(_ ([tv:id <: τ:type] ...) τ_body)
- ; eval first to overwrite the old #%type
- (⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))]))
+(define-typed-syntax ∀ #:export-as ∀ #: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
@@ -79,20 +72,18 @@
#:src #'any
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
-(define-syntax (Λ stx)
- (syntax-parse stx #:datum-literals (<:)
- [(_ ([tv:id <: τsub:type] ...) e)
- ;; NOTE: store the subtyping relation of tv and τsub in another
- ;; "environment", ie, a syntax property with another tag: 'sub
- ;; The "expose" function looks for this tag to enforce the bound,
- ;; as in TaPL (fig 28-1)
- #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
- #:octx #'([tv : τsub] ...) #:tag 'sub)
- (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]))
-(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ:type ...)
- #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
- #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
- (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+(define-typed-syntax Λ #:datum-literals (<:)
+ [(_ ([tv:id <: τsub:type] ...) e)
+ ;; NOTE: store the subtyping relation of tv and τsub in another
+ ;; "environment", ie, a syntax property with another tag: 'sub
+ ;; The "expose" function looks for this tag to enforce the bound,
+ ;; as in TaPL (fig 28-1)
+ #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
+ #:octx #'([tv : τsub] ...) #:tag 'sub)
+ (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))])
+(define-typed-syntax inst
+ [(_ e τ:type ...)
+ #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
+ #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
+ (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))])
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -1,9 +1,5 @@
#lang s-exp "typecheck.rkt"
-(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app))
- (except-in "stlc+cons.rkt" #%app))
-(provide (rename-out [stlc:#%app #%app]))
-(provide (except-out (all-from-out "stlc+cons.rkt") stlc:#%app))
-(provide ref deref :=)
+(extends "stlc+cons.rkt")
;; Simply-Typed Lambda Calculus, plus mutable references
;; Types:
@@ -11,23 +7,21 @@
;; - Ref constructor
;; Terms:
;; - terms from stlc+cons.rkt
+;; - ref deref :=
(define-type-constructor Ref #:arity = 1)
-(define-syntax (ref stx)
- (syntax-parse stx
- [(_ e)
- #:with (e- τ) (infer+erase #'e)
- (⊢ (box e-) : (Ref τ))]))
-(define-syntax (deref stx)
- (syntax-parse stx
- [(_ e)
- #:with (e- (τ)) (⇑ e as Ref)
- (⊢ (unbox e-) : τ)]))
-(define-syntax (:= stx)
- (syntax-parse stx
- [(_ e_ref e)
- #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
- #:with (e- τ2) (infer+erase #'e)
- #:when (typecheck? #'τ1 #'τ2)
- (⊢ (set-box! e_ref- e-) : Unit)]))
-\ No newline at end of file
+(define-typed-syntax ref
+ [(_ e)
+ #:with (e- τ) (infer+erase #'e)
+ (⊢ (box e-) : (Ref τ))])
+(define-typed-syntax deref
+ [(_ e)
+ #:with (e- (τ)) (⇑ e as Ref)
+ (⊢ (unbox e-) : τ)])
+(define-typed-syntax :=
+ [(_ e_ref e)
+ #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
+ #:with (e- τ2) (infer+erase #'e)
+ #:when (typecheck? #'τ1 #'τ2)
+ (⊢ (set-box! e_ref- e-) : Unit)])
+\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -1,9 +1,5 @@
#lang s-exp "typecheck.rkt"
-(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app))
- (except-in "stlc+reco+var.rkt" #%app))
-(provide (rename-out [stlc:#%app #%app] [cons/tc cons]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app))
-(provide nil isnil head tail)
+(extends "stlc+reco+var.rkt")
;; Simply-Typed Lambda Calculus, plus cons
;; Types:
@@ -16,33 +12,25 @@
(define-type-constructor List #:arity = 1)
-(define-syntax (nil stx)
- (syntax-parse stx
- [(_ ~! τi:type-ann)
- (⊢ null : (List τi.norm))]
- [null:id
- #:fail-when #t (error 'nil "requires type annotation")
- #'null]))
-(define-syntax (cons/tc stx)
- (syntax-parse stx
- [(_ e1 e2)
- #:with (e1- τ1) (infer+erase #'e1)
- #:with (e2- (τ2)) (⇑ e2 as List)
- #:when (typecheck? #'τ1 #'τ2)
- (⊢ (cons e1- e2-) : (List τ1))]))
-(define-syntax (isnil stx)
- (syntax-parse stx
- [(_ e)
- #:with (e- _) (⇑ e as List)
- (⊢ (null? e-) : Bool)]))
-(define-syntax (head stx)
- (syntax-parse stx
- [(_ e)
- #:with (e- (τ)) (⇑ e as List)
- (⊢ (car e-) : τ)]))
-(define-syntax (tail stx)
- (syntax-parse stx
- [(_ e)
- #:with (e- τ-lst) (infer+erase #'e)
- #:when (List? #'τ-lst)
- (⊢ (cdr e-) : τ-lst)]))
-\ No newline at end of file
+(define-typed-syntax nil
+ [(_ ~! τi:type-ann) (⊢ null : (List τi.norm))]
+ [_:id #:fail-when #t (error 'nil "requires type annotation") #'(void)])
+(define-typed-syntax cons
+ [(_ e1 e2)
+ #:with (e1- τ1) (infer+erase #'e1)
+ #:with (e2- (τ2)) (⇑ e2 as List)
+ #:when (typecheck? #'τ1 #'τ2)
+ (⊢ (cons e1- e2-) : (List τ1))])
+(define-typed-syntax isnil
+ [(_ e)
+ #:with (e- _) (⇑ e as List)
+ (⊢ (null? e-) : Bool)])
+(define-typed-syntax head
+ [(_ e)
+ #:with (e- (τ)) (⇑ e as List)
+ (⊢ (car e-) : τ)])
+(define-typed-syntax tail
+ [(_ e)
+ #:with (e- τ-lst) (infer+erase #'e)
+ #:when (List? #'τ-lst)
+ (⊢ (cdr e-) : τ-lst)])
+\ No newline at end of file
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -1,10 +1,6 @@
#lang s-exp "typecheck.rkt"
-;(extends "stlc.rkt" #:impl-uses (→))
-(require (except-in "stlc.rkt" #%app)
- (prefix-in stlc: (only-in "stlc.rkt" #%app)))
-(provide (except-out (all-from-out "stlc.rkt") stlc:#%app))
-(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum])
- define-primop)
+(extends "stlc.rkt")
+(provide define-primop)
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@@ -33,9 +29,8 @@
(define-primop + : (→ Int Int Int))
-(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . n:integer) (⊢ (#%datum . n) : Int)]
- [(_ . x)
- #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
- #'(#%datum . x)]))
+(define-typed-syntax #%datum
+ [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+ [(_ . x)
+ #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
+ #'(#%datum . x)])
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -1,19 +1,18 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "stlc+tup.rkt" #%app λ) ; import tuples, not records
- (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ))
- (only-in "stlc+reco+var.rkt" ∨ var case define-type-alias define)) ; and variants
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+tup.rkt") stlc:#%app stlc:λ)
- (all-from-out "stlc+reco+var.rkt"))
-(provide μ fld unfld)
+(extends "stlc+tup.rkt")
+(reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt")
;; stlc + (iso) recursive types
;; Types:
-;; - types from stlc+reco+var.rkt
+;; - types from stlc+tup.rkt
+;; - also ∨ from stlc+reco+var
;; - μ
;; Terms:
-;; - terms from stlc+reco+var.rkt
-;; - fld/unfld
+;; - terms from stlc+tup.rkt
+;; - also var and case from stlc+reco+var
+;; - fld, unfld
+;; Other:
+;; - extend type=? to handle lambdas
(define-type-constructor μ #:arity = 1 #:bvs = 1)
@@ -24,9 +23,7 @@
; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
- [#;(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
- ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
- (((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1))
+ [(((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1))
((~literal #%plain-app) tycon2 ((~literal #%plain-lambda) (y:id ...) k2 ... t2)))
#:when ((current-type=?) #'tycon1 #'tycon2)
#:when (types=? #'(k1 ...) #'(k2 ...))
@@ -38,17 +35,15 @@
(current-type=? type=?)
(current-typecheck-relation type=?))
-(define-syntax (unfld stx)
- (syntax-parse stx
- [(_ τ:type-ann e)
- #:with (~μ* (tv) τ_body) #'τ.norm
- #:with [e- τ_e] (infer+erase #'e)
- #:when (typecheck? #'τ_e #'τ.norm)
- (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]))
-(define-syntax (fld stx)
- (syntax-parse stx
- [(_ τ:type-ann e)
- #:with (~μ* (tv) τ_body) #'τ.norm
- #:with [e- τ_e] (infer+erase #'e)
- #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
- (⊢ e- : τ.norm)]))
-\ No newline at end of file
+(define-typed-syntax unfld
+ [(_ τ:type-ann e)
+ #:with (~μ* (tv) τ_body) #'τ.norm
+ #:with [e- τ_e] (infer+erase #'e)
+ #:when (typecheck? #'τ_e #'τ.norm)
+ (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))])
+(define-typed-syntax fld
+ [(_ τ:type-ann e)
+ #:with (~μ* (tv) τ_body) #'τ.norm
+ #:with [e- τ_e] (infer+erase #'e)
+ #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
+ (⊢ e- : τ.norm)])
+\ No newline at end of file
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -1,14 +1,8 @@
#lang s-exp "typecheck.rkt"
+(extends "stlc+sub.rkt" #:except #%app #%datum)
+(extends "stlc+reco+var.rkt" #:except #%datum +)
;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
;; but extend sub? from stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum)
- (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum))
- (except-in "stlc+reco+var.rkt" #%app #%datum +)
- (prefix-in stlc+reco+var: (only-in "stlc+reco+var.rkt" #%datum)))
-(provide (rename-out [stlc+sub:#%app #%app]
- [datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum)
- (except-out (all-from-out "stlc+reco+var.rkt") stlc+reco+var:#%datum))
;; Simply-Typed Lambda Calculus, plus subtyping, plus records
;; Types:
@@ -16,12 +10,12 @@
;; Type relations:
;; - sub? extended to records
;; Terms:
-;; - terms from stlc+sub.rkt, can leave record form as is
+;; - terms from stlc+sub.rkt
+;; - records and variants from stlc+reco+var
-(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . n:number) #'(stlc+sub:#%datum . n)]
- [(_ . x) #'(stlc+reco+var:#%datum . x)]))
+(define-typed-syntax #%datum
+ [(_ . n:number) #'(stlc+sub:#%datum . n)]
+ [(_ . x) #'(stlc+reco+var:#%datum . x)])
(begin-for-syntax
(define old-sub? (current-sub?))
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -1,15 +1,7 @@
#lang s-exp "typecheck.rkt"
-(require (only-in racket/bool symbol=?))
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let × ×?))
- (except-in "stlc+tup.rkt" #%app begin tup proj let ×)
- (rename-in (only-in "stlc+tup.rkt" ~×) [~× ~stlc:×]))
-(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
- [define/tc define]))
-(provide (except-out (all-from-out "stlc+tup.rkt")
- stlc:#%app stlc:let stlc:begin stlc:×
- (for-syntax ~stlc:× stlc:×?)))
-(provide × tup proj ∨ var case)
-(provide (for-syntax same-types? ~× ~×* ~∨ ~∨*))
+(extends "stlc+tup.rkt" #:except × ×? tup proj
+ #:rename [~× ~stlc:×])
+(provide × ∨ (for-syntax same-types? ~× ~×* ~∨ ~∨*))
;; Simply-Typed Lambda Calculus, plus records and variants
@@ -39,14 +31,13 @@
[(_ alias:id τ:type)
#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
-(define-syntax (define/tc stx)
- (syntax-parse stx
- [(_ x:id e)
- #:with (e- τ) (infer+erase #'e)
- #:with y (generate-temporary)
- #'(begin
- (define-syntax x (make-rename-transformer (⊢ y : τ)))
- (define y e-))]))
+(define-typed-syntax define
+ [(_ x:id e)
+ #:with (e- τ) (infer+erase #'e)
+ #:with y (generate-temporary)
+ #'(begin
+ (define-syntax x (make-rename-transformer (⊢ y : τ)))
+ (define y e-))])
; re-define tuples as records
; dont use define-type-constructor because I want the : literal syntax
@@ -54,7 +45,7 @@
(syntax-parser #:datum-literals (:)
[(_ [label:id : τ:type] ...)
#:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
- #`(stlc:× valid-τ ...)]))
+ #`(stlc+tup:× valid-τ ...)]))
(begin-for-syntax
(define-syntax ~×
(pattern-expander
@@ -64,7 +55,7 @@
[(_ . args)
#'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...))
(~parse args #'((l τ_l) (... ...))))])))
- (define ×? stlc:×?)
+ (define ×? stlc+tup:×?)
(define-syntax ~×*
(pattern-expander
(syntax-parser #:datum-literals (:)
@@ -75,21 +66,19 @@
#:msg "Expected × type, got: ~a" #'any))))]))))
;; records
-(define-syntax (tup stx)
- (syntax-parse stx #:datum-literals (=)
- [(_ [l:id = e] ...)
- #:with ([e- τ] ...) (infers+erase #'(e ...))
- (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]))
-(define-syntax (proj stx)
- (syntax-parse stx #:literals (quote)
- [(_ e_rec l:id)
- #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
- #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
- (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]))
+(define-typed-syntax tup #:datum-literals (=)
+ [(_ [l:id = e] ...)
+ #:with ([e- τ] ...) (infers+erase #'(e ...))
+ (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))])
+(define-typed-syntax proj #:literals (quote)
+ [(_ e_rec l:id)
+ #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
+ #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
+ (⊢ (cadr (assoc 'l e_rec-)) : τ_match)])
(define-type-constructor ∨/internal)
-; re-define tuples as records
+;; variants
(define-syntax ∨
(syntax-parser #:datum-literals (:)
[(_ (~and [label:id : τ:type] x) ...)
@@ -122,27 +111,26 @@
#:msg "Expected ∨ type, got: ~a" #'any))))
~!)])))) ; dont backtrack here
-(define-syntax (var stx)
- (syntax-parse stx #:datum-literals (as =)
- [(_ l:id = e as τ:type)
- #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
- #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
- #:fail-unless (syntax-e #'match_res)
- (format "~a field does not exist" (syntax->datum #'l))
- #:with (_ τ_match) #'match_res
- #:with (e- τ_e) (infer+erase #'e)
- #:when (typecheck? #'τ_e #'τ_match)
- (⊢ (list 'l e) : τ)]))
-(define-syntax (case stx)
- (syntax-parse stx #:datum-literals (of =>)
- [(_ e [l:id x:id => e_l] ...)
- #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
- #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
- #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
- #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
- #:with (((x-) e_l- τ_el) ...)
- (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
- #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
- (⊢ (let ([l_e (car e-)])
- (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
- : #,(stx-car #'(τ_el ...)))]))
+(define-typed-syntax var #:datum-literals (as =)
+ [(_ l:id = e as τ:type)
+ #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
+ #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
+ #:fail-unless (syntax-e #'match_res)
+ (format "~a field does not exist" (syntax->datum #'l))
+ #:with (_ τ_match) #'match_res
+ #:with (e- τ_e) (infer+erase #'e)
+ #:when (typecheck? #'τ_e #'τ_match)
+ (⊢ (list 'l e) : τ)])
+(define-typed-syntax case
+ #:datum-literals (of =>)
+ [(_ e [l:id x:id => e_l] ...)
+ #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+ #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
+ #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+ #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
+ #:with (((x-) e_l- τ_el) ...)
+ (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+ #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+ (⊢ (let ([l_e (car e-)])
+ (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
+ : #,(stx-car #'(τ_el ...)))])
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -1,8 +1,5 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "stlc+lit.rkt" #%datum + #%app)
- (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)))
-(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
+(extends "stlc+lit.rkt" #:except #%datum +)
(provide (for-syntax subs? current-sub?))
;; Simply-Typed Lambda Calculus, plus subtyping
@@ -16,7 +13,9 @@
;; - Int <: Num
;; - →
;; Terms:
-;; - terms from stlc+lit.rkt, except redefined: app, datum, +
+;; - terms from stlc+lit.rkt, except redefined: datum and +
+;; - also *
+;; Other: sub? current-sub?
(define-base-type Top)
(define-base-type Num)
@@ -25,12 +24,11 @@
(define-primop + : (→ Num Num Num))
(define-primop * : (→ Num Num Num))
-(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
- [(_ . n:integer) (⊢ (#%datum . n) : Int)]
- [(_ . n:number) (⊢ (#%datum . n) : Num)]
- [(_ . x) #'(stlc:#%datum . x)]))
+(define-typed-syntax #%datum
+ [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
+ [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+ [(_ . n:number) (⊢ (#%datum . n) : Num)]
+ [(_ . x) #'(stlc+lit:#%datum . x)])
(begin-for-syntax
(define (sub? t1 t2)
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -1,9 +1,5 @@
#lang s-exp "typecheck.rkt"
-(require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app))
- (except-in "ext-stlc.rkt" #%app))
-(provide (rename-out [stlc:#%app #%app])
- tup proj)
-(provide (except-out (all-from-out "ext-stlc.rkt") stlc:#%app))
+(extends "ext-stlc.rkt")
;; Simply-Typed Lambda Calculus, plus tuples
;; Types:
@@ -15,15 +11,13 @@
(define-type-constructor ×) ; default arity >=0
-(define-syntax (tup stx)
- (syntax-parse stx
- [(_ e ...)
- #:with ([e- τ] ...) (infers+erase #'(e ...))
- (⊢ (list e- ...) : (× τ ...))]))
-(define-syntax (proj stx)
- (syntax-parse stx
- [(_ e_tup n:nat)
- #:with [e_tup- τs_tup] (⇑ e_tup as ×)
- #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
- (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
+(define-typed-syntax tup
+ [(_ e ...)
+ #:with ([e- τ] ...) (infers+erase #'(e ...))
+ (⊢ (list e- ...) : (× τ ...))])
+(define-typed-syntax proj
+ [(_ e_tup n:nat)
+ #:with [e_tup- τs_tup] (⇑ e_tup as ×)
+ #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
+ (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
\ No newline at end of file
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -1,7 +1,5 @@
#lang s-exp "typecheck.rkt"
-(provide (rename-out [λ/tc λ] [app/tc #%app]))
(provide (for-syntax current-type=? types=?))
-(provide #%module-begin #%top-interaction #%top require) ; useful racket forms
;; Simply-Typed Lambda Calculus
;; - no base types; can't write any terms
@@ -66,29 +64,27 @@
(define-type-constructor → #:arity >= 1)
-(define-syntax (λ/tc stx)
- (syntax-parse stx
- [(_ bvs:type-ctx e)
- #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
- (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))]))
+(define-typed-syntax λ
+ [(_ bvs:type-ctx e)
+ #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
+ (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))])
-(define-syntax (app/tc stx)
- (syntax-parse stx
- [(_ e_fn e_arg ...)
- #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
- #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
- #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in ...)))
- (string-join (stx-map type->str #'(τ_in ...)) ", "))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
+(define-typed-syntax #%app
+ [(_ e_fn e_arg ...)
+ #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
+ #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (string-append
+ (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e_fn))
+ "or wrong number of arguments:\nGiven:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (stx-map type->str #'(τ_arg ...)))
+ "\n" #:after-last "\n")
+ (format "Expected: ~a arguments with type(s): "
+ (stx-length #'(τ_in ...)))
+ (string-join (stx-map type->str #'(τ_in ...)) ", "))
+ (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -1,11 +1,7 @@
#lang s-exp "typecheck.rkt"
-(require (except-in "stlc+lit.rkt" #%app λ)
- (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ))
- (only-in "stlc+rec-iso.rkt")) ; want type=? from here
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ))
-(provide Λ inst)
-
+(extends "stlc+lit.rkt")
+(reuse #:from "stlc+rec-iso.rkt") ; want this type=?
+
;; System F
;; Type relation:
;; - extend type=? with ∀
@@ -18,13 +14,11 @@
(define-type-constructor ∀ #:arity = 1 #:bvs >= 0)
-(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ (tv:id ...) e)
- #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
- (⊢ e- : (∀ (tv- ...) τ))]))
-(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ:type ...)
- #:with (e- (tvs (τ_body))) (⇑ e as ∀)
- (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #;#'(tv ...) #'τ_body))]))
-\ No newline at end of file
+(define-typed-syntax Λ
+ [(_ (tv:id ...) e)
+ #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
+ (⊢ e- : (∀ (tv- ...) τ))])
+(define-typed-syntax inst
+ [(_ e τ:type ...)
+ #:with (e- (tvs (τ_body))) (⇑ e as ∀)
+ (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))])
+\ No newline at end of file
diff --git a/tapl/tests/fomega3-tests.rkt b/tapl/tests/fomega3-tests.rkt
@@ -0,0 +1,200 @@
+#lang s-exp "../fomega3.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+ : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (λ ([t : ★]) t) : (→ ★ ★))
+(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
+(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+
+(check-type ((λ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
+ : (→ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+ (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(check-type (inst
+ (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+ ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+ : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
+ ;#:with-msg "not a valid type: 1")
+
+;; applied f too early
+(typecheck-fail (inst
+ (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+ ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+ (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+ ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+ (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+ ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1))
+ ;#:with-msg "not a valid type: 1")
+(define-type-alias Id (λ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (→ ★ ★ ★))
+(check-type Pair : (→ ★ ★ (∀★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String)
+ : (→ Int String (Pair Int String)))
+; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1")
+ : (Pair Int String))
+; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X)))
+; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ : (→ (Pair Int String) Int))
+; apply fst
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : Int ⇒ 1)
+; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y)))
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ : (→ (Pair Int String) String))
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : String ⇒ "1")
+
+;;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+ (Λ ([s : ★]) (λ ([y : s]) y)))
+ : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+ : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -24,4 +24,5 @@
;; F_omega
(require "fomega-tests.rkt")
-(require "fomega2-tests.rkt")
-\ No newline at end of file
+(require "fomega2-tests.rkt")
+(require "fomega3-tests.rkt")
+\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -1,14 +1,15 @@
#lang racket/base
(require
- (for-syntax (except-in racket extends)
- syntax/parse racket/syntax syntax/stx
+ (for-syntax (except-in racket extends) (only-in srfi/13 string-prefix?)
+ syntax/parse racket/syntax syntax/stx racket/stxparam
"stx-utils.rkt"
syntax/parse/debug)
(for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
(for-meta 3 racket/base syntax/parse racket/syntax)
- racket/provide)
+ racket/bool racket/provide racket/require)
(provide
- (all-from-out racket/base)
+ symbol=?
+ (except-out (all-from-out racket/base) #%module-begin)
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
(all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
@@ -27,9 +28,35 @@
;; aliasing, is just free-identifier=?
;; - type constructors are prefix
+;; redefine #%module-begin to add some provides
+(provide (rename-out [mb #%module-begin]))
+(define-syntax (mb stx)
+ (syntax-parse stx
+ [(_ . stuff)
+ #'(#%module-begin
+ (provide #%module-begin #%top-interaction #%top require) ; useful racket forms
+ . stuff)]))
+
(struct exn:fail:type:runtime exn:fail:user ())
-;; require macro
+(define-for-syntax (drop-file-ext filename)
+ (car (string-split filename ".")))
+
+(begin-for-syntax
+ (define-syntax-parameter stx (syntax-rules ())))
+
+(define-syntax (define-typed-syntax stx)
+ (syntax-parse stx
+ [(_ name:id #:export-as out-name:id stx-parse-clause ...)
+ #'(begin
+ (provide (rename-out [name out-name]))
+ (define-syntax (name syntx)
+ (syntax-parameterize ([stx (syntax-id-rules () [_ syntx])])
+ (syntax-parse syntx stx-parse-clause ...))))]
+ [(_ name:id stx-parse-clause ...)
+ #`(define-typed-syntax #,(generate-temporary) #:export-as name
+ stx-parse-clause ...)]))
+
;; need options for
;; - pass through
;; - use (generated) prefix to avoid conflicts
@@ -41,19 +68,55 @@
(define-syntax extends
(syntax-parser
[(_ base-lang
- (~optional (~seq #:impl-uses (x ...)) #:defaults ([(x 1) null])))
- #:with pre (generate-temporary)
+ (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) #:defaults ([(x 1) null]))
+ (~optional (~seq #:rename [old new] ...) #:defaults ([(old 1) null][(new 1) null]))
+ (~optional (~seq #:prefix p ...) #:defaults ([(p 1) null])))
+ #:with pre (or (let ([dat (syntax-e #'base-lang)])
+ (and (string? dat)
+ (string->symbol (drop-file-ext dat))))
+ #'base-lang)
#:with pre: (format-id #'pre "~a:" #'pre)
- #'(begin
- (require (prefix-in pre: base-lang))
- (require (only-in base-lang x ...))
+ #:with internal-pre (generate-temporary)
+ #:with non-excluded-imports #'(except-in base-lang p ... x ... old ...)
+ #:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define)))
+ #:with not-conflicted? #'(λ (n) (and (not (conflicted? n)) n))
+ #`(begin
+ (require (prefix-in pre: (only-in base-lang p ... x ...))) ; prefixed
+ (require (rename-in (only-in base-lang old ...) [old new] ...))
+ (require (filtered-in not-conflicted? non-excluded-imports))
+ (require (filtered-in ; conflicted names, with (internal) prefix
+ (let ([conflicted-pre (symbol->string (syntax->datum #'internal-pre))])
+ (λ (name) (and (conflicted? name)
+ (string-append conflicted-pre name))))
+ non-excluded-imports))
(provide (filtered-out
- (let ([pre-pat (regexp (format "^~a" (syntax->datum #'pre:)))])
+ (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+ [int-pre-str #,(symbol->string (syntax->datum #'internal-pre))]
+ [pre-str-len (string-length pre-str)]
+ [int-pre-str-len (string-length int-pre-str)]
+ [drop-pre (λ (s) (substring s pre-str-len))]
+ [drop-int-pre (λ (s) (substring s int-pre-str-len))]
+ [excluded (map symbol->string (syntax->datum #'(x ... new ...)))])
(λ (name)
- (and (regexp-match? pre-pat name)
- (regexp-replace pre-pat name ""))))
+ (define out-name
+ (or (and (string-prefix? pre-str name)
+ (drop-pre name))
+ (and (string-prefix? int-pre-str name)
+ (drop-int-pre name))
+ name))
+ (and (not (member out-name excluded)) out-name)))
+ (all-from-out base-lang))
+ ))]))
+(define-syntax reuse
+ (syntax-parser
+ [(_ (~or x:id [old:id new:id]) ... #:from base-lang)
+ #`(begin
+ (require (rename-in (only-in base-lang x ... old ...) [old new] ...))
+ (provide (filtered-out
+ (let ([excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
+ (λ (n) (and (not (member n excluded)) n)))
(all-from-out base-lang))))]))
-
+
;; type assignment
(begin-for-syntax
;; Type assignment macro for nicer syntax
@@ -411,7 +474,7 @@
#:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
#:with name-ann (format-id #'name "~a-ann" #'name)
#'(begin
- (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann)
+ (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx)
#%tag define-base-name define-name-cons)
(define #%tag void)
(begin-for-syntax
