suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

generalize infer's ctx to use let* semantics and arbitrary sep+keys

Browse Source 
- allow lone ids that default to tyvars
This commit is contained in:
Stephen Chang 2017-02-07 17:18:07 -05:00
parent 1a3f208903
commit d2e93bb1c9
15 changed files with 158 additions and 407 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
macrotypes/examples/exist.rkt
View File

@ -67,8 +67,5 @@
;;
#:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed)
#:with τ_x (subst #'X #'Y #'τ_body)
#:with [(X-) (x-) (e-) (τ_e)]
(infer #'(e)
#:tvctx #'([X :: #%type])
#:ctx #`([x : τ_x]))
#:with [(_ x-) e- τ_e] (infer/ctx+erase #'(X [x : τ_x]) #'e)
(⊢ (let- ([x- e_packed-]) e-) : τ_e)])

7
macrotypes/examples/fomega2.rkt
View File

@ -73,11 +73,8 @@
(define old-typecheck? (current-typecheck-relation))
(define (new-typecheck? t1 t2)
(syntax-parse (list t1 t2) #:datum-literals (:)
[((~∀ ([tv1 : k1]) tbody1)
(~∀ ([tv2 : k2]) tbody2))
(and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))]
[_ (old-typecheck? t1 t2)]))
(and (kindcheck? (kindof t1) (kindof t2))
(old-typecheck? t1 t2)))
(current-typecheck-relation new-typecheck?)
;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind=

7
macrotypes/examples/fsub.rkt
View File

