commit bf126449b4213a3e71f7ffbf45dfd8b317862944
parent dad2c26c496c3232b76d354a1d9f25e9c1d3e08a
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 9 Oct 2015 16:59:48 -0400
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
Diffstat:
12 files changed, 98 insertions(+), 100 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)])))]))
