commit 98fdc8806cd78cc454cd2e59454797399494b08c
parent ad02e586ad05d753479764dd3ad76a9c75311316
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 26 Jun 2015 18:56:01 -0400
convert type representation to fully expanded syntax
- type-eval = expand/df
- fomega tyapp and tylam not yet implemented
Diffstat:
21 files changed, 569 insertions(+), 257 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -119,7 +119,7 @@
(string-append
"letrec: type check fail, args have wrong type:\n"
(string-join
- (stx-map (λ (e τ τ-expect) (format "~a has type ~a, expected ~a"))
+ (stx-map (λ (e τ τ-expect) (format "~a has type ~a, expected ~a" e τ τ-expect))
#'(e ...) #'(τ ...) #'(b.τ ...))
"\n"))
(⊢ #'(letrec ([x- e-] ...) e_body-) #'τ_body)]))
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,13 +1,14 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app λ + Λ inst Int → ∀ eval-τ type=?)
- (prefix-in sysf: (only-in "sysf.rkt" Int → ∀ eval-τ type=?)))
-(provide (rename-out [app/tc #%app] [λ/tc λ]))
+(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + #;type=?)
+ (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ #;type=?)))
+(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
- (for-syntax sysf:type=? sysf:eval-τ)))
-(provide Int → ∀ inst Λ
- (for-syntax eval-τ type=?))
+ sysf:#%app sysf:λ
+ #;(for-syntax sysf:type=?)))
+(provide Int → ∀ inst Λ tyλ tyapp
+ #;(for-syntax type=?))
;; System F_omega
;; Type relation:
@@ -18,18 +19,26 @@
(begin-for-syntax
;; Extend to handle ∀ with type annotations
- (define (eval-τ τ [tvs #'()])
+ #;(define (eval-τ τ [tvs #'()] . rst)
(syntax-parse τ
[((~literal ∀) (b:typed-binding ...) t-body)
- #`(∀ (b ...) #,((current-τ-eval) #'t-body (stx-append tvs #'(b.x ...))))]
+ #:with new-tvs #'(b.x ...)
+ #`(∀ (b ...) #,(apply (current-τ-eval) #'t-body (stx-append tvs #'new-tvs) rst))]
;; need to manually handle type constructors now since they are macros
[((~literal →) t ...)
- #`(→ #,@(stx-map (λ (ty) ((current-τ-eval) ty tvs)) #'(t ...)))]
- [_ (sysf:eval-τ τ tvs)]))
- (current-τ-eval eval-τ)
+ #`(→ #,@(stx-map (λ (ty) (apply (current-τ-eval) ty tvs rst)) #'(t ...)))]
+ #;[((~literal #%app) x ...)
+ #:when (printf "~a\n" (syntax->datum #'(x ...)))
+ #'(void)]
+ [((~literal tyapp) ((~literal tyλ) (b:typed-binding ...) τ_body) τ_arg ...)
+ #:with (τ_arg+ ...) (stx-map (λ (ty) (apply (current-τ-eval) ty tvs rst)) #'(τ_arg ...))
+ #:with τ_body+ (apply (current-τ-eval) #'τ_body tvs rst)
+ (substs #'(τ_arg+ ...) #'(b.x ...) #'τ_body+)]
+ [_ (apply sysf:eval-τ τ tvs rst)]))
+ ;(current-τ-eval eval-τ)
;; extend to handle ∀ with kind annotations
- (define (type=? τ1 τ2)
+ #;(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2) #:literals (∀)
[((∀ (a:typed-binding ...) t1:type) (∀ (b:typed-binding ...) t2:type))
#:when (= (stx-length #'(a ...)) (stx-length #'(b ...)))
@@ -38,8 +47,8 @@
((current-type=?) (substs #'(z ...) #'(a.x ...) #'t1)
(substs #'(z ...) #'(b.x ...) #'t2))]
[_ (sysf:type=? τ1 τ2)]))
- (current-type=? type=?)
- (current-typecheck-relation type=?))
+ #;(current-type=? type=?)
+ #;(current-typecheck-relation type=?))
(define-base-type ★)
(define-type-constructor ⇒)
@@ -48,6 +57,11 @@
;; TODO: move kind checking to a common place (like #%app)?
;; when expanding: check and erase kinds
+;; 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
@@ -57,15 +71,26 @@
#:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
#:when (typecheck? #'k_res #'★)
#:when (same-types? #'(k ... k_res))
- (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+ (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
(define-syntax (∀ stx)
(syntax-parse stx
[(∀ (b:typed-binding ...) τ)
#:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
#:when (typecheck? #'k #'★)
- (⊢ #'(sysf:∀ tvs- τ-) #'★)]))
-
+ (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
+
+#;(define-syntax (Λ stx)
+ (syntax-parse stx
+ [(_ (tv:id ...) e)
+ #:with (tvs- e- τ) (infer/tvs+erase #'e #'(tv ...))
+ (⊢ #'e- #'(∀ tvs- τ))]))
+#;(define-syntax (inst stx)
+ (syntax-parse stx
+ [(_ e τ:type ...)
+ #:with (e- ∀τ) (infer+erase #'e)
+ #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
+ (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
@@ -73,12 +98,28 @@
(⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
(define-syntax (inst stx)
(syntax-parse stx
- [(_ e τ ...)
+ [(_ e τ:type ...)
#:with ([τ- k] ...) (infers+erase #'(τ ...))
- #:with (e- τ_e) (infer+erase #'e)
- #:with ((~literal ∀) (b:typed-binding ...) τ_body) #'τ_e
- #:when (typechecks? #'(k ...) #'(b.τ ...))
- (⊢ #'e- (substs #'(τ ...) #'(b.x ...) #'τ_body))]))
+ #:with (e- ∀τ) (infer+erase #'e)
+ #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
+ #:when (typechecks? #'(k ...) #'(k_tv ...))
+ (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+
+;; TODO: merge with regular λ and app?
+(define-syntax (tyλ stx)
+ (syntax-parse stx
+ ; b = [tv : k]
+ [(_ (b:typed-binding ...) τ)
+ #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+ ; TODO: Racket lambda?
+ (⊢ #'(λ (tv- ...) τ-) #'(⇒ b.τ ... k))]))
+(define-syntax (tyapp stx)
+ (syntax-parse stx
+ [(_ τ_fn τ_arg ...)
+ #:with [τ_fn- ((~literal ⇒) k ... k_res)] (infer+erase #'τ_fn)
+ #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
+ #:when (typechecks? #'(k_arg ...) #'(k ...))
+ (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
;; must override #%app and λ and primops to use new →
;; TODO: parameterize →?
@@ -93,14 +134,15 @@
(⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
(define-syntax (app/tc stx)
- (syntax-parse stx #:literals (→)
+ (syntax-parse stx
[(_ e_fn e_arg ...)
- #:with (e_fn- ((~literal →) τ ... τ_res)) (infer+erase #'e_fn)
-; #:fail-unless (→? #'τ_fn)
-; (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
-; (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-; #:with (→ τ ... τ_res) #'τ_fn
- #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+ #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+ ;; this is sysf:→?, dont need prefix bc it's not defined here
+ #:fail-unless (→? #'τ_fn)
+ (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+ (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+ #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+ #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
(string-append
(format
@@ -115,3 +157,11 @@
", "))
(⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+;; 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)]
+ [(_ . x)
+ #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
+ #'(#%datum . x)]))
+\ No newline at end of file
diff --git a/tapl/id-expand-experiment.rkt b/tapl/id-expand-experiment.rkt
@@ -0,0 +1,51 @@
+#lang racket
+(require (for-syntax syntax/parse))
+#;(define-syntax (test stx)
+ (syntax-parse stx
+ [(_ x)
+ #:with (_ (x2) x3) (local-expand #'(λ (x) (test2 x)) 'expression null)
+ #:with (_ (x4) x5) (local-expand #'(λ (x) x) 'expression null)
+ #:when (printf "test1: ~a\n" (free-identifier=? #'x2 #'x3))
+ #'(void)]))
+#;(define-syntax (test2 stx)
+ (syntax-parse stx
+ [(_ x)
+ #:with xx (local-expand #'x 'expression null)
+ #:when (printf "test2: ~a\n" (bound-identifier=? #'x #'xx))
+ #:with (lam (xxx) xxxx) (local-expand #'(λ (x) xx) 'expression null)
+ #:when (printf "test2 post: ~a\n" (bound-identifier=? #'xxx #'xxxx))
+ (local-expand #'x 'expression null)]))
+#;(test x)
+
+(define x 1)
+(define-for-syntax (f y)
+ (printf "f: ~a\n" (bound-identifier=? y #'x)))
+(define-syntax (test stx)
+ (syntax-parse stx
+ [(_ y)
+ #:when (printf "test: ~a\n" (bound-identifier=? #'x #'y))
+ #:when (printf "test: ~a\n" (bound-identifier=? (syntax-local-introduce #'x) #'y))
+ #:when (printf "test: ~a\n" (bound-identifier=? ((make-syntax-delta-introducer #'y #'x) #'x) #'y))
+ #:when (printf "test: ~a\n" (bound-identifier=? ((make-syntax-delta-introducer #'x #'y) #'x) #'y))
+ #:when (printf "test: ~a\n" (bound-identifier=? (syntax-local-introduce #'y) #'x)) ; negates mark?
+ #:when (printf "test: ~a\n" (bound-identifier=? ((make-syntax-delta-introducer #'y #'x) #'y) #'x))
+ #:when (printf "test: ~a\n" (bound-identifier=? ((make-syntax-delta-introducer #'x #'y) #'y) #'x))
+ #:when (printf "test: ~a\n" (bound-identifier=? (syntax-local-introduce (syntax-local-introduce #'y)) #'x)) ; double negation means no again
+ #:when (f #'x)
+ #:when (local-expand #'(test3 y) 'expression null)
+ #'(test2 y)]))
+(define-syntax (test2 stx)
+ (syntax-parse stx
+ [(_ z)
+ #:when (printf "test2: ~a\n" (bound-identifier=? #'x #'z))
+ #:when (printf "test2: ~a\n" (bound-identifier=? #'x (syntax-local-introduce #'z)))
+ #:when (printf "test2: ~a\n" (bound-identifier=? #'z (syntax-local-introduce #'x)))
+ #'(void)]))
+(define-syntax (test3 stx)
+ (syntax-parse stx
+ [(_ z)
+ #:when (printf "test3: ~a\n" (bound-identifier=? #'x #'z))
+ #:when (printf "test3: ~a\n" (bound-identifier=? #'x (syntax-local-introduce #'z)))
+ #:when (printf "test3: ~a\n" (bound-identifier=? #'z (syntax-local-introduce #'x)))
+ #'(void)]))
+(test x)
+\ No newline at end of file
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,98 @@
+2015-06-26
+Random thought: Can kinds be "erased"?
+- first thought is no, since they appear to be needed for type equality?
+
+2015-06-26
+syntax marks problem:
+- in the type created by \Lambda, eg \x.(-> x x), the binding x and body x's
+ were free-id= but not bound-id= because the body x's had extra marks
+- this is because (the syntax representing) types are marked going "into" an
+ expansion, but do not receive the cancelling mark coming out of the
+ expansion since they are attached as a syntax-property
+- thus, when this lam goes through another expansion (via \vdash), the binding x
+ and body x's become neither free-id nor bound-id=?
+Solution:
+- undo the mark (using syntax-local-introduce) before attaching a type
+ as a syntax property (ie in \vdash)
+- need one more syntax-local-introduce in infer/tvs+erase
+- i guess the rule is I need as many syntax-local-introduce's as extra
+ expanding lambdas that I add
+
+
+2015-06-18
+Design Decision:
+Types must be fully expanded, if we wish to use expansion to typecheck types
+(i.e., kinding).
+Problems:
+- Type constructors can't be both macro and function
+ - solution: macro that expands to tmp function
+ - must provide predicate to check
+- Recursive types
+ - solution: ???
+- Displaying error msgs
+ - need to keep track of surface stx (similar to 'origin prop?)
+ - solution: ???
+- repeated expansion of already expanded types
+ - solution: ???
+- what to do about tuples, where there may be a string in the fn position
+ - solution: add an extra "type constructor" in front of each pair
+ - todo: come up with a nicer way to handle "compound" types
+- what is the expansion of forall?
+
+2015-06-16
+Problem:
+use expansion for typechecking of terms: ok
+- specifically, ok to go under lambda, since eval happens later
+use expansion for typechecking of types: doesnt work now
+- doesnt work because types currently are not fully-expandable
+ - eg a type constructor application (tycon x) is a macro that expands to
+ (#%app tycon x), where this expression will error if expanded further
+ since tycon cannot be used as an identifier
+ - if I define tycon as a regular function, so (tycon x) expands to
+ (#%app tycon x), then it wont catch non-app uses of tycon
+ - should be fine? - this is a parsing, not typechecking problem
+ - but then then parser need to be updated with every new type constructor
+ - this kind of monolithic architecture is what the paper is trying
+ to avoid
+ - alternative: define tycon as a macro where (tycon x) expands to
+ (#%app tycon_new x)
+ - drawback: can't use ~literal to match/destructure the tycon
+ - does this make things like type checking or type=? more difficult?
+ - will have to go through a separately-defined interface,
+ like a \tau? predicate
+Subproblem: must completely change the representation of types?
+- must use fully-expanded forms instead of surface syntax
+- in particular, will be using *fully expanded identifiers*
+ - in this scenario, can I still match with ~literal?
+Subproblem: where/when to expand
+- types now must all be expanded since that is when kind checking occurs
+use expansion for eval of types: not ok
+- dont want to go under binders
+- expand then eval?
+ - but then type constructors cant be macros?
+Possible Solution
+- I think eval must be separate
+Subproblem: Do I need a new eval that is different from current-eval?
+- conflict:
+ - current-eval must go under forall to check for unbound ids
+ - but eval should not go under forall for the case of tyapps
+- maybe tyapp should go into type=?, as in tapl?
+Subproblem: where to eval
+- currently call eval for user type annotations, and in \vdash
+Subproblem: Can type=? assume fully expanded (ie, evaled) types?
+
+2015-06-15
+New Thesis: The abstractions provided by macro systems are effective at
+implementing type systems
+
+2015-06-08
+Problem: how to represent \rightarrow kind operator
+1) If the kind operator is the same as the function type operator then how do I
+attach a kind to a function arrow, since the arrow is still undefined at the
+time.
+2) If the kind arrow is a different arrow then #%app must be parameterized over
+the arrow
+
2015-05-28
Problem: how to represent \forall types
1) (Racket) functions
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -13,7 +13,7 @@
;; Terms:
;; - terms from stlc+cons.rkt
-(define-type-constructor Ref)
+(define-type-constructor Ref #:arity 1)
(define-syntax (ref stx)
(syntax-parse stx
@@ -23,12 +23,14 @@
(define-syntax (deref stx)
(syntax-parse stx
[(_ e)
- #:with (e- ((~literal Ref) τ)) (infer+erase #'e)
+ #:with (e- ref-τ) (infer+erase #'e)
+ #:with (τ) (Ref-args #'ref-τ)
(⊢ #'(unbox e-) #'τ)]))
(define-syntax (:= stx)
(syntax-parse stx
[(_ e_ref e)
- #:with (e_ref- ((~literal Ref) τ1)) (infer+erase #'e_ref)
+ #:with (e_ref- ref-τ) (infer+erase #'e_ref)
+ #:with (τ1) (Ref-args #'ref-τ)
#:with (e- τ2) (infer+erase #'e)
#:when (typecheck? #'τ1 #'τ2)
(⊢ #'(set-box! e_ref- e-) #'Unit)]))
\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -27,7 +27,7 @@
(define-syntax x (make-rename-transformer (⊢ #'y #'τ)))
(define y e-))]))
-(define-type-constructor List)
+(define-type-constructor List #:arity 1)
(define-syntax (nil stx)
(syntax-parse stx
@@ -40,21 +40,25 @@
(syntax-parse stx
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
- #:with (e2- ((~literal List) τ2)) (infer+erase #'e2)
+ #:with (e2- τ-lst) (infer+erase #'e2)
+ #:with (τ2) (List-args #'τ-lst)
#:when (typecheck? #'τ1 #'τ2)
(⊢ #'(cons e1- e2-) #'(List τ1))]))
(define-syntax (isnil stx)
(syntax-parse stx
[(_ e)
- #:with (e- ((~literal List) τ)) (infer+erase #'e)
+ #:with (e- τ-lst) (infer+erase #'e)
+ #:when (List? #'τ-lst)
(⊢ #'(null? e-) #'Bool)]))
(define-syntax (head stx)
(syntax-parse stx
[(_ e)
- #:with (e- ((~literal List) τ)) (infer+erase #'e)
+ #:with (e- τ-lst) (infer+erase #'e)
+ #:with (τ) (List-args #'τ-lst)
(⊢ #'(car e-) #'τ)]))
(define-syntax (tail stx)
(syntax-parse stx
[(_ e)
- #:with (e- ((~literal List) τ)) (infer+erase #'e)
- (⊢ #'(cdr e-) #'(List τ))]))
-\ No newline at end of file
+ #:with (e- τ-lst) (infer+erase #'e)
+ #:when (List? #'τ-lst)
+ (⊢ #'(cdr e-) #'τ-lst)]))
+\ No newline at end of file
diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt
@@ -1,7 +1,7 @@
#lang racket/base
(require "typecheck.rkt")
-;; want to use type=? and eval-τ from stlc+var.rkt, not stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? eval-τ)
+;; want to use type=? and eval-type from stlc+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?))
(except-in "stlc+var.rkt" #%app #%datum +)
(prefix-in var: (only-in "stlc+var.rkt" #%datum)))
@@ -28,8 +28,11 @@
(begin-for-syntax
(define (sub? τ1 τ2)
(or
- (syntax-parse (list τ1 τ2) #:literals (× ∨)
- [((× [k:str τk] ...) (× [l:str τl] ...))
+ (syntax-parse (list τ1 τ2) #:literals (× ∨ quote)
+ [(tup1 tup2)
+ #:when (and (×? #'tup1) (×? #'tup2))
+ #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
+ #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
@@ -38,7 +41,10 @@
#:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
((current-sub?) #'τk_match #'τl)])
#'([l τl] ...))]
- [((∨ [k:str τk] ...) (∨ [l:str τ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))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -2,7 +2,7 @@
(require "typecheck.rkt")
(require (except-in "stlc+lit.rkt" #%datum + #%app)
(prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)))
-(provide (rename-out #;[app/tc #%app] [stlc:#%app #%app] [datum/tc #%datum]))
+(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]))
(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
(provide (for-syntax sub? subs? current-sub?))
@@ -38,14 +38,19 @@
(begin-for-syntax
(define (sub? τ1 τ2)
+; (printf "t1 = ~a\n" (syntax->datum τ1))
+; (printf "t2 = ~a\n" (syntax->datum τ2))
(or ((current-type=?) τ1 τ2)
- (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num Top)
+ (syntax-parse (list τ1 τ2) #:literals (Nat Int Num Top)
[(_ Top) #t]
[(Nat τ) ((current-sub?) #'Int #'τ)]
[(Int τ) ((current-sub?) #'Num #'τ)]
[(τ Num) ((current-sub?) #'τ #'Int)]
[(τ Int) ((current-sub?) #'τ #'Nat)]
- [((→ s1 ... s2) (→ t1 ... t2))
+ [(arr1 arr2)
+ #:when (and (→? #'arr1) (→? #'arr2))
+ #:with (s1 ... s2) (→-args #'arr1)
+ #:with (t1 ... t2) (→-args #'arr2)
(and (subs? #'(t1 ...) #'(s1 ...))
((current-sub?) #'s2 #'t2))]
[_ #f])))
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -26,6 +26,6 @@
[(_ tup n:integer)
#:with (tup- τ_tup) (infer+erase #'tup)
#:fail-unless (×? #'τ_tup) "not tuple type"
- #:fail-unless (< (add1 (syntax->datum #'n)) (stx-length #'τ_tup)) "proj index too large"
- (⊢ #'(list-ref tup n) (stx-list-ref #'τ_tup (add1 (syntax->datum #'n))))]))
+ #:fail-unless (< (syntax-e #'n) (×-num-args #'τ_tup)) "proj index too large"
+ (⊢ #'(list-ref tup n) (×-ref #'τ_tup (syntax-e #'n)))]))
\ No newline at end of file
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
@@ -1,14 +1,13 @@
#lang racket/base
(require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=? eval-τ))
- (except-in "stlc+tup.rkt" #%app λ tup proj let type=? eval-τ))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?))
+ (except-in "stlc+tup.rkt" #%app λ tup proj let type=?))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
(provide (except-out (all-from-out "stlc+tup.rkt")
stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj
- (for-syntax stlc:type=? stlc:eval-τ)))
-;(provide define-type-alias define-variant module quote submod)
+ (for-syntax stlc:type=?)))
(provide tup proj var case)
-(provide (for-syntax type=? eval-τ))
+(provide (for-syntax type=?))
;; Simply-Typed Lambda Calculus, plus variants
@@ -27,11 +26,11 @@
(begin-for-syntax
;; type expansion
;; extend to handle strings
- (define (eval-τ τ . rst)
+ #;(define (eval-τ τ . rst)
(syntax-parse τ
[s:str τ] ; record field
[_ (apply stlc:eval-τ τ rst)]))
- (current-τ-eval eval-τ)
+ #;(current-τ-eval eval-τ)
; extend to:
; 1) first eval types, to accomodate aliases
@@ -47,49 +46,49 @@
(provide define-type-alias)
(define-syntax define-type-alias
(syntax-parser
- [(_ alias:id τ)
+ [(_ alias:id τ:type)
; must eval, otherwise undefined types will be allowed
- #'(define-syntax alias (syntax-parser [x:id ((current-τ-eval) #'τ)]))]))
+ #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+
+(define-type-constructor : #:arity 2)
;; records
(define-syntax (tup stx)
(syntax-parse stx #:datum-literals (=)
[(_ [l:str = e] ...)
#:with ((e- τ) ...) (infers+erase #'(e ...))
- (⊢ #'(list (list l e-) ...) #'(× [l τ] ...))]
+ (⊢ #'(list (list l e-) ...) #'(× [: l τ] ...))]
[(_ e ...)
#'(stlc:tup e ...)]))
(define-syntax (proj stx)
- (syntax-parse stx
+ (syntax-parse stx #:literals (quote)
[(_ rec l:str)
#:with (rec- τ_rec) (infer+erase #'rec)
#:fail-unless (×? #'τ_rec) "not record type"
- #:with (× [l_τ τ] ...) #'τ_rec
- #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ) ...))
+ #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
+ #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
(⊢ #'(cadr (assoc l rec)) #'τ_match)]
- [(_ e ...)
- #'(stlc:proj e ...)]))
+ [(_ e ...) #'(stlc:proj e ...)]))
(define-type-constructor ∨)
(define-syntax (var stx)
- (syntax-parse stx #:datum-literals (as =)
- [(_ l:str = e as τ)
- #:with τ+ ((current-τ-eval) #'τ)
- #:when (∨? #'τ+)
- #:with (∨ (l_τ τ_l) ...) #'τ+
- #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
+ (syntax-parse stx #:datum-literals (as =) #:literals (quote)
+ [(_ l:str = e as τ:type)
+ #:when (∨? #'τ.norm)
+ #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
+ #:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
#:with (e- τ_e) (infer+erase #'e)
- #:when (typecheck? #'τ_match #'τ_e)
- (⊢ #'(list l e) #'τ+)]))
+ #:when (typecheck? #'τ_e #'τ_match)
+ (⊢ #'(list l e) #'τ.norm)]))
(define-syntax (case stx)
- (syntax-parse stx #:datum-literals (of =>)
+ (syntax-parse stx #:datum-literals (of =>) #:literals (quote)
[(_ e [l:str x => e_l] ...)
+ #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
#:with (e- τ_e) (infer+erase #'e)
#:when (∨? #'τ_e)
- #:with (∨ (l_x τ_x) ...) #'τ_e
- #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+ #:with (['l_x:str τ_x] ...) (stx-map :-args (∨-args #'τ_e))
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
#:with (((x-) e_l- τ_el) ...)
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -1,7 +1,7 @@
#lang racket/base
(require "typecheck.rkt")
(provide (rename-out [λ/tc λ] [app/tc #%app]))
-(provide (for-syntax type=? types=? same-types? current-type=? eval-τ))
+(provide (for-syntax type=? types=? same-types? current-type=? type-eval))
(provide #%module-begin #%top-interaction #%top require) ; from racket
;; Simply-Typed Lambda Calculus
@@ -16,35 +16,35 @@
;; type expansion
;; - must structurally recur to check nested identifiers
;; - rst allows adding extra args later
- (define (eval-τ τ . rst)
- ; app is #%app in τ's ctxt, not here (which is racket's #%app)
- (define app (datum->syntax τ '#%app))
- ;; stop right before expanding:
- ;; - #%app, this should mean tycon via define-type-constructor
- ;; - app, other compound types, like variants
- ;; - ow, the type checking in #%app will fail
- ;; (could leave this case out until adding variants but it's general
- ;; enough, so leave it here)
- ;; could match specific type constructors like → before expanding
- ;; but this is more general and wont require subsequent extensions for
- ;; every defined type constructor
- (syntax-parse (local-expand τ 'expression (list app #'#%app))
- ; full expansion checks for undefined types
- [x:id (local-expand #'x 'expression null)]
- [((~literal #%app) tcon t ...)
- #`(tcon #,@(stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...)))]
- ; else just structurually eval
- [(t ...) (stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...))]))
- (current-τ-eval eval-τ))
+ (define (type-eval τ) (expand/df τ))
+; #;(define (eval-τ τ . rst)
+; ; app is #%app in τ's ctxt, not here (which is racket's #%app)
+; (define app (datum->syntax τ '#%app))
+; ;; stop right before expanding:
+; ;; - #%app, this should mean tycon via define-type-constructor
+; ;; - app, other compound types, like variants
+; ;; - ow, the type checking in #%app will fail
+; ;; (could leave this case out until adding variants but it's general
+; ;; enough, so leave it here)
+; ;; could match specific type constructors like → before expanding
+; ;; but this is more general and wont require subsequent extensions for
+; ;; every defined type constructor
+; (syntax-parse (local-expand τ 'expression (list app #'#%app))
+; ; full expansion checks for undefined types
+; [x:id (local-expand #'x 'expression null)]
+; [((~literal #%app) tcon t ...)
+; #`(tcon #,@(stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...)))]
+; ; else just structurually eval
+; [(t ...) (stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...))]))
+ (current-type-eval type-eval))
(begin-for-syntax
;; type=? : Type Type -> Boolean
;; Indicates whether two types are equal
- ;; type equality = structurally recursive identifier equality
- ;; structurally checks for free-identifier=?
+ ;; type equality = structurally free-identifier=?
(define (type=? τ1 τ2)
-; (printf "t1 = ~a\n" (syntax->datum τ1))
-; (printf "t2 = ~a\n" (syntax->datum τ2))
+; (printf "(τ=) t1 = ~a\n" τ1 #;(syntax->datum τ1))
+; (printf "(τ=) t2 = ~a\n" τ2 #;(syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(x:id y:id) (free-identifier=? τ1 τ2)]
[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
@@ -67,6 +67,10 @@
(syntax-parse stx
[(_ (b:typed-binding ...) e)
#:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
+; #:with (a as ...) #'(b.τ ...)
+; #:when (printf "lam: ~a\n" (free-identifier=? #'a #'τ_res))
+; #:with (lam (aa) resres) (local-expand #'(λ (a) τ_res) 'expression null)
+; #:when (printf "lam2: ~a\n" (free-identifier=? #'aa #'resres))
(⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
(define-syntax (app/tc stx)
@@ -76,7 +80,7 @@
#:fail-unless (→? #'τ_fn)
(format "Type error: Attempting to apply a non-function ~a with type ~a\n"
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
- #:with (_ τ ... τ_res) #'τ_fn
+ #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
#:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
(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=? eval-τ)
- (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ type=? eval-τ)))
+(require (except-in "stlc+lit.rkt" #%app λ type=?)
+ (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ type=?)))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app
- (for-syntax stlc:type=? stlc:eval-τ)))
+ (for-syntax stlc:type=?)))
(provide Λ inst)
-(provide (for-syntax type=? eval-τ))
+(provide (for-syntax type=?))
;; System F
@@ -19,25 +19,39 @@
;; - terms from stlc+lit.rkt
;; - Λ and inst
-(define-type-constructor ∀)
+;; dont use define-type-constructor, instead define explicit macro
+(provide ∀)
+(define-syntax (∀ stx)
+ (syntax-parse stx
+ [(_ (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))]))
(begin-for-syntax
;; Extend to handle ∀, skip typevars
- (define (eval-τ τ [tvs #'()] . rst)
- (syntax-parse τ
- [x:id #:when (stx-member τ tvs) τ]
- [((~literal ∀) ts t-body)
- #`(∀ ts #,(apply (current-τ-eval) #'t-body (stx-append tvs #'ts) rst))]
- ;; need to duplicate stlc:eval-τ here to pass extra params
- [_ (apply stlc:eval-τ τ tvs rst)]))
- (current-τ-eval eval-τ)
+; #;(define (type-eval τ [tvs #'()] . rst)
+; (syntax-parse τ
+; [x:id #:when (stx-member τ tvs) τ]
+; [((~literal ∀) ts t-body)
+; #`(∀ ts #,(apply (current-τ-eval) #'t-body (stx-append tvs #'ts) rst))]
+; ;; need to duplicate stlc:eval-τ here to pass extra params
+; [_ (apply stlc:eval-τ τ tvs rst)]))
+; #;(current-type-eval type-eval)
;; extend to handle ∀
(define (type=? τ1 τ2)
- (syntax-parse (list τ1 τ2) #:literals (∀)
- [((∀ (x:id ...) t1) (∀ (y:id ...) t2))
+ (syntax-parse (list τ1 τ2)
+ [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
+ ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
#:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
#:with (z ...) (generate-temporaries #'(x ...))
+ ;#:when (typechecks? #'(k1 ...) #'(k2 ...))
+; #:when (printf "t1 = ~a\n" (syntax->datum #'t1))
+; #:when (printf "t2 = ~a\n" (syntax->datum #'t2))
+; #:when (printf "~a\n"
+; (map syntax->datum
+ ; (list (substs #'(z ...) #'(x ...) #'t1)
+; (substs #'(z ...) #'(y ...) #'t2))))
((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
(substs #'(z ...) #'(y ...) #'t2))]
[_ (stlc:type=? τ1 τ2)]))
@@ -51,8 +65,7 @@
(⊢ #'e- #'(∀ tvs- τ))]))
(define-syntax (inst stx)
(syntax-parse stx
- [(_ e τ ...)
- #:with (e- τ_e) (infer+erase #'e)
- #:with ((~literal ∀) (tv ...) τ_body) #'τ_e
- #:with (τ+ ...) (stx-map (current-τ-eval) #'(τ ...))
- (⊢ #'e- (substs #'(τ+ ...) #'(tv ...) #'τ_body))]))
-\ No newline at end of file
+ [(_ e τ:type ...)
+ #: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/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -2,20 +2,53 @@
(require "rackunit-typechecking.rkt")
(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
(check-type (→ Int Int) : ★)
(typecheck-fail (→ →))
+(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 : X]) x)))
+ : (∀ ([X : ★]) (→ X X )))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+
+;(check-type (λ ([x : (∀ ([t : ★]) t)]) x) : (→ (∀ ([t : ★]) t) (∀ ([t : ★]) t)))
+;(check-type (λ ([x : (∀ ([t : (⇒ ★ ★)]) (tyapp t Int))]) x) : Int #;(→ (∀ ([t : (⇒ ★ ★)]) t) (∀ ([t : (⇒ ★ ★)]) t)))
-(typecheck-fail (λ ([x : (→ →)]) x))
+;(check-type 1 : (tyapp (tyλ ([X : ★]) X) Int))
+;(check-not-type 1 : (tyapp (tyλ ([X : ★]) X) String))
+;
+;;(check-type (λ ([x : Int]) x) : (tyapp (tyλ ([X : ★]) (→ X X)) Int))
+;
+;; Mono Pair
+;#;(tyapp (tyλ ([Pair : (⇒ ★ ★)]) (λ ([p : (tyapp Pair Int)]) p))
+; (tyλ ([X : ★]) (∀ ([P : ★]) (→ (→ X X P) P))))
+;
+;
+;;(check-type Int : ★)
+;;(check-type (→ Int Int) : ★)
+;;(typecheck-fail (→ →))
+;
+;(typecheck-fail (λ ([x : (→ →)]) x))
+;
+;(typecheck-fail (λ ([x : (∀ (t) t)]) x)) ; missing kind annotation
+;(check-type (∀ ([t : ★]) t) : ★)
+;(check-type (∀ ([→ : ★]) →) : ★) ; should be ok
+;(check-type (∀ ([t : ★]) (∀ ([s : ★]) (→ t s))) : ★)
+;(check-type (∀ ([t : ★] [s : ★]) (→ t s)) : ★)
+;;(check-type (∀ ([t : (⇒ ★ ★)] [s : ★]) (t s)) : ★) ; doesnt work yet
+;(typecheck-fail (∀ (t) (→ →)))
+;
+;;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
-(typecheck-fail (∀ (t) t)) ; missing kind annotation
-(check-type (∀ ([t : ★]) t) : ★)
-(check-type (∀ ([→ : ★]) →) : ★) ; should be ok
-(check-type (∀ ([t : ★]) (∀ ([s : ★]) (→ t s))) : ★)
-(check-type (∀ ([t : ★] [s : ★]) (→ t s)) : ★)
-;(check-type (∀ ([t : (⇒ ★ ★)] [s : ★]) (t s)) : ★) ; doesnt work yet
-(typecheck-fail (∀ (t) (→ →)))
+(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
-;; sysf tests wont work, must be augmented with kinds
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
@@ -58,7 +91,6 @@
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
(typecheck-fail #f) ; unsupported literal
(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
(check-not-type (λ ([x : Int]) x) : Int)
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -5,10 +5,9 @@
(define-syntax (check-type stx)
(syntax-parse stx #:datum-literals (:)
[(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
- [(_ e : τ-expected)
+ [(_ e : τ-expected:type)
#:with τ (typeof (expand/df #'e))
- #:with τ-expected+ ((current-τ-eval) #'τ-expected)
- #:fail-unless (typecheck? #'τ #'τ-expected+)
+ #:fail-unless (typecheck? #'τ #'τ-expected.norm)
(format
"Expression ~a [loc ~a:~a] has type ~a, expected ~a"
(syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -17,10 +16,9 @@
(define-syntax (check-not-type stx)
(syntax-parse stx #:datum-literals (:)
- [(_ e : not-τ)
+ [(_ e : not-τ:type)
#:with τ (typeof (expand/df #'e))
- #:with not-τ+ ((current-τ-eval) #'not-τ)
- #:fail-when (typecheck? #'τ #'not-τ)
+ #:fail-when (typecheck? #'τ #'not-τ.norm)
(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
@@ -10,4 +10,5 @@
(require "stlc+sub-tests.rkt")
(require "stlc+rec+sub-tests.rkt")
-(require "sysf-tests.rkt")
-\ No newline at end of file
+;(require "sysf-tests.rkt")
+;(require "fomega-tests.rkt")
+\ No newline at end of file
diff --git a/tapl/tests/stlc+box-tests.rkt b/tapl/tests/stlc+box-tests.rkt
@@ -13,6 +13,9 @@
(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
+(typecheck-fail (λ ([lst : (Ref Int Int)]) lst)) ; type constructor wrong arity
+(typecheck-fail (λ ([lst : (Ref)]) lst)) ; type constructor wrong arity
+
;; previous tests: ------------------------------------------------------------
(typecheck-fail (cons 1 2))
(typecheck-fail (cons 1 nil))
@@ -45,10 +48,9 @@
(check-type + : ArithBinOp)
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
-;; records (ie labeled tuples)
(check-type "Stephen" : String)
(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["male?" Bool]))
+ (× [: "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")
@@ -58,47 +60,48 @@
(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]))
+ (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+ (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+ (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
- (var "coffee" = (void) as (∨ ["coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
- : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit]))
+(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x)
+ (var "coffee" = (void) as (∨ [: "coffee" Unit]))))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+ : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+ : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["teaaaaaa" x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["tea" x => 2]
["coke" x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => "1"]
["tea" x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit]))
+ (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
["coffee" x => x]
["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))
+(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])))
+ (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
["coffee" x => (+ (+ x x) (+ x x))]
["tea" x => 2]
["coke" y => 3])
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
@@ -7,6 +7,8 @@
(typecheck-fail nil)
(typecheck-fail (nil Int))
(typecheck-fail (nil (Int)))
+(typecheck-fail (λ ([lst : (List Int Int)]) lst)) ; type constructor wrong arity
+(typecheck-fail (λ ([lst : (List)]) lst)) ; type constructor wrong arity
; passes bc ⇒-rhs is only used for its runtime value
(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
(check-not-type (nil {Bool}) : (List Int))
@@ -35,7 +37,7 @@
;; records (ie labeled tuples)
(check-type "Stephen" : String)
(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["male?" Bool]))
+ (× [: "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")
@@ -45,47 +47,48 @@
(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]))
+ (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+ (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+ (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
- (var "coffee" = (void) as (∨ ["coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
- : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit]))
+(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x)
+ (var "coffee" = (void) as (∨ [: "coffee" Unit]))))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+ : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+ : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["teaaaaaa" x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["tea" x => 2]
["coke" x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => "1"]
["tea" x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit]))
+ (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
["coffee" x => x]
["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))
+(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])))
+ (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
["coffee" x => (+ (+ x x) (+ x x))]
["tea" x => 2]
["coke" y => 3])
diff --git a/tapl/tests/stlc+rec+sub-tests.rkt b/tapl/tests/stlc+rec+sub-tests.rkt
@@ -3,27 +3,29 @@
;; record subtyping tests
(check-type "coffee" : String)
-(check-type (tup ["coffee" = 3]) : (× ["coffee" Int])) ; element subtyping
-(check-type (tup ["coffee" = 3]) : (× ["coffee" Nat]))
-(check-type (tup ["coffee" = 3]) : (× ["coffee" Top]))
-(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
+(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)]))
;; 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]))
+ (× [: "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")
@@ -33,11 +35,11 @@
(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]))
+ (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+ (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+ (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
;; previous basic subtyping tests ------------------------------------------------------
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
@@ -15,7 +15,7 @@
;; records (ie labeled tuples)
(check-type "Stephen" : String)
(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["male?" Bool]))
+ (× [: "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")
@@ -25,47 +25,47 @@
(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]))
+ (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+ (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+ (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
;; variants
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
- (var "coffee" = (void) as (∨ ["coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
- : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit]))
+(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x)
+ (var "coffee" = (void) as (∨ [: "coffee" Unit]))))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+ : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["teaaaaaa" x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => 1]
["tea" x => 2]
["coke" x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
["coffee" x => "1"]
["tea" x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit]))
+ (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
["coffee" x => x]
["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))
+(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])))
+ (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
["coffee" x => (+ (+ x x) (+ x x))]
["tea" x => 2]
["coke" y => 3])
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -1,6 +1,12 @@
#lang s-exp "../sysf.rkt"
(require "rackunit-typechecking.rkt")
+(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)))))
@@ -17,7 +23,7 @@
; second inst is discarded
(check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
-;; polymorphic arguments
+;;; 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))))
@@ -40,7 +46,7 @@
: Int ⇒ 10)
-;; previous tests -------------------------------------------------------------
+;;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
(typecheck-fail "one") ; unsupported literal
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -31,34 +31,76 @@
(define τ (void))
(define-for-syntax (τ? τ1) (typecheck? τ1 #'τ)))]))
+(struct exn:fail:type:runtime exn:fail:user ())
+
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
(define-syntax (define-type-constructor stx)
(syntax-parse stx
- [(_ τ:id)
+ [(_ τ:id (~optional (~seq #:arity n:exact-positive-integer)))
#:with τ? (format-id #'τ "~a?" #'τ)
- #'(begin
- (provide τ (for-syntax τ?))
+ #:with τ-ref (format-id #'τ "~a-ref" #'τ)
+ #:with τ-num-args (format-id #'τ "~a-num-args" #'τ)
+ #:with τ-args (format-id #'τ "~a-args" #'τ)
+ #:with tmp (generate-temporary #'τ)
+ #`(begin
+ ;; TODO: define syntax class instead of these separate tycon fns
+ (provide τ (for-syntax τ? τ-ref τ-num-args τ-args))
+ (define tmp (λ _ (raise (exn:fail:type:runtime
+ (format "~a: Cannot use type at run time" 'τ)
+ (current-continuation-marks)))))
(define-syntax (τ stx)
(syntax-parse stx
[x:id
(type-error #:src #'x
- #:msg "Cannot use type constructor in non-application position")]
- [(_) (type-error #:src stx
- #:msg "Type constructor must have at least one argument.")]
+ #:msg "Cannot use type constructor ~a in non-application position"
+ #'τ)]
+ [(_) ; default tycon requires 1+ args
+ #:when (not #,(attribute n))
+ (type-error #:src stx
+ #:msg "Type constructor must have at least 1 argument.")]
+ [(_ x (... ...))
+ #:when #,(and (attribute n)
+ #'(not (= n (stx-length #'(x (... ...))))))
+ #:with m #,(and (attribute n) #'n)
+ (type-error #:src stx
+ #:msg "Type constructor ~a expected ~a argument(s), given: ~a"
+ #'τ #'m #'(x (... ...)))]
; this is racket's #%app
- [(_ x (... ...)) #'(#%app τ x (... ...))]))
+ [(_ x (... ...)) #'(tmp x (... ...))]))
+ ; TODO: ok to assume type in canonical (ie, fully expanded) form?
+ ;; yes for now
(define-for-syntax (τ? stx)
- (syntax-parse ((current-τ-eval) stx)
- [(τcons τ_arg (... ...)) (typecheck? #'τcons #'τ)]
- [_ #f])))]))
+ (syntax-parse stx
+ [((~literal #%plain-app) tycon τ_arg (... ...)) (typecheck? #'tycon #'tmp)]
+ [_ #f]))
+ (define-for-syntax (τ-ref stx m)
+ (syntax-parse stx
+ [((~literal #%plain-app) tycon τ_arg (... ...))
+ #:when (typecheck? #'tycon #'tmp)
+ (stx-list-ref #'(τ_arg (... ...)) m)]))
+ (define-for-syntax (τ-args stx)
+ (syntax-parse stx
+ [((~literal #%plain-app) tycon τ_arg (... ...))
+ #:when (typecheck? #'tycon #'tmp)
+ #'(τ_arg (... ...))]))
+ (define-for-syntax (τ-num-args stx)
+ (syntax-parse stx
+ [((~literal #%plain-app) tycon τ_arg (... ...))
+ #:when (typecheck? #'tycon #'tmp)
+ (stx-length #'(τ_arg (... ...)))])))]))
;; syntax classes
(begin-for-syntax
(define-syntax-class type
- (pattern τ:expr))
+ ;; stx = surface syntax, as written
+ ;; norm = canonical form for the type
+ (pattern stx:expr
+ #:with norm ((current-type-eval) #'stx)
+ #:with τ #'norm)) ; backwards compat
+; #:with τ #'stx)) ; backwards compat
(define-syntax-class typed-binding #:datum-literals (:)
- (pattern [x:id : τ:type])
+ (pattern [x:id : stx:type] #:with τ #'stx.τ)
(pattern (~and any (~not [x:id : τ:type]))
#:with x #f
#:with τ #f
@@ -78,11 +120,13 @@
;; ⊢ : Syntax Type -> Syntax
;; Attaches type τ to (expanded) expression e.
;; must eval here, to catch unbound types
- (define (⊢ e τ) (syntax-property e 'type ((current-τ-eval) τ)))
+ (define (⊢ e τ)
+ (syntax-property e 'type (syntax-local-introduce ((current-type-eval) τ))))
+
;; typeof : Syntax -> Type or #f
;; Retrieves type of given stx, or #f if input has not been assigned a type.
(define (typeof stx) (syntax-property stx 'type))
-
+
;; 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)
@@ -105,27 +149,9 @@
#'(λ (x ...)
(let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
(#%expression e) ...)))
- (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
+ (list #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)]))
- #;(define (eval-τ τ [tvs #'()])
- (syntax-parse τ
- [x:id #:when (stx-member τ tvs) τ]
- [s:str τ] ; record field
- [((~and (~datum ∀) forall) ts τ) #`(forall ts #,(eval-τ #'τ #'ts))]
- [_
- (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
- ;; stop right before expanding #%app
- (define maybe-app-τ (local-expand τ 'expression (list app)))
- ;; manually remove app and recursively expand
- (if (identifier? maybe-app-τ) ; base type
- ;; full expansion checks that type is a bound name
- (local-expand maybe-app-τ 'expression null)
- (syntax-parse maybe-app-τ
- [(τ1 ...)
- #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ1 ...))
- #'(τ-exp ...)]))]))
-
;; infers the type and erases types in an expression
(define (infer+erase e)
(define e+ (expand/df e))
@@ -136,15 +162,17 @@
;; infers and erases types in an expression, in the context of given type vars
(define (infer/tvs+erase e [tvs #'()])
(syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
- [(lam tvs+ (#%expression e+)) (list #'tvs+ #'e+ (typeof #'e+))]))
+ [(lam tvs+ (#%expression e+))
+ (list #'tvs+ #'e+ (syntax-local-introduce (typeof #'e+)))]))
(define current-typecheck-relation (make-parameter #f))
(define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
(define (typechecks? τs1 τs2)
(stx-andmap (current-typecheck-relation) τs1 τs2))
- (define current-τ-eval (make-parameter #f))
+ (define current-type-eval (make-parameter #f))
+ (require inspect-syntax)
;; term expansion
;; expand/df : Syntax -> Syntax
;; Local expands the given syntax object.
@@ -156,16 +184,20 @@
(define (expand/df e)
(local-expand e 'expression null))
- ;; type-error #:src Syntax #:msg String Syntax ...
+ (struct exn:fail:type:check exn:fail:user ())
+
+;; type-error #:src Syntax #:msg String Syntax ...
;; usage:
;; type-error #:src src-stx
;; #:msg msg-string msg-args ...
(define-syntax-rule (type-error #:src stx-src #:msg msg args ...)
- (raise-user-error
- 'TYPE-ERROR
- (format (string-append "~a (~a:~a): " msg)
- (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
- (syntax->datum args) ...))))
+ (raise
+ (exn:fail:type:check
+ (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg)
+ (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
+ (syntax->datum args) ...)
+ (current-continuation-marks)))))
+
(define-syntax (define-primop stx)
(syntax-parse stx #:datum-literals (:)
@@ -186,11 +218,15 @@
(define-for-syntax (subst τ x e)
(syntax-parse e
- [y:id #:when (free-identifier=? e x) τ]
+ [y:id
+; #:when (printf "~a = ~a? = ~a\n" #'y x (free-identifier=? e x))
+; #:when (printf "~a = ~a? = ~a\n" #'y x (bound-identifier=? e x))
+ #:when (bound-identifier=? e x)
+ τ]
[y:id #'y]
[(esub ...)
#:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
- #'(esub_subst ...)]))
+ (syntax-track-origin #'(esub_subst ...) e x)]))
(define-for-syntax (substs τs xs e)
(stx-fold subst e τs xs))