@ -75,14 +75,13 @@
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
(define-typed-syntax Λ #:datum-literals (<:)
[(_ ([tv:id <: τsub:type] ...) e)
[(_ ([X:id <: τsub:type] ...) e)
;; NOTE: store the subtyping relation of tv and τsub in another
;; "environment", ie, a syntax property with another tag: '<:
;; The "expose" function looks for this tag to enforce the bound,
;; as in TaPL (fig 28-1)
#:with ((tv- ...) _ (e-) (τ_e))
(infer #'(e) #:tvctx #'([tv :: #%type <: τsub] ...))
(⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))])
#:with ((X- ...) e- τ_e) (infer/ctx #'([X :: #%type <: τsub] ...) #'e)
(⊢ e- : (∀ ([X- <: τsub] ...) τ_e))])
(define-typed-syntax inst
[(_ e τ:type ...)
#:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)

7
macrotypes/examples/sysf.rkt
View File

@ -15,11 +15,10 @@
(define-typed-syntax Λ
[(_ (tv:id ...) e)
#:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv :: #%type] ...) #'e)
(⊢ e- : (∀ (tv- ...) τ))])
#:with [tvs- e- τ-] (infer/ctx #'(tv ...) #'e)
(⊢ e- : (∀ tvs- τ-))])
(define-typed-syntax inst
[(_ e τ:type ...)
#:with [e- (~∀ tvs τ_body)] (infer+erase #'e)
#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
(⊢ e- : τ_inst)]
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
[(_ e) #'e])

459
macrotypes/typecheck.rkt
View File

@ -202,6 +202,9 @@
;; e.g., Stx = expression, Tag = ':, Val = Type stx
(define (attach stx tag v)
(set-stx-prop/preserved stx tag v))
(define (attachs stx tags vs #:ev [ev (λ (x) x)])
(for/fold ([stx stx]) ([t (in-list tags)] [v (in-stx-list vs)])
(attach stx t (ev v))))
;; detach : Stx Tag -> Val
;; Retrieves Val at Tag stx prop on Stx.
;; If Val is a non-empty list, return first element, otherwise return Val.
@ -418,9 +421,8 @@
modes)]))))
;; base types --------------------------------------------------------
(define-syntax define-base-type
(syntax-parser
[(_ (~var τ id)) ; default to 'key2 and #%tag
#'(define-base-type τ key2 #%tag)]
(syntax-parser ; default = 'key2 + #%tag
[(_ (~var τ id)) #'(define-base-type τ key2 #%tag)]
[(_ (~var τ id) new-key2 new-#%tag)
#:with τ? (mk-? #'τ)
#:with τ-expander (mk-~ #'τ)
@ -470,8 +472,6 @@
;; - does not attach a kind to itself
(define-syntax define-internal-type-constructor
(syntax-parser
; [(_ (~var x id) . rst)
; #'(define-basic-checked-stx x key2 type #:no-attach-kind . rst)]))
[(_ (~var τ id)
(~or
(~optional ; variances
@ -486,7 +486,6 @@
(~seq #:extra-info extra-info)
#:name "#:extra-info keyword"
#:defaults ([extra-info #'void]))) (... ...))
; #:with #%kind (mk-#% #'kind)
#:with τ? (mk-? #'τ)
#:with τ- (mk-- #'τ)
#:with τ-expander (mk-~ #'τ)
@ -517,7 +516,7 @@
; τ- is an internal constructor:
; It does not validate inputs and does not attach a kind,
; ie, it won't be recognized as a valid type, the programmer
; must implement their own kind system
; must implement their own kind system on top
(define-syntax (τ- stx)
(syntax-parse stx
[(_ . args)
@ -535,10 +534,8 @@
#:with τ- (mk-- #'τ)
#'(begin
(define-internal-type-constructor τ . other-options)
; #'(define-basic-checked-stx x key2 type . rst)]))
(define-syntax (τ stx)
(syntax-parse stx
; [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
[(_ . args)
#:fail-unless (op (stx-length #'args) n)
(format
@ -577,12 +574,14 @@
#:with τ-expander (mk-~ #'τ)
#:with τ-internal (generate-temporary #'τ)
#`(begin
(begin-for-syntax ; -------------------------------------------
(begin-for-syntax
(define (τ? t)
(syntax-parse t
[(~Any/bvs (~literal τ-internal) _ . _)
#t]
[_ #f]))
;; cannot deal with annotations bc τ- has no knowledge of
;; its kind
(define-syntax τ-expander
(pattern-expander
(syntax-parser
@ -629,13 +628,12 @@
#'expanded-τ)
bvs-pat . pat))])))
(define arg-vars arg-variances-stx))
; end define-internal-binding-type begin-for-stx -------------
(define τ-internal
(λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use ~a at run time" 'τ 'name)
(current-continuation-marks)))))
; τ- is an internal constructor:
; Tt does not validate inputs and does not attach a kind,
; It does not validate inputs and does not attach a kind,
; ie, it won't be recognized as a valid type, the programmer
; must implement their own kind system
(define-syntax (τ- stx)
@ -663,13 +661,11 @@
(... ...)
. (~and other-options
(~not ((~or #:arity #:bvs #:arr) . _))))
; #'(define-binding-checked-stx x key2 type . rst)])))]))
#:with τ- (mk-- #'τ)
#`(begin
(define-internal-binding-type τ . other-options)
(define-syntax (τ stx)
(syntax-parse stx
; [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
[(_ (~and bvs
(~or (bv:id (... (... ...)))
(~and (~fail #:unless #,(attribute has-annotations?))
@ -713,6 +709,34 @@
;; pre-declare all type-related functions and forms
(define-syntax-category type)
;; TODO: move these into define-syntax-category?
(define-syntax typed-out
(make-provide-pre-transformer
(lambda (stx modes)
(syntax-parse stx #:datum-literals (:)
;; cannot write ty:type bc provides might precede type def
[(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
[[x:id (~optional :) ty] out-x:id])) ...)
#:with (x/tc ...) (generate-temporaries #'(x ...))
#:when (stx-map
syntax-local-lift-module-end-declaration
;; use define-primop to validate type
#'((define-primop x/tc x ty) ...))
(pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...))
modes)]))))
;; colon is optional to make it easier to use define-primop in macros
(define-syntax define-primop
(syntax-parser #:datum-literals (:)
[(define-primop op:id (~optional :) τ)
#:with op- (format-id #'op "~a-" #'op)
#'(define-primop op op- τ)]
[(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type)
; rename-transformer doesnt seem to expand at the right time
; - op still has no type in #%app
#'(define-syntax op/tc
(make-variable-like-transformer (assign-type #'op #'τ)))]))
;; generic, type-agnostic parameters
;; Use in code that is generic over types and kinds, e.g., in #lang Turnstile
(begin-for-syntax
@ -726,12 +750,14 @@
(define (check? x1 x2) ((current-check-relation) x1 x2))
(define (checks? xs1 xs2) ; map current-check-relation pairwise of lists
(and (stx-length=? xs1 xs2) (stx-andmap check? xs1 xs2)))
;; (define current-attach (make-parameter assign-type))
;; (define current-detach (make-parameter typeof))
(define current-ev (make-parameter (current-type-eval)))
(define current-tag (make-parameter (type-key1))))
;; type assignment utilities --------------------------------------------------
(define-syntax (let*-syntax stx)
(syntax-parse stx
[(_ () . body) #'(let-syntax () . body)]
[(_ (b . bs) . es) #'(let-syntax (b) (let*-syntax bs . es))]))
(begin-for-syntax
;; Type assignment macro (ie assign-type) for nicer syntax
(define-syntax (⊢ stx)
@ -743,41 +769,24 @@
[(_ e tag τ) #'(fast-assign-type #`e #`τ)]
[(_ e τ) #'(⊢/no-teval e : τ)]))
;; Actual type assignment function.
;; assign-type Type -> Syntax
;; Attaches type τ to (expanded) expression e.
;; - eval here so all types are stored in canonical form
;; - syntax-local-introduce fixes marks on types
;; which didnt get marked bc they were syntax properties
#;(define (fast-assign-type e τ #:tag [tag ':])
(set-stx-prop/preserved e tag (syntax-local-introduce τ)))
#;(define (assign-type e τ #:tag [tag ':])
(fast-assign-type e ((current-type-eval) τ) #:tag tag))
(define (add-expected-type e τ)
;; functions for manipulating "expected type"
(define (add-expected-type e τ)
(if (and (syntax? τ) (syntax-e τ))
(set-stx-prop/preserved e 'expected-type τ) ; dont type-eval?, ie expand?
e))
(define (get-expected-type e)
(get-stx-prop/cd*r e 'expected-type))
;; TODO: remove? only used by macrotypes/examples/infer.rkt
(define (add-env e env) (set-stx-prop/preserved e 'env env))
(define (get-env e) (syntax-property e 'env))
;; 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 ':])
(get-stx-prop/car stx tag))
;; get-stx-prop/car : Syntax Any -> Any
#;(define (get-stx-prop/car stx tag)
(define v (syntax-property stx tag))
(if (cons? v) (car v) v))
(define (mk-tyvar X) (attach X 'tyvar #t))
(define (tyvar? X) (syntax-property X 'tyvar))
(define type-pat "[A-Za-z]+")
;; TODO: remove this? only benefit is single control point for current-promote
;; - infers type of e
;; - checks that type of e matches the specified type
;; - erases types in e
@ -849,19 +858,39 @@
#'(τ_e (... ...)))
#'res])]))
;; --------------------------------------------------------------------------
;; "infer" function for expanding/computing type of an expression
;; matches arbitrary number of nexted (expanded) let-stxs
(define-syntax ~let*-syntax
(pattern-expander
(syntax-parser
[(_ . pat)
#:with the-stx (generate-temporary)
#'(~and the-stx
(~parse pat (let L ([stxs #'(the-stx)])
(syntax-parse stxs
[(((~literal let-values) ()
((~literal let-values) ()
. rst)))
(L #'rst)]
[es #'es]))))])))
;; basic infer function with no context:
;; infers the type and erases types in an expression
(define (infer+erase e #:tag [tag (current-tag)] #:expa [expa expand/df])
(define e+ (expa e))
(list e+ (detach e+ tag)))
;; infers the types and erases types in multiple expressions
(define (infers+erase es #:tag [tag (current-tag)])
(stx-map (λ (e) (infer+erase e #:tag tag)) es))
(define (infers+erase es #:tag [tag (current-tag)] #:expa [expa expand/df])
(stx-map (λ (e) (infer+erase e #:tag tag #:expa expa)) es))
;; This is the main "infer" function. All others are defined in terms of this.
;; This is the main "infer" function. Most others are defined in terms of this.
;; It should be named infer+erase but leaving it for now for backward compat.
;; ctx = vars and their types (or other props, denoted with "sep")
;; tvctx = tyvars and their kinds
;; ctx = vars and their types (or or any props, denoted with any "sep")
;; - each x in ctx is in scope for subsequent xs
;; - ie, dont need separate ctx and tvctx
;; - keep tvctx bc it's often useful to separate the returned Xs-
;; TODO: infer currently tries to be generic over types and kinds
;; but I'm not sure it properly generalizes
;; eg, what if I need separate type-eval and kind-eval fns?
@ -871,36 +900,32 @@
#:expa [expa expand/df] ; used to expand e
#:tev [tev #'(current-type-eval)] ; type-eval (τ in ctx)
#:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx)
(syntax-parse ctx
[([x sep τ] ...) ; dont expand yet bc τ may have references to tvs
#:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx
(syntax-parse ctx
[((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv
#:with (~or (~and (tv:id ...)
(~parse ([(tvsep ...) (tvk ...)] ...)
(stx-map (λ _ #'[(::) (#%type)]) #'(tv ...))))
([tv (~seq tvsep:id tvk) ...] ...))
tvctx
#:with (e ...) es
#:with
; old expander pattern (leave commented out)
#;((~literal #%plain-lambda) tvs+
((~literal #%expression)
((~literal #%plain-lambda) xs+
((~literal letrec-syntaxes+values) stxs1 ()
((~literal letrec-syntaxes+values) stxs2 ()
((~literal #%expression) e+) ...)))))
; new expander pattern
((~literal #%plain-lambda) tvs+
((~literal let-values) () ((~literal let-values) ()
((~literal #%expression)
((~literal #%plain-lambda) xs+
((~literal let-values) () ((~literal let-values) ()
((~literal #%expression) e+) ... (~literal void))))))))
(expa
#:with ((~literal #%plain-lambda) tvs+
(~let*-syntax
((~literal #%expression)
((~literal #%plain-lambda) xs+
(~let*-syntax
((~literal #%expression) e+) ... (~literal void))))))
(expa
#`(λ (tv ...)
(let-syntax ([tv (make-rename-transformer
(mk-tyvar
(for/fold ([tv-id #'tv])
([s (in-list '(tvsep ...))]
[k (in-stx-list #'(tvk ...))])
(attach tv-id s (#,kev k)))))] ...)
(λ (x ...)
(let-syntax ([x (make-variable-like-transformer
(attach #'x 'sep (#,tev #'τ)))] ...)
(let*-syntax ([tv (make-rename-transformer
(mk-tyvar
(attachs #'tv '(tvsep ...) #'(tvk ...)
#:ev #,kev)))] ...)
(λ (X ... x ...)
(let*-syntax ([X (make-variable-like-transformer
(mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ...
[x (make-variable-like-transformer
(attachs #'x '(sep ...) #'(τ ...)
#:ev #,tev))] ...)
(#%expression e) ... void)))))
(list #'tvs+ #'xs+
#'(e+ ...)
@ -925,6 +950,8 @@
(define (infers/tyctx+erase ctx es #:tag [tag (current-tag)])
(syntax-parse (infer es #:tvctx ctx #:tag tag)
[(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
(define infer/tyctx infer/tyctx+erase)
(define infer/ctx infer/ctx+erase)
(define current-promote (make-parameter (λ (t) t)))
@ -939,6 +966,7 @@
(define (expand/df e)
(local-expand e 'expression null))
;; TODO: move these into define-syntax-category?
;; typecheck-fail-msg/1 : Type Type Stx -> String
(define (typecheck-fail-msg/1 τ_expected τ_given expression)
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
@ -988,6 +1016,7 @@
(struct exn:fail:type:check exn:fail:user ())
(struct exn:fail:type:infer exn:fail:user ())
;; TODO: deprecate this? can we rely on stx-parse instead?
;; type-error #:src Syntax #:msg String Syntax ...
;; usage:
;; type-error #:src src-stx
@ -1091,292 +1120,6 @@
(define (get-type-tags ts)
(stx-map get-type-tag ts)))
#;(define-syntax define-basic-checked-id-stx
(syntax-parser #:datum-literals (:)
[(_ τ:id key tag)
#:with τ? (mk-? #'τ)
#:with τ-expander (mk-~ #'τ)
#:with τ-internal (generate-temporary #'τ)
#`(begin
(begin-for-syntax
(define (τ? t)
(syntax-parse t
[((~literal #%plain-app) (~literal τ-internal)) #t]
[_ #f]))
(define-syntax τ-expander
(pattern-expander
(syntax-parser
[:id #'((~literal #%plain-app) (~literal τ-internal))]
; - this case used by ⇑, TODO: remove this case?
; - but it's also needed when matching a list of types,
; e.g., in stlc+sub (~Nat τ)
[(_ . rst)
#'(((~literal #%plain-app) (~literal τ-internal)) . rst)]))))
(define τ-internal
(λ () (raise (exn:fail:type:runtime
(format "~a: Cannot use ~a at run time" 'τ 'tag)
(current-continuation-marks)))))
(define-syntax τ
(syntax-parser
[:id
(add-orig
(set-stx-prop/preserved
(syntax/loc this-syntax (τ-internal))
'key (expand/df #'tag))
#'τ)])))]))
;; The def uses pattern vars "τ" and "kind" but this form is not restricted to
;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type)
#;(define-syntax (define-basic-checked-stx stx)
(syntax-parse stx #:datum-literals (:)
[(_ τ:id key kind
(~or
(~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t)))
(~optional
(~seq #:arity op n:exact-nonnegative-integer)
#:defaults ([op #'=] [n #'1]))
(~optional (~seq #:arg-variances arg-variances-stx:expr)
#:defaults ([arg-variances-stx
#`(λ (stx-id)
(for/list ([arg (in-list (stx->list (stx-cdr stx-id)))])
invariant))]))
(~optional (~seq #:extra-info extra-info)
#:defaults ([extra-info #'void]))) ...)
#:with #%kind (mk-#% #'kind)
#:with τ? (mk-? #'τ)
#:with τ- (mk-- #'τ)
#:with τ-expander (mk-~ #'τ)
#:with τ-internal (generate-temporary #'τ)
#`(begin
(begin-for-syntax
(define-syntax τ-expander
(pattern-expander
(syntax-parser
[(_ . pat)
#:with expanded-τ (generate-temporary)
#'(~and expanded-τ
(~Any
(~literal/else τ-internal
(format "Expected ~a type, got: ~a"
'τ (type->str #'expanded-τ))
#'expanded-τ)
. pat))])))
(define arg-variances arg-variances-stx)
(define (τ? t)
(syntax-parse t
[(~Any (~literal τ-internal) . _) #t]
[_ #f])))
(define τ-internal
(λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use ~a at run time" 'τ 'kind)
(current-continuation-marks)))))
; τ- is an internal constructor:
; - it does not validate inputs and does not attach a kind,
; ie, it won't be recognized as a valid type unless a kind
; system is implemented on top
; - the τ constructor implements a default kind system but τ-
; is available if the programmer wants to implement their own
(define-syntax (τ- stx)
(syntax-parse stx
[(_ . args)
#:with τ-internal* (add-arg-variances #'τ-internal (arg-variances #'(τ . args)))
(syntax/loc stx
(τ-internal* (λ () (#%expression extra-info) . args)))]))
; this is the actual constructor
#,@(if (attribute no-attach-kind?)
#'()
#'((define-syntax (τ stx)
(syntax-parse stx
[(_ . args)
#:fail-unless (op (stx-length #'args) n)
(format "wrong number of arguments, expected ~a ~a"
'op 'n)
#:with ([arg- _] (... ...)) (infers+erase #'args)
;; the args are validated on the next line, rather than above
;; to ensure enough stx-parse progress so we get a proper err msg,
;; ie, "invalid type" instead of "improper tycon usage"
#:with (~! (~var _ kind) (... ...)) #'(arg- (... ...))
(add-orig
(set-stx-prop/preserved #'(τ- arg- (... ...)) 'key (expand/df #'#%kind))
stx)]
[_ ;; else fail with err msg
(type-error
#:src stx
#:msg
(string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
#'τ stx #'op #'n)])))))]))
;; Form for defining *binding* types, kinds, etc.
;; The def uses pattern vars "τ" and "kind" but this form is not restricted to
;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type)
#;(define-syntax (define-binding-checked-stx stx)
(syntax-parse stx
[(_ τ:id key kind
(~or
(~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t)))
(~optional
(~seq #:arity op n:exact-nonnegative-integer)
#:defaults ([op #'=] [n #'1]))
(~optional
(~seq #:bvs bvs-op bvs-n:exact-nonnegative-integer)
#:defaults ([bvs-op #'>=][bvs-n #'0]))
(~optional
(~seq #:arr (~and kindcon (~parse has-annotations? #'#t)))
#:defaults ([kindcon #'void])) ; default kindcon should never be used
(~optional
(~seq #:arg-variances arg-variances-stx:expr)
#:defaults ([arg-variances-stx
#`(λ (stx-id)
(for/list ([arg (in-list (stx->list (stx-cdr stx-id)))])
invariant))]))
(~optional
(~seq #:extra-info extra-info)
#:defaults ([extra-info #'void]))) ...)
#:with #%kind (mk-#% #'kind)
#:with τ? (mk-? #'τ)
#:with τ- (mk-- #'τ)
#:with τ-expander (mk-~ #'τ)
#:with τ-internal (generate-temporary #'τ)
#`(begin
(begin-for-syntax
(define-syntax τ-expander
(pattern-expander
(syntax-parser
; this case used by ⇑, TODO: remove this case?
;; if has-annotations?
;; - type has surface shape
;; (τ ([tv : k] ...) body ...)
;; - this case parses to pattern
;; [([tv k] ...) (body ...)]
;; if not has-annotations?
;; - type has surface shape
;; (τ (tv ...) body ...)
;; - this case parses to pattern
;; [(tv ...) (body ...)]
[(_ . pat:id)
#:with expanded-τ (generate-temporary)
#:with kindcon-expander (mk-~ #'kindcon)
#'(~and expanded-τ
(~Any/bvs
(~literal/else τ-internal
(format "Expected ~a type, got: ~a"
'τ (type->str #'expanded-τ))
#'expanded-τ)
(~and bvs (tv (... (... ...))))
. rst)
#,(if (attribute has-annotations?)
#'(~and
(~parse (kindcon-expander k (... (... ...)))
(tagoftype #'expanded-τ))
(~parse pat
#'[([tv k] (... (... ...))) rst]))
#'(~parse
pat
#'[bvs rst]))
)]
;; TODO: fix this to handle has-annotations?
;; the difference with the first case is that here
;; the body is ungrouped, ie,
;; parses to pattern[(tv ...) . (body ...)]
[(_ bvs-pat . pat)
#:with expanded-τ (generate-temporary)
#'(~and expanded-τ
(~Any/bvs
(~literal/else τ-internal
(format "Expected ~a type, got: ~a"
'τ (type->str #'expanded-τ))
#'expanded-τ)
bvs-pat
. pat))])))
(define arg-variances arg-variances-stx)
(define (τ? t)
(syntax-parse t
[(~Any/bvs (~literal τ-internal) _ . _)
#t]
[_ #f])))
(define τ-internal
(λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use ~a at run time" 'τ 'kind)
(current-continuation-marks)))))
; τ- is an internal constructor:
; - it does not validate inputs and does not attach a kind,
; ie, it won't be recognized as a valid type unless a kind
; system is implemented on top
; - the τ constructor implements a default kind system but τ-
; is available if the programmer wants to implement their own
(define-syntax (τ- stx)
(syntax-parse stx
[(_ bvs . args)
#:with τ-internal* (add-arg-variances
#'τ-internal
(arg-variances #'(τ- . args))) ; drop bvs
(syntax/loc stx
(τ-internal* (λ bvs (#%expression extra-info) . args)))]))
; this is the actual constructor
#,@(if (attribute no-attach-kind?)
#'()
#`((define-syntax (τ stx)
(syntax-parse stx
[(_ (~or (bv:id (... ...))
(~and (~fail #:unless #,(attribute has-annotations?))
bvs+ann))
. args)
#:with bvs+ks (if #,(attribute has-annotations?)
#'bvs+ann
#'([bv :: #%kind] (... ...)))
#:fail-unless (bvs-op (stx-length #'bvs+ks) 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 #'bvs+ks #'args)
;; the args are validated on the next line, rather than above
;; to ensure enough stx-parse progress so we get a proper err msg,
;; ie, "invalid type" instead of "improper tycon usage"
#:with (~! (~var _ kind) (... ...)) #'τs-
#:with ([tv (~datum ::) k_arg] (... ...)) #'bvs+ks
#:with k_result (if #,(attribute has-annotations?)
#'(kindcon k_arg (... ...))
#'#%kind)
(add-orig
(set-stx-prop/preserved #'(τ- bvs- . τs-) 'key (expand/df #'k_result))
stx)]
;; else fail with err msg
[_
(type-error #:src stx
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
#'τ stx #'op #'n)])))))]))
(define-syntax typed-out
(make-provide-pre-transformer
(lambda (stx modes)
(syntax-parse stx #:datum-literals (:)
;; cannot write ty:type bc provides might precede type def
[(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
[[x:id (~optional :) ty] out-x:id])) ...)
#:with (x/tc ...) (generate-temporaries #'(x ...))
#:when (stx-map
syntax-local-lift-module-end-declaration
;; use define-primop to validate type
#'((define-primop x/tc x ty) ...))
(pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...))
modes)]))))
;; colon is optional to make it easier to use define-primop in macros
(define-syntax define-primop
(syntax-parser #:datum-literals (:)
[(define-primop op:id (~optional :) τ)
#:with op- (format-id #'op "~a-" #'op)
#'(define-primop op op- τ)]
[(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type)
; rename-transformer doesnt seem to expand at the right time
; - op still has no type in #%app
#'(define-syntax op/tc
(make-variable-like-transformer (assign-type #'op #'τ)))]))
; substitution
(begin-for-syntax
(define-syntax ~Any/bvs ; matches any tycon
@ -1404,7 +1147,7 @@
(free-identifier=? #'actual #'lit))
fail-msg)
stx))])))
(define (merge-type-tags stx) ;; TODO: merge other tags
(define (merge-type-tags stx) ;; TODO: merge other tags?
(define t (syntax-property stx ':))
(or (and (pair? t)
(identifier? (car t)) (identifier? (cdr t))

3
turnstile/examples/exist.rkt
View File

@ -65,7 +65,6 @@
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
;;
[⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)]
#:with τ_x (subst #'X #'Y #'τ_body)
[([X ≫ X- :: #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
[X [x ≫ x- : #,(subst #'X #'Y #'τ_body)] ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])

2
turnstile/examples/fomega-no-reuse.rkt
View File

@ -169,7 +169,7 @@
[_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
(define-typed-syntax (Λ bvs:kind-ctx e) ≫
[([bvs.x ≫ tv- :: bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
[[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)])

2
turnstile/examples/fomega3.rkt
View File

@ -1,6 +1,8 @@
#lang turnstile/lang
(extends "fomega.rkt" #:except tyapp tyλ)
;; not current working 2017-02-03
; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
; → is both type and kind --- but reuses parts of fomega.rkt,
; ie removes the duplication in fomega2.rkt

2
turnstile/examples/fsub.rkt
View File

@ -79,7 +79,7 @@
;; environment with a syntax property using another tag: '<:
;; The "expose" function looks for this tag to enforce the bound,
;; as in TaPL (fig 28-1)
[([tv ≫ tv- :: #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e]
[[tv ≫ tv- :: #%type <: τsub] ... ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)])
(define-typed-syntax (inst e τ:type ...) ≫

2
turnstile/examples/mlish+adhoc.rkt
View File

@ -1713,7 +1713,7 @@
(~=> TCsub ...
(~TC [generic-op-expected ty-concrete-op-expected] ...)))
_)
(infers/tyctx+erase #'([X :: #%type] ...) #'(TC ... (Name ty ...)))
(infers/tyctx+erase #'(X ...) #'(TC ... (Name ty ...)))
;; this produces #%app bad stx err, so manually call infer for now
;; [([X ≫ X- :: #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫
;; (TC+ ...

7
turnstile/examples/mlish.rkt
View File

@ -850,16 +850,15 @@
#:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
(format "expected a function of ~a arguments, got one with ~a arguments"
(stx-length #'[τ_in ...]) (stx-length #'[x ...]))
[([X ≫ X- :: #%type] ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]]
[(X ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]]
--------
[⊢ (λ- (x- ...) body-)]]
[(λ ([x : τ_x] ...) body) ⇐ (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
#:with [X ...] (compute-tyvars #'(τ_x ...))
[([X ≫ X- :: #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...]
[[X ≫ X- :: #%type] ... ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...]
[τ_in τ⊑ τ_x- #:for x] ...
;; TODO is there a way to have λs that refer to ids defined after them?
[([V ≫ V- :: #%type] ... [X- ≫ X-- :: #%type] ...) ([x ≫ x- : τ_x-] ...)
⊢ body ≫ body- ⇐ τ_out]
[(V ... X- ...) ([x ≫ x- : τ_x-] ...) ⊢ body ≫ body- ⇐ τ_out]
--------
[⊢ (λ- (x- ...) body-)]]
[(λ ([x : τ_x] ...) body) ≫

3
turnstile/examples/stlc+rec-iso.rkt
View File

@ -23,7 +23,6 @@
[⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)])
(define-typed-syntax (fld τ:type-ann e) ≫
#:with (~μ (tv) τ_body) #'τ.norm
#:with τ_e (subst #'τ.norm #'tv #'τ_body)
[⊢ e ≫ e- ⇐ τ_e]
[⊢ e ≫ e- ⇐ #,(subst #'τ.norm #'tv #'τ_body)]
--------
[⊢ e- ⇒ τ.norm])

9
turnstile/examples/sysf.rkt
View File

@ -14,17 +14,14 @@
(define-binding-type ∀)
(define-typed-syntax (Λ (tv:id ...) e) ≫
[([tv ≫ tv- :: #%type] ...) () ⊢ e ≫ e- ⇒ τ]
[[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ]
--------
[⊢ e- ⇒ (∀ (tv- ...) τ)])
(define-typed-syntax inst
[(_ e τ:type ...) ≫
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
--------
[⊢ e- ⇒ τ_inst]]
[(_ e) ≫
--------
[≻ e]])
[⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
[(_ e) ≫ --- [≻ e]])

36
turnstile/scribblings/reference.scrbl
View File

@ -34,7 +34,7 @@ and then press Control-@litchar{\}.
@; define-typed-syntax---------------------------------------------------------
@defform*[
#:literals (≫ ⊢ ⇒ ⇐ ≻ : --------)
#:literals (≫ ⊢ ⇒ ⇐ ≻ --------)
((define-typed-syntax (name-id . pattern) ≫
premise ...
--------
@ -50,7 +50,7 @@ and then press Control-@litchar{\}.
premise ...
--------
⇐-conclusion]
[expr-pattern ⇐ key type-pattern ≫
[expr-pattern ⇐ key pattern ≫
premise ...
--------
⇐-conclusion]]
@ -70,21 +70,22 @@ and then press Control-@litchar{\}.
type-relation
(code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
[ctx (ctx-elem ...)]
[ctx-elem (code:line [id ≫ id : type-template] ooo ...)]
[ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)
(code:line id ooo ...)]
[tc (code:line tc-elem ooo ...)]
[tc-elem [expr-template ≫ expr-pattern ⇒ type-pattern]
[expr-template ≫ expr-pattern ⇒ key type-pattern]
[expr-template ≫ expr-pattern (⇒ key type-pattern) ooo ...]
[expr-template ≫ expr-pattern ⇒ key pattern]
[expr-template ≫ expr-pattern (⇒ key pattern) ooo ...]
[expr-template ≫ expr-pattern ⇐ type-template]
[expr-template ≫ expr-pattern ⇐ key type-template]
[expr-template ≫ expr-pattern (⇐ key type-template) ooo ...]]
[expr-template ≫ expr-pattern ⇐ key template]
[expr-template ≫ expr-pattern (⇐ key template) ooo ...]]
[type-relation (code:line [type-template τ= type-template] ooo ...)
(code:line [type-template τ= type-template #:for expr-template] ooo ...)
(code:line [type-template τ⊑ type-template] ooo ...)
(code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)]
[conclusion [⊢ expr-template ⇒ type-template]
[⊢ expr-template ⇒ key type-template]
[⊢ expr-template (⇒ key type-template) ooo ...]
[⊢ expr-template ⇒ key template]
[⊢ expr-template (⇒ key template) ooo ...]
[≻ expr-template]
[#:error expr-template]]
[⇐-conclusion [⊢ expr-template]]
@ -104,8 +105,8 @@ declares that expression @racket[e] expands to @racket[e-] and has type
outputs. Syntactically, @racket[e] is a syntax template position and
@racket[e-] @racket[τ] are syntax pattern positions.
A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key τ) ...]] to
specify propagation of arbitrary values, associated with any number of
A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key pat) ...]]
to specify propagation of arbitrary values, associated with any number of
keys. For example, a type and effect system may wish to additionally propagate
source locations of allocations and mutations. When no key is specified,
@litchar{:}, i.e., the "type" key, is used. Dually, one may write @racket[[⊢ e
@ -113,6 +114,19 @@ source locations of allocations and mutations. When no key is specified,
and @racket[τ] are inputs (templates) and only @racket[e-] is an
output (pattern).
A context may be specified to the left of the turnstile. A context element has
shape @racket[[⊢ x ≫ x- key pat ... ...]] where @racket[x-] is the expansion of
@racket[x] and the @racket[(key pat) ...] are arbitrary key-value pairs, e.g. a
@litchar{:} key and type pattern. Elements in the context have @racket[let*]
semantics where each binding is in scope for subsequent parts of the
context. This means type and term variables may be in the same context (though
order matters). Nevertheless, Turnstile allows writing two separate contexts,
where bindings in first are in scope for the second. This is often convenient
for separating the context bindings and using their outputs in different forms.
For convenience, lone identifiers written to the left of the turnstile are
automatically treated as type variables.
The @racket[≻] conclusion form is useful in many scenarios where the rule being
implemented may not want to attach type information. E.g.,

14
turnstile/turnstile.rkt
View File

@ -32,7 +32,7 @@
(define origs (lens-view flat origs*))
(define/with-syntax [tvxs- xs- es- _]
(infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag))
(define es*- (lens-set flat es* #'es-))
(define es*- (lens-set flat es* #`es-))
(list #'tvxs- #'xs- es*-))
;; infers/depths
(define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*
@ -156,6 +156,12 @@
(define-splicing-syntax-class id+props+≫
#:datum-literals (≫)
#:attributes ([x- 1] [ctx 1])
[pattern (~seq (~and X:id (~not _:elipsis)))
#:with [x- ...] #'[_]
#:with [ctx ...] #'[[X :: #%type]]]
[pattern (~seq X:id ooo:elipsis)
#:with [x- ...] #'[_ ooo]
#:with [ctx ...] #'[[X :: #%type] ooo]]
[pattern (~seq [x:id ≫ x--:id props:props])
#:with [x- ...] #'[x--]
#:with [ctx ...] #'[[x props.stuff ...]]]
@ -229,19 +235,19 @@
#'[ooo ...])
#:with tvctxs/ctxs/ess/origs
(with-depth
#'[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
#`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
#'[ooo ...])
#:with pat
#`(~post
(~post
(~parse
tcs-pat
(infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs
(infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs
#:tag (current-tag)))))]
)
(define-splicing-syntax-class clause
#:attributes (pat)
#:datum-literals (τ⊑ τ=) ; TODO: drop the τ
#:datum-literals (τ⊑ τ=) ; TODO: drop the τ in τ⊑ and τ=
[pattern :tc-clause]
[pattern [a τ⊑ b]
#:with pat