From bf126449b4213a3e71f7ffbf45dfd8b317862944 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 9 Oct 2015 16:59:48 -0400 Subject: [PATCH] define-type-constructor supports annotated bound vars - use this to impl forall in fomega - define-type-constructor default arity is =1 - define explicit normalize fn in fomega -- speeds up tests 15% - move same-type to define-syntax-category --- tapl/exist.rkt | 2 +- tapl/fomega.rkt | 86 ++++++++++++++---------------------------- tapl/fomega2.rkt | 4 +- tapl/fomega3.rkt | 2 +- tapl/notes.txt | 10 +++++ tapl/stlc+box.rkt | 2 +- tapl/stlc+cons.rkt | 2 +- tapl/stlc+rec-iso.rkt | 2 +- tapl/stlc+reco+var.rkt | 14 ++----- tapl/stlc+tup.rkt | 2 +- tapl/sysf.rkt | 2 +- tapl/typecheck.rkt | 68 ++++++++++++++++++++++----------- 12 files changed, 97 insertions(+), 99 deletions(-) diff --git a/tapl/exist.rkt b/tapl/exist.rkt index 5150901..2e62982 100644 --- a/tapl/exist.rkt +++ b/tapl/exist.rkt @@ -12,7 +12,7 @@ ;; Other: type=? from stlc+rec-iso.rkt -(define-type-constructor ∃ #:arity = 1 #:bvs = 1) +(define-type-constructor ∃ #:bvs = 1) (define-typed-syntax pack [(_ (τ:type e) as ∃τ:type) diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt index 3207c2e..a7b687f 100644 --- a/tapl/fomega.rkt +++ b/tapl/fomega.rkt @@ -1,6 +1,6 @@ #lang s-exp "typecheck.rkt" -(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀]) -(reuse String #%datum same-types? #:from "stlc+reco+var.rkt") +(extends "sysf.rkt" #:except #%datum ∀ Λ inst) +(reuse String #%datum #:from "stlc+reco+var.rkt") ;; System F_omega ;; Type relation: @@ -35,64 +35,36 @@ #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ)) #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) -(begin-for-syntax - (define sysf:type-eval (current-type-eval)) - ;; extend type-eval to handle tyapp - ;; - requires manually handling all other forms - (define (type-eval τ) - (syntax-parse τ - [((~literal #%plain-app) τ_fn τ_arg ...) - #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn) - #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...)) - (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)] - [((~or (~literal ∀)(~literal →) - (~literal ⇒)(~literal tyapp)) . _) - ((current-type-eval) (sysf:type-eval τ))] - [((~literal #%plain-lambda) (x ...) τ_body ...) - #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...)) - (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)] - [_ (sysf:type-eval τ)])) ; dont eval under tyλ - (current-type-eval type-eval)) (define-base-kind ★) (define-kind-constructor ⇒ #:arity >= 1) (define-kind-constructor ∀★ #:arity >= 0) -(define-typed-syntax ∀ #:export-as ∀ - [(_ bvs:kind-ctx τ_body) - ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type - #:with (tvs- τ_body- k_body) - (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval)) - ; expand so kind gets overwritten - (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]) +(define-type-constructor ∀ #:bvs >= 0 #:arr ∀★) + +;; alternative: normalize before type=? +; but then also need to normalize in current-promote (begin-for-syntax - (define-syntax ~∀ - (pattern-expander - (syntax-parser #:datum-literals (:) - [(_ ([tv:id : k] ...) τ) - #:with ∀τ (generate-temporary) - #'(~and ∀τ - (~parse (~sysf:∀ (tv ...) τ) #'∀τ) - (~parse (~∀★ k ...) (typeof #'∀τ)))] - [(_ . args) - #:with ∀τ (generate-temporary) - #'(~and ∀τ - (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ) - (~parse (~∀★ k (... ...)) (typeof #'∀τ)) - (~parse args #'(([tv k] (... ...)) τ)))]))) - (define-syntax ~∀* - (pattern-expander - (syntax-parser #:datum-literals (<:) - [(_ . args) - #'(~or - (~∀ . args) - (~and any (~do - (type-error - #:src #'any - #:msg "Expected ∀ type, got: ~a" #'any))))]))) + (define (normalize τ) + (syntax-parse τ + [x:id #'x] + [((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) + (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] + [((~literal #%plain-lambda) (x ...) . bodys) + #:with bodys_norm (stx-map normalize #'bodys) + (syntax-track-origin #'(#%plain-lambda (x ...) . bodys_norm) τ #'plain-lambda)] + [((~literal #%plain-app) x:id . args) + #:with args_norm (stx-map normalize #'args) + (syntax-track-origin #'(#%plain-app x . args_norm) τ #'#%plain-app)] + [((~literal #%plain-app) . args) + #:with args_norm (stx-map normalize #'args) + (syntax-track-origin (normalize #'(#%plain-app . args_norm)) τ #'#%plain-app)] + [_ τ])) + + (define old-eval (current-type-eval)) + (define (type-eval τ) (normalize (old-eval τ))) + (current-type-eval type-eval) + (define old-type=? (current-type=?)) (define (type=? t1 t2) (or (and (★? t1) (#%type? t2)) @@ -109,12 +81,12 @@ (define-typed-syntax Λ [(_ bvs:kind-ctx e) #:with ((tv- ...) e- τ_e) - (infer/ctx+erase #'bvs #'e); #:expand (current-type-eval)) + (infer/ctx+erase #'bvs #'e #:expand (current-type-eval)) (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]) (define-typed-syntax inst [(_ e τ ...) - #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀) + #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀) #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval)) #:when (stx-andmap @@ -122,7 +94,7 @@ (type-error #:src t #:msg "not a valid type: ~a" t))) #'(τ ...) #'(k_τ ...)) #:when (typechecks? #'(k_τ ...) #'(k ...)) - (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]) + (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]) ;; TODO: merge with regular λ and app? ;; - see fomega2.rkt diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt index 6de8cbd..a81d0c2 100644 --- a/tapl/fomega2.rkt +++ b/tapl/fomega2.rkt @@ -1,6 +1,6 @@ #lang s-exp "typecheck.rkt" (extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀]) -(reuse String #%datum same-types? #:from "stlc+reco+var.rkt") +(reuse String #%datum #:from "stlc+reco+var.rkt") ; same as fomega.rkt except here λ and #%app works as both type and terms ; - uses definition from stlc, but tweaks type? and kind? predicates @@ -118,4 +118,4 @@ (type-error #:src t #:msg "not a valid type: ~a" t))) #'(τ ...) #'(k_τ ...)) #:when (typechecks? #'(k_τ ...) #'(k ...)) - (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]) \ No newline at end of file + (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]) \ No newline at end of file diff --git a/tapl/fomega3.rkt b/tapl/fomega3.rkt index 1ed6a8e..dd219f4 100644 --- a/tapl/fomega3.rkt +++ b/tapl/fomega3.rkt @@ -1,6 +1,6 @@ #lang s-exp "typecheck.rkt" (extends "sysf.rkt" #:except #%datum ∀ Λ inst) -(reuse String #%datum same-types? #:from "stlc+reco+var.rkt") +(reuse String #%datum #:from "stlc+reco+var.rkt") (reuse current-kind? ∀★ ∀★? ★ ★? kind? ∀ Λ inst define-type-alias #:from "fomega.rkt") ; same as fomega2.rkt --- λ and #%app works as both regular and type versions, diff --git a/tapl/notes.txt b/tapl/notes.txt index de1075e..d69fd0f 100644 --- a/tapl/notes.txt +++ b/tapl/notes.txt @@ -1,3 +1,13 @@ +2015-10-09 +TODO: variant case should call current-join? + +2015-10-09 +Can I get rid of current-type-eval? +- would have to put "normalize" call in type=? +- and call normalize in current-promote (before pattern matching) + +Thus, it's probably better to keep type-eval + 2015-08-16: TODO: - generalize binding forms diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt index f5e9cd4..8211cc3 100644 --- a/tapl/stlc+box.rkt +++ b/tapl/stlc+box.rkt @@ -9,7 +9,7 @@ ;; - terms from stlc+cons.rkt ;; - ref deref := -(define-type-constructor Ref #:arity = 1) +(define-type-constructor Ref) (define-typed-syntax ref [(_ e) diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index 16e5318..6ed26ea 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -10,7 +10,7 @@ ;; TODO: enable HO use of list primitives -(define-type-constructor List #:arity = 1) +(define-type-constructor List) (define-typed-syntax nil [(_ ~! τi:type-ann) (⊢ null : (List τi.norm))] diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt index 8e8c714..336179c 100644 --- a/tapl/stlc+rec-iso.rkt +++ b/tapl/stlc+rec-iso.rkt @@ -14,7 +14,7 @@ ;; Other: ;; - extend type=? to handle lambdas -(define-type-constructor μ #:arity = 1 #:bvs = 1) +(define-type-constructor μ #:bvs = 1) (begin-for-syntax (define stlc:type=? (current-type=?)) diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt index bf8ff05..af118de 100644 --- a/tapl/stlc+reco+var.rkt +++ b/tapl/stlc+reco+var.rkt @@ -1,7 +1,7 @@ #lang s-exp "typecheck.rkt" (extends "stlc+tup.rkt" #:except × ×? tup proj #:rename [~× ~stlc:×]) -(provide × ∨ (for-syntax same-types? ~× ~×* ~∨ ~∨*)) +(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*)) ;; Simply-Typed Lambda Calculus, plus records and variants @@ -16,20 +16,12 @@ ;; TopLevel: ;; - define (values only) ;; - define-type-alias -;; Typechecking forms -;; - same-types? - -(begin-for-syntax - (define (same-types? τs) - (define τs-lst (syntax->list τs)) - (or (null? τs-lst) - (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst))))) (provide define-type-alias) (define-syntax define-type-alias (syntax-parser [(_ alias:id τ:type) - #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))])) + #'(define-syntax alias (make-variable-like-transformer #'τ.norm) #;(syntax-parser [x:id #'τ.norm]))])) (define-typed-syntax define [(_ x:id e) @@ -76,7 +68,7 @@ #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...)) (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]) -(define-type-constructor ∨/internal) +(define-type-constructor ∨/internal #:arity >= 0) ;; variants (define-syntax ∨ diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt index c0d6eaf..2558993 100644 --- a/tapl/stlc+tup.rkt +++ b/tapl/stlc+tup.rkt @@ -9,7 +9,7 @@ ;; - terms from ext-stlc.rkt ;; - tup and proj -(define-type-constructor ×) ; default arity >=0 +(define-type-constructor × #:arity >= 0) (define-typed-syntax tup [(_ e ...) diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt index 7177274..33d1332 100644 --- a/tapl/sysf.rkt +++ b/tapl/sysf.rkt @@ -12,7 +12,7 @@ ;; - terms from stlc+lit.rkt ;; - Λ and inst -(define-type-constructor ∀ #:arity = 1 #:bvs >= 0) +(define-type-constructor ∀ #:bvs >= 0) (define-typed-syntax Λ [(_ (tv:id ...) e) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index ec9c8d5..1d20234 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -339,6 +339,7 @@ (define-syntax define-basic-checked-id-stx (syntax-parser #:datum-literals (:) [(_ τ:id : kind) + #:with #%tag (format-id #'kind "#%~a" #'kind) #:with τ? (mk-? #'τ) #:with τ-internal (generate-temporary #'τ) #:with τ-expander (format-id #'τ "~~~a" #'τ) @@ -366,12 +367,12 @@ [(_ . rst) #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) (define τ-internal (λ () (raise (exn:fail:type:runtime - (format "~a: Cannot use type at run time" 'τ) + (format "~a: Cannot use ~a at run time" 'τ 'kind) (current-continuation-marks))))) (define-syntax τ (syntax-parser ;[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))])) - [(~var _ id) (add-orig (assign-type #'(τ-internal) #'kind) #'τ)])))])) + [(~var _ id) (add-orig (assign-type #'(τ-internal) #'#%tag) #'τ)])))])) ; I use identifiers "τ" and "kind" but this form is not restricted to them. ; E.g., τ can be #'★ and kind can be #'#%kind (★'s type) @@ -380,33 +381,42 @@ [(_ τ:id : kind (~optional (~seq #:arity op n:exact-nonnegative-integer) - #:defaults ([op #'>=] [n #'0])) + #:defaults ([op #'=] [n #'1])) (~optional - (~seq #:bvs (~and has-bvs? bvs-op) bvs-n:exact-nonnegative-integer) - #:defaults ([bvs-op #'>=][bvs-n #'0]))) + (~seq #:bvs (~and (~parse has-bvs? #'#t) bvs-op) bvs-n:exact-nonnegative-integer) + #:defaults ([bvs-op #'=][bvs-n #'0])) + (~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon)) + #:defaults ([tycon #'void]))) #:with #%kind (format-id #'kind "#%~a" #'kind) #:with τ-internal (generate-temporary #'τ) #:with τ? (mk-? #'τ) #:with τ-expander (format-id #'τ "~~~a" #'τ) #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander) #`(begin - (provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase)) + (provide τ (for-syntax τ-expander τ-expander* τ?)) (begin-for-syntax (define-syntax τ-expander (pattern-expander (syntax-parser [(_ . pat:id) - #'(~and #;((~literal #%plain-lambda) bvs - ((~literal #%plain-app) (~literal τ-internal) . rst)) - ((~literal #%plain-app) (~literal τ-internal) ((~literal #%plain-lambda) bvs (~literal void) . rst)) + #:with expanded-τ (generate-temporary) + #:with tycon-expander (format-id #'tycon "~~~a" #'tycon) + #'(~and expanded-τ + (~parse + ((~literal #%plain-app) (~literal τ-internal) + ((~literal #%plain-lambda) (~and bvs (tv (... (... ...)))) (~literal void) . rst)) + #'expanded-τ) #,(if (attribute has-bvs?) - #'(~parse pat #'(bvs rst)) + (if (attribute has-annotations?) + #'(~and (~parse (tycon-expander k (... (... ...))) (typeof #'expanded-τ)) + (~parse pat #'(([tv k] (... (... ...))) rst))) + #'(~parse pat #'(bvs rst))) #'(~parse pat #'rst)))] + ;; TODO: fix this to handle has-annotations? [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) bvs-pat) #:defaults ([bvs-pat #'()])) . pat) - #'((~literal #%plain-app) (~literal τ-internal) ((~literal #%plain-lambda) bvs-pat (~literal void) . pat)) - #;((~literal #%plain-lambda) bvs-pat - ((~literal #%plain-app) (~literal τ-internal) . pat))]))) + #'((~literal #%plain-app) (~literal τ-internal) + ((~literal #%plain-lambda) bvs-pat (~literal void) . pat))]))) (define-syntax τ-expander* (pattern-expander (syntax-parser @@ -430,25 +440,34 @@ [_ #f])))) (define τ-internal (λ _ (raise (exn:fail:type:runtime - (format "~a: Cannot use type at run time" 'τ) + (format "~a: Cannot use ~a at run time" 'τ 'kind) (current-continuation-marks))))) ;; ; this is the actual constructor (define-syntax (τ stx) (syntax-parse stx [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) - (bv (... ...))) + (~or (bv:id (... ...)) + (~and (~fail #:unless #,(attribute has-annotations?)) + bvs+ann))) #:defaults ([(bv 1) null])) . args) - #:with bvs #'(bv (... ...)) + #:with bvs (if #,(attribute has-annotations?) + #'bvs+ann + #'([bv : #%kind] (... ...))) + ;#:declare bvs ctx ; can't assume kind-ctx is defined #: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 (bvs- τs- _) - (infers/ctx+erase #'([bv : #%kind] (... ...)) #'args + (infers/ctx+erase #'bvs #'args ;#'([bv : #%kind] (... ...)) #'args #:expand (current-type-eval)) #:with (~! (~var _ kind) (... ...)) #'τs- - ;(assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind) - (assign-type #'(τ-internal (λ bvs- void . τs-)) #'#%kind)] + #:with ([tv (~datum :) k_arg] (... ...)) #'bvs + #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...))) + #:with k_result (if #,(attribute has-annotations?) + #'(tycon k_arg+ (... ...)) + #'#%kind) + (assign-type #'(τ-internal (λ bvs- void . τs-)) #'k_result)] ;; else fail with err msg [_ (type-error #:src stx @@ -476,8 +495,9 @@ #:with name=? (format-id #'name "~a=?" #'name) #:with names=? (format-id #'names "~a=?" #'names) #:with current-name=? (format-id #'name=? "current-~a" #'name=?) + #:with same-names? (format-id #'name "same-~as?" #'name) #'(begin - (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx) + (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx same-names?) #%tag define-base-name define-name-cons) (define #%tag void) (begin-for-syntax @@ -536,10 +556,14 @@ (current-typecheck-relation name=?) (define (names=? τs1 τs2) (and (stx-length=? τs1 τs2) - (stx-andmap (current-name=?) τs1 τs2)))) + (stx-andmap (current-name=?) τs1 τs2))) + (define (same-names? τs) + (define τs-lst (syntax->list τs)) + (or (null? τs-lst) + (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst))))) (define-syntax define-base-name (syntax-parser - [(_ (~var x id)) #'(define-basic-checked-id-stx x : #%tag)])) + [(_ (~var x id)) #'(define-basic-checked-id-stx x : name)])) (define-syntax define-name-cons (syntax-parser [(_ (~var x id) . rst) #'(define-basic-checked-stx x : name . rst)])))]))