commit 6feff7d3b372d1aa71700a717ba9455029d13529
parent 1a831454f467d7ade5bc3ca01f24c0ad7f1387cc
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 19 Aug 2015 19:29:07 -0400
completed: type valiation; new type constructor pattern matching
Diffstat:
24 files changed, 956 insertions(+), 595 deletions(-)
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -1,12 +1,10 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
- (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let #;type=?))
+ (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let))
(only-in "stlc+rec-iso.rkt" type=?))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
- #;(for-syntax type=?))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
- #;(for-syntax stlc: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)
(all-from-out "stlc+rec-iso.rkt"))
(provide ∃ pack open)
@@ -28,29 +26,34 @@
#;(define-type-constructor (∃ [[X]] τ_body))
+(define-basic-checked-stx ∃ #:arity = 1 #:bvs = 1)
; this is exactly the same as μ
-(define-syntax ∃
- (syntax-parser
- [(_ (tv:id) τ_body)
- #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
- #:when (#%type? #'k)
- (mk-type #'(λ (tv-) τ_body-))]))
-(begin-for-syntax
- (define (infer∃+erase e)
- (syntax-parse (infer+erase e) #:context e
- [(e- τ_e)
- #:with ((~literal #%plain-lambda) (tv) τ) #'τ_e
- #'(e- (tv τ))]))
- (define-syntax ~∃*
- (pattern-expander
- (syntax-parser
- [(_ (tv:id) τ)
- #'(~or
- ((~literal #%plain-lambda) (tv) τ)
- (~and any (~do
- (type-error
- #:src #'any
- #:msg "Expected ∃ type, got: ~a" #'any))))]))))
+;(define-syntax ∃
+; (syntax-parser
+; [(_ (tv:id) τ_body)
+; #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
+; #:when (#%type? #'k)
+; (mk-type #'(λ (tv-) τ_body-))]))
+;(begin-for-syntax
+; #;(define (infer∃+erase e)
+; (syntax-parse (infer+erase e) #:context e
+; [(e- τ_e)
+; #:with ((~literal #%plain-lambda) (tv) τ) #'τ_e
+; #'(e- (tv τ))]))
+; (define-syntax ~∃
+; (pattern-expander
+; (syntax-parser
+; [(_ (tv:id) τ)
+; #'((~literal #%plain-lambda) (tv) τ)])))
+; (define-syntax ~∃*
+; (pattern-expander
+; (syntax-parser
+; [(_ (tv:id) τ)
+; #'(~or (~∃ (tv) τ)
+; (~and any (~do
+; (type-error
+; #:src #'any
+; #:msg "Expected ∃ type, got: ~a" #'any))))]))))
(define-syntax (pack stx)
(syntax-parse stx
@@ -64,7 +67,11 @@
(define-syntax (open stx)
(syntax-parse stx #:datum-literals (<=)
[(_ ([(tv:id x:id) <= e_packed]) e)
- #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
+; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
+; #:when (displayln #'τ_packed)
+; #:with (~∃ (τ_abstract) τ_body) #'τ_packed
+ #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
+; #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
;; The subst below appears to be a hack, but it's not really.
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -47,8 +47,10 @@
(define-syntax (and/tc stx)
(syntax-parse stx
[(_ e1 e2)
- #:with e1- (inferBool+erase #'e1)
- #:with e2- (inferBool+erase #'e2)
+; #:with e1- (inferBool+erase #'e1)
+; #:with e2- (inferBool+erase #'e2)
+ #:with e1- (⇑ e1 as Bool)
+ #:with e2- (⇑ e2 as Bool)
; #:with (e1- τ1) (infer+erase #'e1)
; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
; #:with (e2- τ2) (infer+erase #'e2)
@@ -58,8 +60,10 @@
(define-syntax (or/tc stx)
(syntax-parse stx
[(_ e1 e2)
- #:with e1- (inferBool+erase #'e1)
- #:with e2- (inferBool+erase #'e2)
+; #:with e1- (inferBool+erase #'e1)
+; #:with e2- (inferBool+erase #'e2)
+ #:with e1- (⇑ e1 as Bool)
+ #:with e2- (⇑ e2 as Bool)
; #:with (e1- τ1) (infer+erase #'e1)
; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
; #:with (e2- τ2) (infer+erase #'e2)
@@ -69,13 +73,13 @@
(define-syntax (if/tc stx)
(syntax-parse stx
[(_ e_tst e1 e2)
- #:with e_tst- (inferBool+erase #'e_tst)
+ #:with e_tst- (⇑ e_tst as Bool)
; #:with (e_tst- τ_tst) (infer+erase #'e_tst)
; #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
#:with (e1- τ1) (infer+erase #'e1)
#:with (e2- τ2) (infer+erase #'e2)
- #:fail-unless (or ((current-typecheck-relation) #'τ1 #'τ2)
- ((current-typecheck-relation) #'τ2 #'τ1))
+ #:fail-unless (or (typecheck? #'τ1 #'τ2)
+ (typecheck? #'τ2 #'τ1))
(format "branches must have the same type: given ~a and ~a"
(type->str #'τ1) (type->str #'τ2))
(⊢ (if e_tst- e1- e2-) : τ1)]))
@@ -86,7 +90,8 @@
(define-syntax (begin/tc stx)
(syntax-parse stx
[(_ e_unit ... e)
- #:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+ ;#:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+ #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
; #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
; #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
; (string-append
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,13 +1,15 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + type-eval)
- (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval))
+ (prefix-in sysf: (only-in "sysf.rkt" type-eval))
(only-in "stlc+reco+var.rkt" same-types?))
(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
-(provide (except-out (all-from-out "sysf.rkt")
+#;(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
sysf:#%app sysf:λ
(for-syntax sysf:type-eval)))
+(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval))
+ (all-from-out "stlc+reco+var.rkt"))
(provide Int → ∀ inst Λ tyλ tyapp
(for-syntax type-eval))
@@ -18,11 +20,15 @@
;; Terms:
;; - terms from sysf.rkt
+(define-syntax-category kind)
+
(provide define-type-alias)
(define-syntax define-type-alias
(syntax-parser
- [(_ alias:id τ:type)
- #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
+ [(_ 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 #'τ-]))]))
(begin-for-syntax
;; extend type-eval to handle tyapp
@@ -33,23 +39,26 @@
#:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
#:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
(substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
- [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- [((~literal tyλ) _ ...) (sysf:type-eval τ)]
- [((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ [((~or (~literal ∀)(~literal →)
+ (~literal ⇒)(~literal tyapp)) . _)
+ ((current-type-eval) (sysf:type-eval τ))]
+ ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ ;[((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ ;[((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ ;[((~literal tyλ) _ ...) (sysf:type-eval τ)] ; dont eval under tyλ
[((~literal #%plain-lambda) (x ...) τ_body ...)
#:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
- (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'plain-lambda)]
+ (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
[((~literal #%plain-app) arg ...)
#:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
(syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))]
- [_ (sysf:type-eval τ)]))
+ [(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
+ (sysf:type-eval τ)]))
(current-type-eval type-eval))
-(define-base-type ★)
-(define-type-constructor (⇒ k_in ... k_out))
+(define-basic-checked-id-stx ★ : #%kind)
+(define-basic-checked-stx ⇒ : #%kind #:arity >= 1)
+;(define-type-constructor (⇒ k_in ... k_out))
;; for now, handle kind checking in the types themselves
;; TODO: move kind checking to a common place (like #%app)?
@@ -57,13 +66,16 @@
;; TODO: need some kind of "promote" abstraction,
;; so I dont have to manually add kinds to all types
-(define-base-type Str)
-(provide String)
-(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
+(define-basic-checked-id-stx String : ★)
+(define-basic-checked-id-stx Int : ★)
+;(define-base-type Str)
+;(provide String)
+;(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
+;(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
;; → in Fω is not first-class, can't pass it around
-(define-syntax (→ stx)
+(define-basic-checked-stx → : ★ #:arity >= 1)
+#;(define-syntax (→ stx)
(syntax-parse stx
[(_ τ ... τ_res)
#:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
@@ -73,36 +85,37 @@
(define-syntax (∀ stx)
(syntax-parse stx
- [(∀ (b:typed-binding ...) τ)
- #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
- #:when (typecheck? #'k #'★)
- (⊢ (#%type
- (λ (tv- ...)
- (let-syntax ([tv- (syntax-parser [tv-:id #'(#%type tv-)])] ...)
- b.τ ... τ-))) #;(sysf:∀ #:bind tvs- τ-) : ★)]))
+ [(_ (b:kinded-binding ...) τ_body)
+ #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
+ #:when (★? #'k_body)
+ (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
(define-syntax (Λ stx)
(syntax-parse stx
- [(_ (b:typed-binding ...) e)
- #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
- #:when (displayln #'(∀ ([tv- : b.τ] ...) τ))
- (⊢ e- : (∀ ([tv- : b.τ] ...) τ))]))
+ [(_ (b:kinded-binding ...) e)
+ #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
+ (⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
(define-syntax (inst stx)
(syntax-parse stx
- [(_ e τ:type ...)
- #:with ([τ- k] ...) (infers+erase #'(τ ...))
+ [(_ e τ ...)
+ #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+ #:when (stx-andmap
+ (λ (t k)
+ (or (kind? k)
+ (type-error #:src t
+ #:msg "not a valid type: ~a" t)))
+ #'(τ ...) #'(k_τ ...))
#:with (e- ∀τ) (infer+erase #'e)
#:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
- #:when (typechecks? #'(k ...) #'(k_tv ...))
- (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+ #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
+ (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
;; TODO: merge with regular λ and app?
(define-syntax (tyλ stx)
(syntax-parse stx
- [(_ (b:typed-binding ...) τ)
- #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
- ;; b.τ's here are actually kinds
- (⊢ (λ tvs- τ-) : (⇒ b.τ ... k))]))
+ [(_ (b:kinded-binding ...) τ_body)
+ #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
+ (⊢ (λ tvs- τ_body-) : (⇒ b.tag ... k_body))]))
(define-syntax (tyapp stx)
(syntax-parse stx
@@ -163,14 +176,16 @@
;; must override #%app and λ and primops to use new →
;; TODO: parameterize →?
-(define-primop + : (→ Int Int Int))
+(define-primop + : (→ Int Int Int) : ★)
(define-syntax (λ/tc stx)
- (syntax-parse stx
- [(_ (b:typed-binding ...) e)
- #:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
- #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
- (⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
+ (syntax-parse stx #:datum-literals (:)
+ [(_ ([x : τ] ...) e)
+ ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
+ #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
+ #:when (stx-andmap ★? #'(k ...))
+ #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
+ (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
(define-syntax (app/tc stx)
(syntax-parse stx
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -1,34 +1,35 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + type-eval)
- (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
+ (prefix-in sysf: (only-in "sysf.rkt" type-eval))
+ (only-in "stlc+reco+var.rkt" same-types?))
(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
-(provide (except-out (all-from-out "sysf.rkt")
+#;(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
sysf:#%app sysf:λ
(for-syntax sysf:type-eval)))
-(provide Int → ∀ inst Λ
- (for-syntax type-eval))
+(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval))
+ (all-from-out "stlc+reco+var.rkt"))
+(provide Int → ∀ inst Λ (for-syntax type-eval))
;; same as fomega.rkt, except tyapp == #%app, tyλ = λ, and ⇒ = →
-;; System F_omega
+;; System F_omega
;; Type relation:
;; Types:
;; - types from sysf.rkt
;; Terms:
;; - terms from sysf.rkt
+(define-syntax-category kind)
+
(provide define-type-alias)
(define-syntax define-type-alias
(syntax-parser
- [(_ alias:id τ:type)
- ; must eval, otherwise undefined types will be allowed
- #'(define-syntax alias
- (syntax-parser
- [x:id #'τ.norm]
- [(_ x (... ...))
- ((current-type-eval) (⊢ #'(#%plain-app τ.norm x (... ...)) #'★))]))]))
+ [(_ 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 #'τ-]))]))
(begin-for-syntax
;; extend type-eval to handle tyapp
@@ -54,47 +55,57 @@
[_ (sysf:type-eval τ)]))
(current-type-eval type-eval))
-(define-base-type ★)
-;(define-type-constructor ⇒)
-
-;; for now, handle kind checking in the types themselves
-;; TODO: move kind checking to a common place (like #%app)?
-;; when expanding: check and erase kinds
+(define-basic-checked-id-stx ★ : #%kind)
+(define-basic-checked-id-stx String : ★)
+(define-basic-checked-id-stx Int : ★)
-;; TODO: need some kind of "promote" abstraction,
-;; so I dont have to manually add kinds to all types
-(define-base-type Str)
-(provide String)
-(define-syntax String (syntax-parser [x:id (⊢ #'Str #'★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
-
-;; → in Fω is not first-class, can't pass it around
-(define-syntax (→ stx)
+(define-syntax (define-multi stx)
(syntax-parse stx
- [(_ τ ... τ_res)
- #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
- #:when (or
- ; when used as →
- (and (typecheck? #'k_res #'★)
- (same-types? #'(k ... k_res)))
- ; when used as ⇒
- (not (syntax-e (stx-ormap (λ (x) x) #'(k ... k_res)))))
- (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+ [(_ tycon:id)
+ #:with tycon-internal (generate-temporary #'tycon)
+ #'(...
+ (begin
+ (define tycon-internal void)
+ (define-syntax (tycon stx)
+ (syntax-parse stx
+ [(_ τ ... τ_res)
+ #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
+ #:when (or ; when used as →
+ (and (or (★? #'k_res) (#%kind? #'k_res))
+ (same-types? #'(k ... k_res))))
+ (if (★? #'k_res)
+ (⊢ (tycon-internal τ- ... τ_res-) : ★)
+ (⊢ (tycon-internal τ- ... τ_res-) : #%kind))]))))]))
+(define-multi →)
(define-syntax (∀ stx)
(syntax-parse stx
- [(∀ (b:typed-binding ...) τ)
+ [(_ (b:kinded-binding ...) τ)
#:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
- #:when (typecheck? #'k #'★)
- (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
+ #:when (★? #'k)
+ (⊢ (λ tvs- b.tag ... τ-) : ★)]))
(define-syntax (Λ stx)
(syntax-parse stx
- [(_ (b:typed-binding ...) e)
+ [(_ (b:kinded-binding ...) e)
#:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
- (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+ (⊢ e- : (∀ ([tv- : b.tag] ...) τ))]))
(define-syntax (inst stx)
(syntax-parse stx
+ [(_ e τ ...)
+ #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+ #:when (stx-andmap
+ (λ (t k)
+ (or (kind? k)
+ (type-error #:src t
+ #:msg "not a valid type: ~a" t)))
+ #'(τ ...) #'(k_τ ...))
+ #:with (e- ∀τ) (infer+erase #'e)
+ #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
+ #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
+ (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
+#;(define-syntax (inst stx)
+ (syntax-parse stx
[(_ e τ:type ...)
#:with ([τ- k] ...) (infers+erase #'(τ ...))
#:with (e- ∀τ) (infer+erase #'e)
@@ -102,9 +113,19 @@
#:when (typechecks? #'(k ...) #'(k_tv ...))
(⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
-(define-primop + : (→ Int Int Int))
+(define-primop + : (→ Int Int Int) : ★)
(define-syntax (λ/tc stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ ([x : τ] ...) e)
+ ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
+ #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
+ #:when (or (stx-andmap ★? #'(k ...))
+ (stx-andmap #%kind? #'(k ...)))
+ #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
+ (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
+
+#;(define-syntax (λ/tc stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
#:with (k ...) (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...))
@@ -119,6 +140,26 @@
(define-syntax (app/tc stx)
(syntax-parse stx
[(_ e_fn e_arg ...)
+ #:with [e_fn- ((~literal #%plain-lambda) _ τ_in ... τ_out)] (infer+erase #'e_fn)
+ #: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-syntax (app/tc stx)
+ (syntax-parse stx
+ [(_ e_fn e_arg ...)
#:with [e_fn- τ_fn] (infer+erase #'e_fn)
;; this is sysf:→?, it's not defined in fomega so import without prefix
#:fail-unless (→? #'τ_fn)
@@ -158,8 +199,8 @@
;; must override #%datum to use new kinded-Int, etc
(define-syntax (datum/tc stx)
(syntax-parse stx
- [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
- [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+ [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+ [(_ . s:str) (⊢ (#%datum . s) : String)]
[(_ . x)
#:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
#'(#%datum . x)]))
\ No newline at end of file
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -1,15 +1,16 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
- (prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
- (except-in "stlc+reco+sub.rkt" #%app + type=? sub?)
- (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? sub?)))
-(provide (rename-out [sysf:#%app #%app]) (for-syntax sub?))
-(provide (except-out (all-from-out "sysf.rkt")
- sysf:#%app sysf:∀ sysf:Λ sysf:inst
- (for-syntax sysf:type=?))
- (except-out (all-from-out "stlc+reco+sub.rkt")
- (for-syntax stlc:type=? stlc:sub?)))
+(require ;(except-in "sysf.rkt" #%app λ + #%datum ∀ Λ inst type=?)
+ ;(prefix-in sysf: (only-in "sysf.rkt" #%app λ))
+ (except-in "stlc+reco+sub.rkt" #%app λ + type=? #;sub?)
+ (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ #;type=? sub?))
+ (only-in "stlc+rec-iso.rkt" type=?)) ; type=? for binding forms
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]) (for-syntax sub?))
+(provide (except-out (all-from-out "stlc+reco+sub.rkt")
+ stlc:#%app stlc:λ (for-syntax stlc:sub?))
+ (all-from-out "stlc+rec-iso.rkt")
+ #;(except-out (all-from-out "stlc+reco+sub.rkt")
+ (for-syntax #;stlc+reco+sub:type=? stlc+reco+sub:sub?)))
(provide ∀ Λ inst)
;; System F<:
@@ -20,6 +21,11 @@
(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)
@@ -27,11 +33,12 @@
(if sub (expose sub) t)]
[else t]))
(current-promote expose)
+ ; need this, to lift base-types; is there another way to do this?
(define (sub? t1 t2)
(stlc:sub? (expose t1) (expose t2)))
(current-sub? sub?)
;; extend to handle new ∀
- (define (type=? τ1 τ2)
+ #;(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2)
[(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
((~literal #%plain-lambda) (y:id ...) k2 ... t2))
@@ -39,36 +46,80 @@
#:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
(substs #'(k2 ...) #'(y ...) #'t2))]
- [_ (or (sysf:type=? τ1 τ2) (stlc:type=? τ1 τ2))]))
- (current-type=? type=?)
+ [_ (or (sysf:type=? τ1 τ2) (stlc+reco+sub:type=? τ1 τ2))]))
+ #;(current-type=? type=?)
(current-typecheck-relation (current-sub?)))
-;; TODO: shouldnt really support non-bounded (ie, no <: annotation) ∀, etc
-;; but support for now, so old tests pass
-(define-syntax (∀ stx)
+;; Type annotations used in two places:
+;; 1) typechecking the body of
+;; 2) instantiation of ∀
+;; Problem: need type annotations, even in expanded form
+#;(define-syntax (∀ stx)
(syntax-parse stx #:datum-literals (<:)
[(_ ([X:id <: τ] ...) ~! body)
(syntax/loc stx (#%plain-lambda (X ...) τ ... body))]
- [(_ x ...) #'(sysf:∀ x ...)]))
+ #;[(_ x ...) #'(sysf:∀ x ...)]))
+(define ∀-internal void)
+(define-syntax ∀
+ (syntax-parser #:datum-literals (<:)
+ [(_ ([tv:id <: τ:type] ...) τ_body)
+ #:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
+ #:when (#%type? #'k)
+ (mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
+(begin-for-syntax
+ #;(define (infer∀+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- τ_e)
+ #:with ((~literal #%plain-lambda) (tv ...) τ_sub ... τ_body) #'τ_e
+ #'(e- (([tv τ_sub] ...) τ_body))]))
+ (define (∀? t)
+ (syntax-parse t
+ [((~literal #%plain-lambda) tvs ((~literal #%plain-app) (~literal ∀-internal) . args))
+ #t]
+ [_ #f]))
+ (define-syntax ~∀
+ (pattern-expander
+ (syntax-parser #:datum-literals (<:)
+ [(_ ([tv:id <: τ_sub] ...) τ)
+ #'((~literal #%plain-lambda) (tv ...)
+ ((~literal #%plain-app) (~literal ∀-internal) τ_sub ... τ))]
+ [(_ . args)
+ #'(~and ((~literal #%plain-lambda) (tv (... ...))
+ ((~literal #%plain-app) (~literal ∀-internal) τ_sub (... ...) τ))
+ (~parse args #'(([tv τ_sub] (... ...)) τ)))])))
+ (define-syntax ~∀*
+ (pattern-expander
+ (syntax-parser #:datum-literals (<:)
+ [(_ . args) ; (_ ([tv:id <: τ_sub] ...) τ)
+ #'(~or
+ (~∀ . args)
+ ;((~literal #%plain-lambda) (tv ...) τ_sub ... τ)
+ (~and any (~do
+ (type-error
+ #:src #'any
+ #:msg "Expected ∀ type, got: ~a" #'any))))]))))
(define-syntax (Λ stx)
(syntax-parse stx #:datum-literals (<:)
- [(_ ([tv:id <: τsub] ...) ~! e)
- ;; NOTE: we are storing the subtyping relation of tv and τsub in the
- ;; "environment", as we store type annotations
- ;; So we need to add "expose" to certain forms that expect a certain type,
+ [(_ ([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-) (τ)) (infer #'(e) #:ctx #'([tv : τsub] ...) #:tag 'sub)
- (⊢ #'e- #'(∀ ([tv- <: τsub] ...) τ))]
- [(_ x ...) #'(sysf:Λ x ...)]))
+ #:with ((tv- ...) _ (e-) (τ)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
+ #:octx #'([tv : τsub] ...) #:tag 'sub)
+ (⊢ e- : (∀ ([tv- <: τsub] ...) τ))]
+ #;[(_ x ...) #'(sysf:Λ x ...)]))
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
- #:with (e- ∀τ) (infer+erase #'e)
- #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
+ ;#:with (e- (([tv τ_sub] ...) τ_body)) (infer∀+erase #'e)
+ #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
+; #:with (e- ∀τ) (infer+erase #'e)
+; #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
#:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
- (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
- [(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
+ (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
+ #;[(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
#:with (e- ∀τ) (infer+erase #'e)
#:with ((~literal #%plain-lambda) (tv:id ...) τ_body) #'∀τ
#'(sysf:inst e τ ...)]))
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,20 @@
+2015-08-16:
+TODO:
+- generalize binding forms
+- add tags to distinguish different binding forms
+
+2015-08-16:
+Paper outline
+
+stlc.rkt
+Concepts:
+- #%app
+- lambda
+- user input types must be checked
+
+stlc+rec-iso.rkt
+Concept(s): binding form, type=? for binding forms
+
2015-08-13
Requirements for define-type-constructor syntax:
- identifier types, like Int
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -25,12 +25,14 @@
(syntax-parse stx
[(_ e)
; #:with (e- (~Ref* τ)) (infer+erase #'e) ; alternate pattern; worse err msg
- #:with (e- (τ)) (inferRef+erase #'e)
+; #:with (e- (τ)) (inferRef+erase #'e)
+ #:with (e- (τ)) (⇑ e as Ref)
(⊢ (unbox e-) : τ)]))
(define-syntax (:= stx)
(syntax-parse stx
[(_ e_ref e)
- #:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
+; #:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
+ #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
; #:with (e_ref- (~Ref* τ1)) (infer+erase #'e_ref) ; alt pattern; worse err msg
#:with (e- τ2) (infer+erase #'e)
#:when (typecheck? #'τ1 #'τ2)
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -29,7 +29,8 @@
(syntax-parse stx
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
- #:with (e2- (τ2)) (inferList+erase #'e2)
+; #:with (e2- (τ2)) (inferList+erase #'e2)
+ #:with (e2- (τ2)) (⇑ e2 as List)
; #:with (e2- τ-lst) (infer+erase #'e2)
; #:with τ2 (List-get τ from τ-lst)
#:when (typecheck? #'τ1 #'τ2)
@@ -37,14 +38,16 @@
(define-syntax (isnil stx)
(syntax-parse stx
[(_ e)
- #:with (e- _) (inferList+erase #'e)
+; #:with (e- _) (inferList+erase #'e)
+ #:with (e- _) (⇑ e as List)
; #:with (e- τ-lst) (infer+erase #'e)
; #:fail-unless (List? #'τ-lst) "expected argument of List type"
(⊢ (null? e-) : Bool)]))
(define-syntax (head stx)
(syntax-parse stx
[(_ e)
- #:with (e- (τ)) (inferList+erase #'e)
+; #:with (e- (τ)) (inferList+erase #'e)
+ #:with (e- (τ)) (⇑ e as List)
; #:with (e- τ-lst) (infer+erase #'e)
; #:with τ (List-get τ from τ-lst)
(⊢ (car e-) : τ)]))
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -17,15 +17,16 @@
;; - terms from stlc+reco+var.rkt
;; - fld/unfld
+(define-basic-checked-stx μ #:arity = 1 #:bvs = 1)
#;(define-type-constructor
(μ [[tv]] τ_body))
-(define-syntax μ
+#;(define-syntax μ
(syntax-parser
[(_ (tv:id) τ_body)
#:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
#:when (#%type? #'k)
(mk-type #'(λ (tv-) τ_body-))]))
-(begin-for-syntax
+#;(begin-for-syntax
(define-syntax ~μ*
(pattern-expander
(syntax-parser
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -1,15 +1,16 @@
#lang racket/base
(require "typecheck.rkt")
-;; want to use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? type-eval)
- (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
+;;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 sub?)
+ (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum sub?))
(except-in "stlc+reco+var.rkt" #%app #%datum +)
- (prefix-in var: (only-in "stlc+reco+var.rkt" #%datum)))
-(provide (rename-out [stlc:#%app #%app]
+ (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:#%app stlc:#%datum
- (for-syntax stlc:sub?))
- (except-out (all-from-out "stlc+reco+var.rkt") var:#%datum))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum
+ (for-syntax stlc+sub:sub?))
+ (except-out (all-from-out "stlc+reco+var.rkt") stlc+reco+var:#%datum))
(provide (for-syntax sub?))
;; Simply-Typed Lambda Calculus, plus subtyping, plus records
@@ -22,40 +23,34 @@
(define-syntax (datum/tc stx)
(syntax-parse stx
- [(_ . n:number) #'(stlc:#%datum . n)]
- [(_ . x) #'(var:#%datum . x)]))
+ [(_ . n:number) #'(stlc+sub:#%datum . n)]
+ [(_ . x) #'(stlc+reco+var:#%datum . x)]))
(begin-for-syntax
(define (sub? τ1 τ2)
+; (printf "t1 = ~a\n" (syntax->datum τ1))
+; (printf "t2 = ~a\n" (syntax->datum τ2))
(or
- (syntax-parse (list τ1 τ2) #:literals (quote)
- [((~× [: 'k τk] ...) (~× [: 'l τl] ...))
-; [(tup1 tup2)
-; #:when (and (×? #'tup1) (×? #'tup2))
-; #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
-; #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
+ (syntax-parse (list τ1 τ2)
+ [((~× [k : τk] ...) (~× [l : τl] ...))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
(syntax-parser
- [(l:str τl)
- #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
- ((current-sub?) #'τk_match #'τl)])
+ [(label τlabel)
+ #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+ ((current-sub?) #'τk_match #'τlabel)])
#'([l τl] ...))]
- [((~∨ [<> 'k τk] ...) (~∨ [<> 'l τl] ...))
-; [(var1 var2)
-; #:when (and (∨? #'var1) (∨? #'var2))
-; #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
-; #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
+ [((~∨ [k : τk] ...) (~∨ [l : τl] ...))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
(syntax-parser
- [(l:str τl)
- #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
- ((current-sub?) #'τk_match #'τl)])
+ [(label τlabel)
+ #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+ ((current-sub?) #'τk_match #'τlabel)])
#'([l τl] ...))]
[_ #f])
- (stlc:sub? τ1 τ2)))
+ (stlc+sub:sub? τ1 τ2)))
(current-sub? sub?)
(current-typecheck-relation (current-sub?)))
\ No newline at end of file
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -1,15 +1,16 @@
#lang racket/base
(require "typecheck.rkt")
(require (only-in racket/bool symbol=?))
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let #;type=? × infer×+erase))
- (except-in "stlc+tup.rkt" #%app begin tup proj let #;type=? × infer×+erase))
+(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:type=? stlc:infer×+erase)))
-(provide tup proj × var case ∨)
-(provide (for-syntax #;type=? same-types?))
+ (for-syntax ~stlc:× stlc:×?)))
+(provide × tup proj ∨ var case)
+(provide (for-syntax same-types? ~× ~×* ~∨ ~∨*))
;; Simply-Typed Lambda Calculus, plus records and variants
@@ -61,11 +62,29 @@
[(_ [label:id : τ:type] ...)
#:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
#`(stlc:× valid-τ ...)]))
-(define-for-syntax (infer×+erase e)
- (syntax-parse (stlc:infer×+erase e) #:context e
- [(e- τ_e)
- #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
- #'(e- ((l τ) ...))]))
+(begin-for-syntax
+ #;(define (infer×+erase e)
+ (syntax-parse (stlc:infer×+erase e) #:context e
+ [(e- τ_e)
+ #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
+ #'(e- ((l τ) ...))]))
+ (define-syntax ~×
+ (pattern-expander
+ (syntax-parser #:datum-literals (:)
+ [(_ [l : τ_l] (~and ddd (~literal ...)))
+ #'(~stlc:× ((~literal #%plain-app) (quote l) τ_l) ddd)]
+ [(_ . args)
+ #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...))
+ (~parse args #'((l τ_l) (... ...))))])))
+ (define ×? stlc:×?)
+ (define-syntax ~×*
+ (pattern-expander
+ (syntax-parser #:datum-literals (:)
+ [(_ [l : τ_l] (~and ddd (~literal ...)))
+ #'(~or (~× [l : τ_l] ddd)
+ (~and any (~do (type-error
+ #:src #'any
+ #:msg "Expected × type, got: ~a" #'any))))]))))
#;(define-type-constructor
;(× [~× label τ_fld] ...) #:lits (~×)
@@ -89,7 +108,8 @@
(syntax-parse stx #:literals (quote)
[(_ e_rec l:id)
; #:with (e_rec- (~×* [: 'l_τ τ] ...)) (infer+erase #'e_rec)
- #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
+; #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
+ #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
; #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get
; #:with ('l_τ:str ...) (×-get label from τ_rec)
; #:with (τ ...) (×-get τ_fld from τ_rec)
@@ -112,7 +132,7 @@
"Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
#'any)]))
(begin-for-syntax
- (define (infer∨+erase e)
+ #;(define (infer∨+erase e)
(syntax-parse (infer+erase e) #:context e
[(e- τ_e)
#:fail-unless (∨/internal? #'τ_e)
@@ -122,14 +142,24 @@
(syntax->datum e) (type->str #'τ_e))
#:with (~∨/internal ((~literal #%plain-app) (quote l) τ) ...) #'τ_e
#'(e- ((l τ) ...))]))
+ (define ∨? ∨/internal?)
+ (define-syntax ~∨
+ (pattern-expander
+ (syntax-parser #:datum-literals (:)
+ [(_ [l : τ_l] (~and ddd (~literal ...)))
+ #'(~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)]
+ [(_ . args)
+ #'(~and (~∨/internal ((~literal #%plain-app) (quote l) τ_l) (... ...))
+ (~parse args #'((l τ_l) (... ...))))])))
(define-syntax ~∨*
(pattern-expander
(syntax-parser #:datum-literals (:)
[(_ [l : τ_l] (~and ddd (~literal ...)))
- #'(~or (~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)
- (~and any (~do (type-error
- #:src #'any
- #:msg "Expected ∨ type, got: ~a" #'any))))]))))
+ #'(~and (~or (~∨ [l : τ_l] ddd)
+ (~and any (~do (type-error
+ #:src #'any
+ #:msg "Expected ∨ type, got: ~a" #'any))))
+ ~!)])))) ; dont backtrack here
#;(define-type-constructor
(∨ [<> label τ_var] ...) #:lits (<>)
@@ -141,10 +171,16 @@
[(_ l:id = e as τ:type)
; #:when (∨? #'τ.norm)
; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
+; #:when (displayln #'τ)
+; #:when (displayln #'τ.norm)
+; #:when (displayln (type->str #'τ.norm))
#:with (~∨* [l_τ : τ_l] ...) #'τ.norm
; #:with ('l_τ:str ...) (∨-get label from τ)
; #:with (τ_l ...) (∨-get τ_var from τ)
- #:with (_ τ_match) (stx-assoc #'l #'((l_τ τ_l) ...))
+ #: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) : τ)]))
@@ -153,7 +189,8 @@
[(_ e [l:id x:id => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
; #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
- #:with (e- ([l_x τ_x] ...)) (infer∨+erase #'e)
+ ;#:with (e- ([l_x τ_x] ...)) (infer∨+erase #'e)
+ #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
; #:with ('l_x:str ...) (∨-get label from τ_e)
; #:with (τ_x ...) (∨-get τ_var from τ_e)
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -37,7 +37,7 @@
[(_ . x) #'(stlc:#%datum . x)]))
(begin-for-syntax
- (define (sub? τ1 τ2)
+ (define (sub? t1 t2)
; only need this because recursive calls made with unexpanded types
(define τ1 ((current-type-eval) t1))
(define τ2 ((current-type-eval) t2))
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -25,7 +25,8 @@
(define-syntax (proj stx)
(syntax-parse stx
[(_ e_tup n:nat)
- #:with [e_tup- τs_tup] (infer×+erase #'e_tup)
+; #:with [e_tup- τs_tup] (infer×+erase #'e_tup)
+ #: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
@@ -21,7 +21,7 @@
;; - may require some caution when mixing expanded and unexpanded types to
;; create other types
(define (type-eval τ)
- (or (plain-type? τ) ; don't expand if already expanded
+ (or (expanded-type? τ) ; don't expand if already expanded
(add-orig (expand/df τ) τ)))
(current-type-eval type-eval)
@@ -67,7 +67,7 @@
;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander
;#:with (τ_in ...) (→-get τ_in from #'τ_fn)
;#:with τ_out (→-get τ_out from #'τ_fn)
- #:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term -- better err msg
+ #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →) ; #3 work directly on term -- better err msg
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(string-append
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -1,12 +1,12 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "stlc+lit.rkt" #%app λ type=?)
- (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ type=?)))
+ (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ))
+ (only-in "stlc+rec-iso.rkt" type=?))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app
- (for-syntax stlc:type=?)))
-(provide Λ inst)
-(provide (for-syntax type=?))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ)
+ (all-from-out "stlc+rec-iso.rkt")) ; type=?
+(provide ∀ Λ inst)
;; System F
@@ -26,11 +26,36 @@
[(_ (x:id ...) body) ; cannot use :type annotation on body bc of unbound vars
;; use #%plain-lambda to avoid insertion of #%expression
(syntax/loc stx (#%plain-lambda (x ...) body))]))
-(define-type-constructor (∀ [[x ...]] body))
+#;(define-type-constructor (∀ [[x ...]] body))
-(begin-for-syntax
+(define-basic-checked-stx ∀ #:arity = 1 #:bvs >= 0)
+;(define-syntax ∀
+; (syntax-parser
+; [(_ (tv:id ...) τ_body)
+; #:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
+; #:when (#%type? #'k)
+; (mk-type #'(λ (tv- ...) τ_body-))]))
+;(begin-for-syntax
+; (define (infer∀+erase e)
+; (syntax-parse (infer+erase e) #:context e
+; [(e- τ_e)
+; #:with ((~literal #%plain-lambda) (tv ...) τ) #'τ_e
+; #'(e- ((tv ...) τ))]))
+; (define-syntax ~∀*
+; (pattern-expander
+; (syntax-parser
+; [(_ (tv:id ...) τ)
+; #'(~or
+; ((~literal #%plain-lambda) (tv ...) τ)
+; (~and any (~do
+; (type-error
+; #:src #'any
+; #:msg "Expected ∀ type, got: ~a" #'any))))]))))
+
+
+#;(begin-for-syntax
;; extend to handle ∀
- (define (type=? τ1 τ2)
+ #;(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2)
[(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
((~literal #%plain-lambda) (y:id ...) k2 ... t2))
@@ -45,12 +70,12 @@
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (tv:id ...) e)
- #:with ((tv- ...) e- τ) (infer/tvs+erase #'e #'(tv ...))
- (⊢ e- : (∀ #:bind (tv- ...) τ))]))
+ #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
+ (⊢ e- : (∀ (tv- ...) τ))]))
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
- #:with (e- (~∀* [[tv ...]] τ_body)) (infer+erase #'e)
+ #:with (e- (~∀* (tv ...) τ_body)) (infer+erase #'e)
; #:with (e- ∀τ) (infer+erase #'e)
; #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
(⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
@@ -29,7 +29,7 @@
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
(begin 1 2 3)
- #:with-msg "Expected expression 1 to have type Unit, got: Int")
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
@@ -101,23 +101,23 @@
;; check some more err msgs
(typecheck-fail
(and "1" #f)
- #:with-msg "Expected expression \"1\" to have type Bool, got: String")
+ #:with-msg "Expected expression \"1\" to have Bool type, got: String")
(typecheck-fail
(and #t "2")
#:with-msg
- "Expected expression \"2\" to have type Bool, got: String")
+ "Expected expression \"2\" to have Bool type, got: String")
(typecheck-fail
(or "1" #f)
#:with-msg
- "Expected expression \"1\" to have type Bool, got: String")
+ "Expected expression \"1\" to have Bool type, got: String")
(typecheck-fail
(or #t "2")
#:with-msg
- "Expected expression \"2\" to have type Bool, got: String")
+ "Expected expression \"2\" to have Bool type, got: String")
(typecheck-fail
(if "true" 1 2)
#:with-msg
- "Expected expression \"true\" to have type Bool, got: String")
+ "Expected expression \"true\" to have Bool type, got: String")
(typecheck-fail
(if #t 1 "2")
#:with-msg
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -1,191 +1,198 @@
#lang s-exp "../fomega.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)) (→ Int Int)) : ★)
-
-(Λ ([X : ★]) (λ ([x : X]) x))
-
-#;(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+(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)) (→ 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 (tyλ ([t : ★]) t) : (⇒ ★ ★))
-;(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
-;(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
-;(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
-;
-;(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
-;(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-;(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
-;
-;;; partial-apply →
-;(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
-; : (⇒ ★ ★))
-;; f's type must have kind ★
-;(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
-;(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
-; (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
-;(check-type (inst
-; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-; : (→ (→ Int String) (→ Int String)))
-;;; applied f too early
-;(typecheck-fail (inst
-; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
-; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
-;(check-type ((inst
-; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-; (λ ([x : Int]) "int")) : (→ Int String))
-;(check-type (((inst
-; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-; (λ ([x : Int]) "int")) 1) : String ⇒ "int")
-;
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
+(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+
+(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+ : (⇒ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+ (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+(check-type (inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([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 : (tyapp tyf String)]) (f 1)))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
;; tapl examples, p441
-;(define-type-alias Id (tyλ ([X : ★]) X))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
-;
+(typecheck-fail
+ (define-type-alias tmp 1)
+ #:with-msg "not a valid type: 1")
+(define-type-alias Id (tyλ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+
;; tapl examples, p451
-;(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
-;
-;(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 (tyapp 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 (tyapp 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")
-; : (tyapp 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 : ★]) (→ (tyapp 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)
-; : (→ (tyapp 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 : ★]) (→ (tyapp 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)
-; : (→ (tyapp 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)
+(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+(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 (tyapp 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 (tyapp 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")
+ : (tyapp 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 : ★]) (→ (tyapp 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)
+ : (→ (tyapp 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 : ★]) (→ (tyapp 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)
+ : (→ (tyapp 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/fomega2-tests.rkt b/tapl/tests/fomega2-tests.rkt
@@ -6,14 +6,17 @@
(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)) (→ 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))))
+ : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
(check-type (λ ([t : ★]) t) : (→ ★ ★))
(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
@@ -40,9 +43,13 @@
(Λ ([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
- (Λ ([yf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+ (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
(check-type ((inst
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
@@ -53,7 +60,10 @@
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
-; tapl examples, p441
+;; 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))
@@ -66,13 +76,13 @@
(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
+;; tapl examples, p451
(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
(check-type Pair : (→ ★ ★ ★))
(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
-;; parametric pair constructor
+; 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))))
diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
@@ -3,64 +3,65 @@
;; examples from tapl ch26, bounded quantification
;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
-(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
-(define ra (tup ["a" = 0]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) ra)
- : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
-(define rab (tup ["a" = 0]["b" = #t]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) rab)
- : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+(define ra (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) ra)
+ : (× [a : Int]) ⇒ (tup [a = 0]))
+(define rab (tup [a = 0][b = #t]))
+(check-type ((λ ([x : (× [a : Int])]) x) rab)
+ : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
-(check-type (proj ((λ ([x : (× [: "a" Int])]) x) rab) "a")
+(check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
: Int ⇒ 0)
-(check-type (proj ((inst (Λ (X) (λ ([x : X]) x))
- (× [: "a" Int][: "b" Bool]))
- rab) "b")
+(check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
+ (× [a : Int][b : Bool]))
+ rab) b)
: Bool ⇒ #t)
-(define f2 (λ ([x : (× [: "a" Nat])]) (tup ["orig" = x] ["asucc" = (+ 1 (proj x "a"))])))
-(check-type f2 : (→ (× [: "a" Nat]) (× [: "orig" (× [: "a" Nat])] [: "asucc" Nat])))
-(check-type (f2 ra) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
-(check-type (f2 rab) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+(define f2 (λ ([x : (× [a : Nat])]) (tup [orig = x] [asucc = (+ 1 (proj x a))])))
+(check-type f2 : (→ (× [a : Nat]) (× [orig : (× [a : Nat])] [asucc : Nat])))
+(check-type (f2 ra) : (× [orig : (× [a : Nat])][asucc : Nat]))
+(check-type (f2 rab) : (× [orig : (× [a : Nat])][asucc : Nat]))
-;; define-primop (actually #%app) needs to call current-promote
+; check expose properly called for primops
(define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
(check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
+; check type constructors properly call expose
(define f2poly
- (Λ ([X <: (× [: "a" Nat])])
+ (Λ ([X <: (× [a : Nat])])
(λ ([x : X])
- (tup ["orig" = x]["asucc" = (+ (proj x "a") 1)]))))
+ (tup [orig = x][asucc = (+ (proj x a) 1)]))))
-(check-type f2poly : (∀ ([X <: (× [: "a" Nat])]) (→ X (× [: "orig" X][: "asucc" Nat]))))
+(check-type f2poly : (∀ ([X <: (× [a : Nat])]) (→ X (× [orig : X][asucc : Nat]))))
-;; inst f2poly with (× [: "a" Nat])
-(check-type (inst f2poly (× [: "a" Nat]))
- : (→ (× [: "a" Nat])
- (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])))
-(check-type ((inst f2poly (× [: "a" Nat])) ra)
- : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
- ⇒ (tup ["orig" = ra]["asucc" = 1]))
+; inst f2poly with (× [a : Nat])
+(check-type (inst f2poly (× [a : Nat]))
+ : (→ (× [a : Nat])
+ (× [orig : (× [a : Nat])][asucc : Nat])))
+(check-type ((inst f2poly (× [a : Nat])) ra)
+ : (× [orig : (× [a : Nat])][asucc : Nat])
+ ⇒ (tup [orig = ra][asucc = 1]))
-(check-type ((inst f2poly (× [: "a" Nat])) rab)
- : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
- ⇒ (tup ["orig" = rab]["asucc" = 1]))
+(check-type ((inst f2poly (× [a : Nat])) rab)
+ : (× [orig : (× [a : Nat])][asucc : Nat])
+ ⇒ (tup [orig = rab][asucc = 1]))
-(typecheck-fail (proj (proj ((inst f2poly (× [: "a" Nat])) rab) "orig") "b"))
+(typecheck-fail (proj (proj ((inst f2poly (× [a : Nat])) rab) orig) b))
-;; inst f2poly with (× [: "a" Nat][: "b" Bool])
-(check-type (inst f2poly (× [: "a" Nat][: "b" Bool]))
- : (→ (× [: "a" Nat][: "b" Bool])
- (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])))
-(typecheck-fail ((inst f2poly (× [: "a" Nat][: "b" Bool])) ra))
+;; inst f2poly with (× [a : Nat][b : Bool])
+(check-type (inst f2poly (× [a : Nat][b : Bool]))
+ : (→ (× [a : Nat][b : Bool])
+ (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])))
+(typecheck-fail ((inst f2poly (× [a : Nat][b : Bool])) ra))
-(check-type ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab)
- : (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])
- ⇒ (tup ["orig" = rab]["asucc" = 1]))
+(check-type ((inst f2poly (× [a : Nat][b : Bool])) rab)
+ : (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])
+ ⇒ (tup [orig = rab][asucc = 1]))
-(check-type (proj (proj ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab) "orig") "b")
+(check-type (proj (proj ((inst f2poly (× [a : Nat][b : Bool])) rab) orig) b)
: Bool ⇒ #t)
;; make sure inst still checks args
@@ -78,49 +79,50 @@
;; old sysf tests -------------------------------------------------------------
-(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)
+;; old syntax no longer valid
+;(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 -------------------------------------------------------------
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -5,9 +5,9 @@
(define-syntax (check-type stx)
(syntax-parse stx #:datum-literals (: ⇒)
[(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
- [(_ e : τ-expected:type)
+ [(_ e : τ-expected)
#:with τ (typeof (expand/df #'e))
- #:fail-unless (typecheck? #'τ #'τ-expected.norm)
+ #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
(format
"Expression ~a [loc ~a:~a] has type ~a, expected ~a"
(syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -16,9 +16,9 @@
(define-syntax (check-not-type stx)
(syntax-parse stx #:datum-literals (:)
- [(_ e : not-τ:type)
+ [(_ e : not-τ)
#:with τ (typeof (expand/df #'e))
- #:fail-when (typecheck? #'τ #'not-τ.norm)
+ #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ))
(format
"(~a:~a) Expression ~a should not have type ~a"
(syntax-line stx) (syntax-column stx)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -15,12 +15,13 @@
;; subtyping
(require "stlc+sub-tests.rkt")
-;(require "stlc+reco+sub-tests.rkt")
-;;(require "fsub-tests.rkt")
-;
-;;; system F
-;(require "sysf-tests.rkt")
+(require "stlc+reco+sub-tests.rkt")
+
+;; system F
+(require "sysf-tests.rkt")
+
+(require "fsub-tests.rkt") ; sysf + reco-sub
;;; F_omega
-;(require "fomega-tests.rkt")
-;(require "fomega2-tests.rkt")
-\ No newline at end of file
+(require "fomega-tests.rkt")
+(require "fomega2-tests.rkt")
+\ No newline at end of file
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -3,57 +3,61 @@
;; record subtyping tests
(check-type "coffee" : String)
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping
-(check-type (var "coffee" = 3 as (∨ [<> "coffee" Nat])) : (∨ [<> "coffee" Int])) ; element subtyping
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat]))
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Top]))
-(check-type (var "coffee" = 3 as (∨ [<> "coffee" Int])) : (∨ [<> "coffee" Top])) ; element subtyping (twice)
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Num]))
-(check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat]))
-(check-type (tup ["coffee" = -3]) : (× [: "coffee" Num]))
-(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Int])) ; width subtyping
-(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Num])) ; width+element subtyping
+(check-type (tup [coffee = 3]) : (× [coffee : Int])) ; element subtyping
+(check-type (var coffee = 3 as (∨ [coffee : Nat])) : (∨ [coffee : Int])) ; element subtyping
+;err
+(typecheck-fail
+ (var cooffee = 3 as (∨ [coffee : Nat]))
+ #:with-msg "cooffee field does not exist")
+(check-type (tup [coffee = 3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = 3]) : (× [coffee : Top]))
+(check-type (var coffee = 3 as (∨ [coffee : Int])) : (∨ [coffee : Top])) ; element subtyping (twice)
+(check-type (tup [coffee = 3]) : (× [coffee : Num]))
+(check-not-type (tup [coffee = -3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = -3]) : (× [coffee : Num]))
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Int])) ; width subtyping
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Num])) ; width+element subtyping
;; record + fns
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Num Num Num)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Num Num Num)]))
(check-type + : (→ Num Num Num))
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Num)]))
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)]))
-(check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Num)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Top)]))
+(check-type (tup [plus = +] [mul = *]) : (× [plus : (→ Int Num Top)]))
;; examples from tapl ch26, bounded quantification
-(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
-(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]))
- : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t]))
- : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0]))
+ : (× [a : Int]) ⇒ (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t]))
+ : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
-(check-type (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "a")
+(check-type (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) a)
: Int ⇒ 0)
;; this should work! but needs bounded quantification, see fsub.rkt
-(typecheck-fail (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "b"))
+(typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b))
;; previous record tests ------------------------------------------------------
;; records (ie labeled tuples)
(check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
: Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
: Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [is-male? : Bool]))
;; previous basic subtyping tests ------------------------------------------------------
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -1,20 +1,20 @@
#lang s-exp "../sysf.rkt"
(require "rackunit-typechecking.rkt")
-(check-type (Λ (X) (λ ([x : X]) x)) : (∀ [[X]] (→ X X)))
+(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 (Λ (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)))))
+ : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ [[t3]] (∀ [[t4]] (→ t3 (→ t4 t4)))))
+ : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ [[t4]] (∀ [[t3]] (→ t3 (→ t4 t4)))))
+ : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
(check-type (inst (Λ (t) 1) (→ Int Int)) : Int)
@@ -30,27 +30,29 @@
"Expected type of expression to match pattern \\(∀ \\(\\(x ...)) body), got: 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 (Λ (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))
+ (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)
+ ((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))
+(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)
+; ∀ errs
+(typecheck-fail (λ ([x : (∀ (y) (+ 1 y))]) x))
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -74,7 +74,53 @@
;; typeof : Syntax -> Type or #f
;; Retrieves type of given stx, or #f if input has not been assigned a type.
(define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
-
+
+ (define-syntax (⇑ stx)
+ (syntax-parse stx #:datum-literals (as)
+ [(_ e as tycon)
+ #:with τ? (mk-? #'tycon)
+ #:with τ-get (format-id #'tycon "~a-get" #'tycon)
+ #:with τ-expander (format-id #'tycon "~~~a" #'tycon)
+ #'(syntax-parse (infer+erase #'e) #:context #'e
+ [(e- τ_e_)
+ #:with τ_e ((current-promote) #'τ_e_)
+ #:fail-unless (τ? #'τ_e)
+ (format
+ "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
+ (syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
+ (syntax->datum #'e) 'tycon (type->str #'τ_e))
+ ;#:with args (τ-get #'τ_e)
+ (if (stx-pair? #'τ_e)
+ (syntax-parse #'τ_e
+ [(τ-expander . args) #'(e- args)])
+ #'e-)])]))
+ (define-syntax (⇑s stx)
+ (syntax-parse stx #:datum-literals (as)
+ [(_ es as tycon)
+ #:with τ? (mk-? #'tycon)
+ #:with τ-get (format-id #'tycon "~a-get" #'tycon)
+ #:with τ-expander (format-id #'tycon "~~~a" #'tycon)
+ #'(syntax-parse (stx-map infer+erase #'es) #:context #'es
+ [((e- τ_e_) (... ...))
+ #:with (τ_e (... ...)) (stx-map (current-promote) #'(τ_e_ (... ...)))
+ #:when (stx-andmap
+ (λ (e t)
+ (or (τ? t)
+ (type-error #:src e
+ #:msg "Expected expression ~a to have ~a type, got: ~a"
+ e (quote-syntax tycon) t)))
+ #'es
+ #'(τ_e (... ...)))
+ ;#:with args (τ-get #'τ_e)
+ #:with res
+ (stx-map (λ (e t)
+ (if (stx-pair? t)
+ (syntax-parse t
+ [(τ-expander . args) #`(#,e #'args)])
+ e))
+ #'(e- (... ...))
+ #'(τ_e (... ...)))
+ #'res])]))
;; infers the type and erases types in an expression
(define (infer+erase e)
(define e+ (expand/df e))
@@ -89,10 +135,11 @@
;; expanded before wrapping in lambda
;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
;; the types before typechecking, which is acceptable
- (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag 'type])
+ (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:octx [octx tvctx] #:tag [tag 'unused])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
#:with ([tv : k] ...) tvctx
+ #:with ([_ : ok] ...) octx
#:with (e ...) es
#:with
; old expander pattern
@@ -108,13 +155,15 @@
((~literal #%expression)
((~literal #%plain-lambda) xs+
((~literal let-values) () ((~literal let-values) ()
- ((~literal #%expression) e+) ...)))))))
+ ((~literal #%expression) e+) ... (~literal void))))))))
(expand/df
#`(λ (tv ...)
- (let-syntax ([tv (make-rename-transformer (assign-type #'tv #'k #:tag '#,tag))] ...)
+ (let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
(λ (x ...)
- (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
- (#%expression e) ...)))))
+ (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ))] ...)
+ (#%expression e) ... void)))))
+ ;#:when (stx-map displayln #'(e+ ...))
+ ; #:when (displayln (stx-map typeof #'(e+ ...)))
(list #'tvs+ #'xs+ #'(e+ ...)
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
@@ -122,10 +171,19 @@
;; fns derived from infer ---------------------------------------------------
;; some are syntactic shortcuts, some are for backwards compat
- ;; shorter name
+ ;; shorter names
+ ; ctx = type env for bound vars in term e, etc
+ ; can also use for bound tyvars in type e
(define (infer/ctx+erase ctx e)
(syntax-parse (infer (list e) #:ctx ctx)
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+ (define (infers/ctx+erase ctx es)
+ (stx-cdr (infer es #:ctx ctx)))
+ ; tyctx = kind env for bound type vars in term e
+ (define (infer/tyctx+erase ctx e)
+ (syntax-parse (infer (list e) #:tvctx ctx)
+ [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+
;; infers type and erases types in a single expression,
;; in the context of the given bindings and their types
(define (infer/type-ctxt+erase x+τs e)
@@ -151,8 +209,7 @@
(define current-type-eval (make-parameter #f))
(define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
- ; get rid of this?
- (define current-promote (make-parameter (λ (x) x)))
+ (define current-promote (make-parameter (λ (t) t)))
;; term expansion
;; expand/df : Syntax -> Syntax
@@ -188,8 +245,8 @@
; partial expand to reveal #%type wrapper
(syntax-parse (local-expand τ 'expression (list #'#%type))
[((~literal #%type) _) #t] [_ #f])))
- (define (plain-type? τ)
- (and (typeof τ) (typecheck? (typeof τ) #'#%type) τ))
+ (define (expanded-type? τ)
+ (and (typeof τ) #;(typecheck? (typeof τ) #'#%type) τ))
; surface type syntax is saved as the value of the 'orig property
(define (add-orig stx orig)
@@ -248,7 +305,8 @@
(bracket? (stx-car #'stx)))))))
(begin-for-syntax
- (define (mk-? id) (format-id id "~a?" id)))
+ (define (mk-? id) (format-id id "~a?" id))
+ (define-for-syntax (mk-? id) (format-id id "~a?" id)))
(define #%type void)
(define-for-syntax (mk-type t) (assign-type t #'#%type))
@@ -304,7 +362,7 @@
(define-syntax define-basic-checked-id-stx
(syntax-parser
- [(_ τ:id)
+ [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type])))
#:with τ? (format-id #'τ "~a?" #'τ)
#:with τ-internal (generate-temporary #'τ)
#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
@@ -335,28 +393,45 @@
(current-continuation-marks)))))
(define-syntax τ
(syntax-parser
- [(~var _ id) (add-orig (assign-type #'τ-internal #'#%type) #'τ)])))]))
+ [(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
+; I use identifiers "τ" and "kind" but this form is not restricted to them.
+; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
(define-syntax (define-basic-checked-stx stx)
- (syntax-parse stx
- [(_ τ:id (~optional
- (~seq #:arity op n:exact-nonnegative-integer)
- #:defaults ([op #'>=] [n #'0])))
+ (syntax-parse stx #:datum-literals (:)
+ [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type]))
+ (~optional
+ (~seq #:arity op n:exact-nonnegative-integer)
+ #:defaults ([op #'>=] [n #'0]))
+ (~optional
+ (~seq #:bvs (~and has-bvs? bvs-op) bvs-n:exact-nonnegative-integer)
+ #:defaults ([bvs-op #'>=][bvs-n #'0])))
+ #:with kind+ ((current-type-eval) #'kind)
#:with τ-internal (generate-temporary #'τ)
#:with τ? (mk-? #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
- #'(begin
- (provide τ (for-syntax τ-expander τ-expander* inferτ+erase))
+ #:with τ-get (format-id #'τ "~a-get" #'τ)
+ #`(begin
+ (provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase))
(begin-for-syntax
(define-syntax τ-expander
(pattern-expander
(syntax-parser
- [(_ . pat)
- #'((~literal #%plain-app) (~literal τ-internal) . pat)])))
+ [(_ . pat:id)
+ #'(~and ((~literal #%plain-lambda) bvs
+ ((~literal #%plain-app) (~literal τ-internal) . rst))
+ #,(if (attribute has-bvs?)
+ #'(~parse pat #'(bvs rst))
+ #'(~parse pat #'rst)))]
+ [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
+ (bv (... ...)))
+ #:defaults ([(bv 1) null])) . pat)
+ #'((~literal #%plain-lambda) (bv (... ...))
+ ((~literal #%plain-app) (~literal τ-internal) . pat))])))
(define-syntax τ-expander*
(pattern-expander
(syntax-parser
@@ -371,8 +446,15 @@
#:msg
"Expected ~a type, got: ~a"
#'τ #'any))))])))
- (define (τ? t) (and (stx-pair? t) (typecheck? (stx-cadr t) #'τ-internal)))
- (define (inferτ+erase e)
+ (define (τ? t)
+ (and (stx-pair? t)
+ (syntax-parse t
+ [((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
+ (typecheck? #'tycon #'τ-internal)])))
+ #;(define (τ-get t)
+ (syntax-parse t
+ [(τ-expander . pat) #'pat]))
+ #;(define (inferτ+erase e)
(syntax-parse (infer+erase e) #:context e
[(e- τ_e)
#:fail-unless (stx-pair? #'τ_e)
@@ -395,13 +477,25 @@
;; ; this is the actual constructor
(define-syntax (τ stx)
(syntax-parse stx
- [(_ . args)
+ [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
+ (bv (... ...)))
+ #:defaults ([(bv 1) null])) . args)
+ #:with bvs #'(bv (... ...))
+ #:fail-unless (bvs-op (stx-length #'bvs) bvs-n)
+ (format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n)
#:fail-unless (op (stx-length #'args) n)
(format "wrong number of arguments, expected ~a ~a" 'op 'n)
- #:with (~! (~var ty type) (... ...)) #'args
+ #:with (bvs- τs- ks) (infers/ctx+erase #'([bv : kind] (... ...)) #'args)
+ #:when (stx-andmap
+ (λ (t k)
+ (or (typecheck? k #'kind+)
+ (type-error #:src t
+ #:msg "not a valid type: ~a" t)))
+ #'args #'ks)
+ ;#:with (~! (~var _ type) (... ...)) #'τs-
; #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
; #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
- (assign-type #'(τ-internal ty.norm (... ...)) #'#%type)]
+ (assign-type #'(λ bvs- (τ-internal . τs-)) #'kind)]
;; else fail with err msg
[_
(type-error #:src stx
@@ -797,6 +891,41 @@
; #:when (typecheck? #'tycon #'tmp)
; (stx-length #'(τ_arg (... ...)))])))]))
+; examples:
+; (define-syntax-category type)
+; (define-syntax-category kind)
+(define-syntax (define-syntax-category stx)
+ (syntax-parse stx
+ [(_ name:id)
+ #:with #%tag (format-id #'name "#%~a" #'name)
+ #:with #%tag? (mk-? #'#%tag)
+ #:with name? (mk-? #'name)
+ #:with named-binding (format-id #'name "~aed-binding" #'name)
+ #'(begin
+ (define #%tag void)
+ (begin-for-syntax
+ (define (#%tag? t) (typecheck? t #'#%tag))
+ (define (name? t) (#%tag? (typeof t)))
+ (define-syntax-class name
+ #:attributes (norm)
+ (pattern τ
+ #:with norm ((current-type-eval) #'τ)
+ #:with k (typeof #'norm)
+ #:fail-unless (#%tag? #'k)
+ (format "~a (~a:~a) not a valid ~a: ~a"
+ (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
+ 'name (type->str #'τ))))
+ (define-syntax-class named-binding #:datum-literals (:)
+ #:attributes (x tag)
+ (pattern [x:id : ~! (~var ty name)] #:attr tag #'ty.norm)
+ (pattern any
+ #:fail-when #t
+ (format
+ (string-append
+ "Improperly formatted ~a annotation: ~a; should have shape [x : τ], "
+ "where τ is a valid ~a.")
+ 'name (type->str #'any) 'name)
+ #:attr x #f #:attr tag #f))))]))
;; syntax classes
(begin-for-syntax
(define-syntax-class type
@@ -805,7 +934,9 @@
;; -dont bother to check if type is already expanded, because this class
;; typically annotates user-written types
(pattern τ
- #:with [norm k] (infer+erase #'τ)
+; #:with [norm k] (infer+erase #'τ)
+ #:with norm ((current-type-eval) #'τ)
+ #:with k (typeof #'norm)
#:fail-unless (#%type? #'k)
(format "~a (~a:~a) not a valid type: ~a"
(syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
@@ -846,7 +977,11 @@
(define-syntax (define-primop stx)
(syntax-parse stx #:datum-literals (:)
- [(_ op:id : τ:type)
+ [(_ op:id : τ (~optional (~seq : k) #:defaults ([k #'#%type])))
+ #:with kind ((current-type-eval) #'k)
+ #:with τ+ ((current-type-eval) #'τ)
+ #:with k_τ (typeof #'τ+)
+ #:when (typecheck? #'k_τ #'kind)
#:with op/tc (generate-temporary #'op)
#`(begin
(provide (rename-out [op/tc op]))
