reference.scrbl (34478B)
1 #lang scribble/manual 2 3 @(require scribble/example racket/sandbox 4 (for-label racket/base 5 turnstile/mode 6 (except-in turnstile/turnstile ⊢ stx mk-~ mk-?)) 7 "doc-utils.rkt" "common.rkt") 8 9 @title{The Turnstile Reference} 10 11 @section{Typing Unicode Characters} 12 13 @(define the-eval 14 (parameterize ([sandbox-output 'string] 15 [sandbox-error-output 'string] 16 [sandbox-eval-limits #f]) 17 (make-base-eval #:lang 'turnstile))) 18 19 @; insert link? 20 @; https://docs.racket-lang.org/drracket/Keyboard_Shortcuts.html 21 Turnstile utilizes unicode. Here are DrRacket keyboard shortcuts for the 22 relevant characters. Type (any unique prefix of) the following 23 and then press Control-@litchar{\}. 24 25 @itemlist[ 26 @item{@litchar{\vdash} → @litchar{⊢}} 27 @item{@litchar{\gg} → @litchar{≫}} 28 @item{@litchar{\rightarrow} → @litchar{→}} 29 @item{@litchar{\Rightarrow} → @litchar{⇒}} 30 @item{@litchar{\Leftarrow} → @litchar{⇐}} 31 @item{@litchar{\succ} → @litchar{≻}} 32 ] 33 34 @section{Forms} 35 36 @; define-typed-syntax--------------------------------------------------------- 37 @defform*[ 38 #:literals (≫ ⊢ ⇒ ⇐ ≻ --------) 39 ((define-typed-syntax (name-id . pattern) ≫ 40 premise ... 41 -------- 42 conclusion) 43 (define-typed-syntax name-id option ... rule ...+)) 44 #:grammar 45 ([option (code:line @#,racket[syntax-parse] option)] 46 [rule [expr-pattern ≫ 47 premise ... 48 -------- 49 conclusion] 50 [expr-pattern ⇐ type-pattern ≫ 51 premise ... 52 -------- 53 ⇐-conclusion] 54 [expr-pattern ⇐ key pattern ≫ 55 premise ... 56 -------- 57 ⇐-conclusion]] 58 [expr-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)] 59 [type-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)] 60 [expr-template (code:line @#,racket[quasisyntax] @#,tech:template)] 61 [type-template (code:line @#,racket[quasisyntax] @#,tech:template)] 62 [key identifier?] 63 [premise (code:line [⊢ tc ... prem-options] ooo ...) 64 (code:line [ctx-elem ... ⊢ tc ... prem-options] ooo ...) 65 (code:line [ctx ⊢ tc ... prem-options] ooo ...) 66 (code:line [ctx ctx ⊢ tc ... prem-options] ooo ...) 67 (code:line [⊢ . tc-elem] ooo ...) 68 (code:line [ctx-elem ... ⊢ . tc-elem] ooo ...) 69 (code:line [ctx ⊢ . tc-elem] ooo ...) 70 (code:line [ctx ctx ⊢ . tc-elem] ooo ...) 71 type-relation 72 (code:line #:mode mode-expr (premise ...)) 73 (code:line #:submode fn-expr (premise ...)) 74 (code:line @#,racket[syntax-parse] @#,tech:pat-directive)] 75 [ctx (ctx-elem ...)] 76 [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...) 77 (code:line id ooo ...)] 78 [tc (code:line tc-elem ooo ...)] 79 [tc-elem [expr-template ≫ expr-pattern ⇒ type-pattern] 80 [expr-template ≫ expr-pattern ⇒ key pattern] 81 [expr-template ≫ expr-pattern (⇒ key pattern) ooo ...] 82 [expr-template ≫ expr-pattern ⇐ type-template] 83 [expr-template ≫ expr-pattern ⇐ key template] 84 [expr-template ≫ expr-pattern (⇐ key template) ooo ...]] 85 [type-relation (code:line [type-template τ= type-template] ooo ...) 86 (code:line [type-template τ= type-template #:for expr-template] ooo ...) 87 (code:line [type-template τ⊑ type-template] ooo ...) 88 (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)] 89 [prem-options (code:line) 90 (code:line #:mode mode-expr) 91 (code:line #:submode fn-expr)] 92 [conclusion [⊢ expr-template ⇒ type-template] 93 [⊢ expr-template ⇒ key template] 94 [⊢ expr-template (⇒ key template) ooo ...] 95 [≻ expr-template] 96 [#:error expr-template]] 97 [⇐-conclusion [⊢ expr-template]] 98 [ooo ...]) 99 ]{ 100 101 Generates a macro definition that also performs type checking. The macro is 102 generated from @racket[syntax-parse] @tech:stx-pats and @tech:pat-directives, 103 along with type-judgement-like clauses that interleave typechecking and macro 104 expansion. The resulting macro type checks its surface syntax as part of macro 105 expansion and the resulting type is attached to the expanded expression. 106 107 @; ---------------------------------------------------------------------------- 108 @bold{Premises} 109 110 @italic{Bidirectional judgements} 111 112 Turnstile @racket[define-typed-syntax] rules use bidirectional type checking 113 judgements: 114 @itemlist[ 115 @item{@racket[[⊢ e ≫ e- ⇒ τ]] declares that expression @racket[e] expands to 116 @racket[e-] and has type @racket[τ], where @racket[e] is the input and, 117 @racket[e-] and @racket[τ] outputs. Syntactically, @racket[e] is a syntax 118 template position and @racket[e-] and @racket[τ] are syntax pattern positions.} 119 120 @item{Dually, one may write @racket[[⊢ e 121 ≫ e- ⇐ τ]] to check that @racket[e] has type @racket[τ]. Here, both @racket[e] 122 and @racket[τ] are inputs (templates) and only @racket[e-] is an 123 output (pattern).}] 124 125 Each bidirectional arrow has a generalized form that associates a key with a 126 value, e.g., @racket[[⊢ e ≫ e- (⇒ key pat) ...]]. A programmer may use this 127 generalized form to specify propagation of arbitrary values, associated with 128 any number of keys. For example, a type and effect system may wish to 129 additionally propagate source locations of allocations and mutations. When no 130 key is specified, @litchar{:}, i.e., the "type" key, is used. 131 132 @italic{Contexts} 133 134 A context may be specified to the left of the turnstile. A context element has 135 shape @racket[[⊢ x ≫ x- key pat ... ...]] where @racket[x-] is a pattern 136 matching the expansion of @racket[x] and the interleaved @racket[key ...] and 137 @racket[pat ...] are arbitrary key-value pairs, e.g. a @litchar{:} key and type 138 pattern. 139 140 A context has @racket[let*] semantics where each binding is in scope for 141 subsequent parts of the context. This means type and term variables may be in 142 the same context (if properly ordered). In addition, Turnstile allows writing 143 two separate contexts, grouped by parens, where bindings in first are in scope 144 for the second. This is often convenient for scenarios that Racket's pattern 145 language cannot express, e.g., when there two distinct groups of bindings, a 146 pattern @racket[x ... y ...] will not work as expected. 147 148 For convenience, lone identifiers written to the left of the turnstile are 149 automatically treated as type variables. 150 151 @italic{Modes} 152 153 The keyword @racket[#:mode], when appearing at end of a typechecking rule, 154 sets the parameter @racket[current-mode] to the @racket[mode] object supplied 155 by @racket[_mode-expr], for the extent of that rule. @racket[#:mode], when 156 appearing as its own premise, sets the @racket[current-mode] parameter for the 157 extent of all the grouped sub-premises. 158 159 The keyword @racket[#:submode] is similar to @racket[#:mode], but it calls 160 @racket[(_fn-expr (current-mode))] to obtain the new mode object. Thus, 161 @racket[#:mode (_fn-expr (current-mode))] is identical to @racket[#:submode 162 _fn-expr]. 163 164 See @secref{Modes} for more details. 165 166 WARNING: @racket[#:mode] is unaware of the backtracking behavior of 167 @racket[syntax-parse]. If pattern backtracking escapes a @racket[#:mode] group, it may 168 leave @racket[current-mode] in an undesirable state. 169 170 171 @; ---------------------------------------------------------------------------- 172 @bold{Conclusion} 173 174 Bidirectional judgements below the conclusion line invert their inputs and 175 outputs so that both positions in @racket[[⊢ e- ⇒ τ]] are syntax templates and 176 means that @racket[e-] is the output of the generated macro and it has type τ 177 attached. The generalized key-value form of the bidirectional judgements may 178 also be used in the conclusion. 179 180 The @racket[≻] conclusion form is useful in many scenarios where the rule being 181 implemented may not want to attach type information. E.g., 182 183 @itemlist[#:style 'ordered 184 185 @item{when a rule's output is another typed macro. 186 187 For example, here is a hypothetical @tt{typed-let*} that is implemented in 188 terms of a @tt{typed-let}: 189 190 @racketblock0[ 191 (define-typed-syntax typed-let* 192 [(_ () e_body) ≫ 193 -------- 194 [≻ e_body]] 195 [(_ ([x e] [x_rst e_rst] ...) e_body) ≫ 196 -------- 197 [≻ (typed-let ([x e]) (typed-let* ([x_rst e_rst] ...) e_body))]])] 198 199 The conclusion in the first clause utilizes @racket[≻] since the body already 200 carries its own type. The second clause uses @racket[≻] because it defers to 201 @tt{typed-let}, which will attach type information.} 202 203 @item{when a rule extends another. 204 205 This is related to the first example. For example, here is a @racket[#%datum] 206 that extends another with more typed literals (see also @secref{stlcsub}). 207 208 @racketblock0[ 209 210 (define-typed-syntax typed-datum 211 [(_ . n:integer) ≫ 212 -------- 213 [⊢ (#%datum- . n) ⇒ Int]] 214 [(_ . x) ≫ 215 -------- 216 [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) 217 218 (define-typed-syntax extended-datum 219 [(_ . s:str) ≫ 220 -------- 221 [⊢ (#%datum- . s) ⇒ String]] 222 [(_ . x) ≫ 223 -------- 224 [≻ (typed-datum . x)]])]} 225 226 @item{for top-level forms. 227 228 For example, here is a basic typed version of @racket[define]: 229 230 @racketblock0[ 231 232 (define-typed-syntax define 233 [(_ x:id e) ≫ 234 [⊢ e ≫ e- ⇒ τ] 235 #:with y (generate-temporary #'x) 236 -------- 237 [≻ (begin- 238 (define-syntax x (make-rename-transformer (⊢ y : τ))) 239 (define- y e-))]])] 240 241 This macro creates an indirection @racket[make-rename-transformer] in order to 242 attach type information to the top-level @tt{x} identifier, so the 243 @racket[define] forms themselves do not need type information.} 244 245 ]} 246 247 @; ---------------------------------------------------------------------------- 248 @bold{Note} 249 250 @racket[define-typed-syntax] is generated by 251 @racket[define-syntax-category]. See @racket[define-syntax-category] for more 252 information. 253 254 @defform[(define-typerule ....)]{Alias for @racket[define-typed-syntax].} 255 @defform[(define-syntax/typecheck ....)]{Alias for @racket[define-typed-syntax].} 256 257 @; syntax-parse/typecheck------------------------------------------------------ 258 @defform[(syntax-parse/typecheck stx option ... rule ...+)]{ 259 A @racket[syntax-parse]-like form that supports 260 @racket[define-typed-syntax]-style clauses. In particular, see the 261 "rule" part of @racket[define-typed-syntax]'s grammar above.} 262 263 @; ~typecheck and ~⊢ 264 265 @defform[(~typecheck premise ...)]{ 266 A @racket[syntax-parse] @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander} 267 that supports typechecking syntax. 268 269 For example the pattern 270 271 @racketblock[ 272 (~typecheck 273 [⊢ a ≫ a- ⇒ τ_a] 274 [⊢ b ≫ b- ⇐ τ_a])] 275 276 typechecks @racket[a] and @racket[b], expecting @racket[b] to have the 277 type of @racket[a], and binding @racket[a-] and @racket[b-] to the 278 expanded versions. 279 280 This is most useful in places where you want to do typechecking in 281 something other than a type rule, like in a function or a syntax 282 class. 283 284 @(let ([ev (make-base-eval)]) 285 (ev '(require turnstile/turnstile)) 286 @examples[ 287 #:eval ev 288 (begin-for-syntax 289 (struct clause [stx- result-type]) 290 (code:comment "f : Stx -> Clause") 291 (define (f stx) 292 (syntax-parse stx 293 [(~and [condition:expr body:expr] 294 (~typecheck 295 [⊢ condition ≫ condition- ⇐ Bool] 296 [⊢ body ≫ body- ⇒ τ_body])) 297 (clause #'[condition- body-] #'τ_body)]))) 298 ])} 299 300 @defform*[[(~⊢ tc ...)]]{ 301 A shorthand @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander} 302 for @racket[(~typcheck [⊢ tc ...])]. 303 304 For example the pattern @racket[(~⊢ a ≫ a- ⇒ τ_a)] typechecks 305 @racket[a], binding the expanded version to @racket[a-] and the type 306 to @racket[τ_a]. 307 308 @(let ([ev (make-base-eval)]) 309 (ev '(require turnstile/turnstile)) 310 @examples[ 311 #:eval ev 312 (begin-for-syntax 313 (struct clause [stx- result-type]) 314 (code:comment "f : Stx -> Clause") 315 (define (f stx) 316 (syntax-parse stx 317 [(~and [condition:expr body:expr] 318 (~⊢ condition ≫ condition- ⇐ Bool) 319 (~⊢ body ≫ body- ⇒ τ_body)) 320 (clause #'[condition- body-] #'τ_body)]))) 321 ])} 322 323 @; define-primop -------------------------------------------------------------- 324 @defform*[((define-primop typed-op-id τ) 325 (define-primop typed-op-id : τ) 326 (define-primop typed-op-id op-id τ) 327 (define-primop typed-op-id op-id : τ) 328 (define-primop typed-op-id #:as op-id τ) 329 (define-primop typed-op-id #:as op-id : τ))]{ 330 Defines @racket[typed-op-id] by attaching type @racket[τ] to (untyped) 331 identifier @racket[op-id], e.g.: 332 333 @racketblock[(define-primop typed+ + : (→ Int Int))] 334 335 When not specified, @racket[op-id] is @racket[typed-op-id] suffixed with 336 @litchar{-} (see @secref{racket-}).} 337 338 @; define-syntax-category ----------------------------------------------------- 339 @defform*[((define-syntax-category name-id) 340 (define-syntax-category key1 name-id) 341 (define-syntax-category key1 name-id key2))]{ 342 343 Defines a new "category" of syntax by defining a series of forms and functions. 344 Turnstile pre-declares @racket[(define-syntax-category type)], which in turn 345 defines the forms and functions below. 346 347 Each category of syntax is associated with two keys: @racket[key1] is used when 348 attaching values in the category to other syntax, e.g., attaching types to 349 terms, and @racket[key2] is used for attaching an additional syntax property to 350 values in the category, e.g. using @racket[#%type] to indicate well-formedness. 351 352 If no keys are specified, @racket[key1] is @litchar{:} and @racket[key2] is 353 @litchar{::}. If only @racket[key1] is given, then @racket[key2] is 354 @racket[key1] appended to itself. 355 356 Defining another category, e.g., @racket[(define-syntax-category kind)], 357 defines a separate set of forms and functions, e.g., 358 @racket[define-kinded-syntax], @racket[define-base-kind], @racket[kind=?], etc. 359 360 @; ---------------------------------------------------------------------------- 361 @italic{The following forms and functions are automatically defined by a 362 @racket[(define-syntax-category type)] declaration:} 363 364 @margin-note{It's not important to immediately understand all these 365 definitions. Some, like @racket[type?] and @racket[mk-type], are 366 more "low-level" and are mainly used by the other forms. The most useful forms 367 are probably @racket[define-typed-syntax], and the type-defining forms 368 @racket[define-base-type], @racket[define-type-constructor], and 369 @racket[define-binding-type].} 370 371 @itemlist[ 372 373 @item{@racket[define-typed-syntax], as described above. Uses 374 @racket[current-typecheck-relation] @racket[current-type-eval] for 375 typechecking, and uses @litchar{:} as the key when an explicit key is not specificed in type judgements.} 376 377 @item{@defform*[((define-base-type base-type-name-id) 378 (define-base-type base-type-name-id key tag))]{ 379 Defines a base type. @racket[(define-base-type τ)] in turn defines: 380 @itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].} 381 @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].} 382 @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]} 383 384 Types defined with @racket[define-base-type] are automatically tagged with a 385 @racket[key2]-keyed (as specified in the @racket[define-syntax-category] 386 declaration) @racket[#%type] syntax property, unless second form above is used, 387 in which case the specified @tt{tag} is attached to the type using the 388 specified @tt{key}.} 389 390 @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types, each using the default key.}} 391 392 @item{ 393 @defform[(define-type-constructor name-id option ...) 394 #:grammar 395 ([option (code:line #:arity op n) 396 (code:line #:arg-variances expr) 397 (code:line #:extra-info stx)])]{ 398 Defines a type constructor (that does not bind type variables). 399 Defining a type constructor @racket[τ] subsequently defines: 400 @itemlist[ 401 402 @item{@racket[τ], a macro for constructing an instance of type @racket[τ], 403 with the specified arity. Validates inputs and expands to 404 @racket[τ-], attaching @racket[#%type] at @tt{key2}.} 405 406 @item{@racket[τ-], an internal macro that expands to the internal 407 (i.e., fully expanded) type representation. Does not validate inputs 408 or attach any extra properties. This macro is useful when creating a 409 separate kind system, see @racket[define-internal-type-constructor].} 410 411 @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].} 412 @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type 413 @racket[τ].}] 414 415 The @racket[#:arity] argument specifies the valid shapes 416 for the type. For example 417 @racket[(define-type-constructor → #:arity >= 1)] defines an arrow type and 418 @racket[(define-type-constructor Pair #:arity = 2)] defines a pair type. 419 The default arity is @racket[= 1]. 420 421 The @racket[#:arg-variances] argument is a transformer converting a syntax 422 object of the type to a list of variances for the arguments to the type 423 constructor. 424 425 The possible variances are @racket[invariant], @racket[contravariant], 426 @racket[covariant], and @racket[irrelevant]. 427 428 If @racket[#:arg-variances] is not specified, @racket[invariant] is used for 429 all positions. 430 431 Example: 432 433 @racketblock0[(define-type-constructor → #:arity >= 1 434 #:arg-variances 435 (λ (stx) 436 (syntax-parse stx 437 [(_ τ_in ... τ_out) 438 (append 439 (make-list (stx-length #'[τ_in ...]) contravariant) 440 (list covariant))])))] 441 442 The @racket[#:extra-info] argument is useful for attaching additional 443 metainformation to types, for example to communicate accessors to a pattern 444 matching form.}} 445 @item{ 446 @defform[(define-internal-type-constructor name-id option ...) 447 #:grammar 448 ([option (code:line #:arg-variances expr) 449 (code:line #:extra-info stx)])]{ 450 451 Like @racket[define-type-constructor], except the surface macro is not 452 defined. Use this form, for example, when creating a separate kind system so 453 that you can still use other Turnstile conveniences like pattern expanders.}} 454 455 @item{ 456 @defform[(define-binding-type name-id option ...) 457 #:grammar 458 ([option (code:line #:arity op n) 459 (code:line #:bvs op n) 460 (code:line #:arr kindcon) 461 (code:line #:arg-variances expr) 462 (code:line #:extra-info stx)])]{ 463 Similar to @racket[define-type-constructor], except 464 @racket[define-binding-type] defines a type that binds type variables. 465 Defining a type constructor @racket[τ] defines: 466 467 The @racket[#:arity] and @racket[#:bvs] arguments specify the valid shapes 468 for the type. For example 469 @racket[(define-binding-type ∀ #:arity = 1 #:bvs = 1)] defines a type 470 with shape @racket[(∀ (X) τ)], where @racket[τ] may reference @racket[X]. 471 472 The default @racket[#:arity] is @racket[= 1] 473 and the default @racket[#:bvs] is @racket[>= 0]. 474 475 Use the @racket[#:arr] argument to define a type with kind annotations 476 on the type variables. The @racket[#:arr] argument is an "arrow" that "saves" 477 the annotations after a type is expanded and annotations are erased, 478 analogous to how → "saves" the type annotations on a lambda.}} 479 @item{ 480 @defform[(define-internal-binding-type name-id option ...) 481 #:grammar 482 ([option (code:line #:arr kindcon) 483 (code:line #:arg-variances expr) 484 (code:line #:extra-info stx)])]{ 485 Analogous to @racket[define-internal-type-constructor], but for binding types.}} 486 @item{ 487 @defform[(type-out ty-id ...)]{ 488 A @racket[provide]-spec that, for each given @racket[ty-id], provides @racket[ty-id], 489 and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-expander @racket[~ty-id].}} 490 491 @item{@defparam[current-type-eval type-eval type-eval]{ 492 A phase 1 parameter for controlling "type evaluation". A @racket[type-eval] 493 function consumes and produces syntax. It is typically used to convert a type 494 into a canonical representation. The @racket[(current-type-eval)] is called 495 immediately before attaching a type to a syntax object, i.e., by 496 @racket[assign-type]. 497 498 It defaults to full expansion, i.e., @racket[(lambda (stx) (local-expand stx 'expression null))], and also stores extra surface syntax information used for error reporting. 499 500 One should extend @racket[current-type-eval] if canonicalization of types 501 depends on combinations of different types, e.g., type lambdas and type application in F-omega. }} 502 503 @; current-typecheck-relation ------------------------------------------------- 504 @item{@defparam[current-typecheck-relation type-pred type-pred]{ 505 506 A phase 1 parameter for controlling type checking, used by 507 @racket[define-typed-syntax]. A @racket[type-pred] function consumes two 508 types---the first is the given type and the second is the expected type---and 509 returns true if they "type check". It defaults to @racket[type=?] though it 510 does not have to be a symmetric relation. Useful for reusing rules that differ 511 only in the type check operation, e.g., equality vs subtyping.}} 512 513 @item{@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{ 514 A phase 1 function that calls @racket[current-typecheck-relation]. The first 515 argument is the given type and the second is the expected type.}} 516 517 @item{@defproc[(typechecks? [τs1 (or/c (list/c type?) (stx-list/c type?))] 518 [τs2 (or/c (list/c type?) (stx-list/c type?))]) boolean?]{ 519 Phase 1 function mapping @racket[typecheck?] over lists of types, 520 pairwise. @racket[τs1] and @racket[τs2] must have the same length. The first 521 list contains the given types and the second list contains the expected 522 types.}} 523 524 @item{@defproc[(type=? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 equality 525 predicate for types that computes structural, @racket[free-identifier=?] 526 equality, but includes alpha-equivalence. 527 528 @examples[#:eval the-eval 529 (define-base-type Int) 530 (define-base-type String) 531 (begin-for-syntax (displayln (type=? #'Int #'Int))) 532 (begin-for-syntax (displayln (type=? #'Int #'String))) 533 (define-type-constructor → #:arity > 0) 534 (define-binding-type ∀ #:arity = 1 #:bvs = 1) 535 (begin-for-syntax 536 (displayln 537 (type=? ((current-type-eval) #'(∀ (X) X)) 538 ((current-type-eval) #'(∀ (Y) Y))))) 539 (begin-for-syntax 540 (displayln 541 (type=? ((current-type-eval) #'(∀ (X) (∀ (Y) (→ X Y)))) 542 ((current-type-eval) #'(∀ (Y) (∀ (X) (→ Y X))))))) 543 (begin-for-syntax 544 (displayln 545 (type=? ((current-type-eval) #'(∀ (Y) (∀ (X) (→ Y X)))) 546 ((current-type-eval) #'(∀ (X) (∀ (X) (→ X X))))))) 547 ] 548 }} 549 550 @item{@defproc[(types=? [τs1 (listof type?)][τs2 (listof type?)]) boolean?]{ 551 A phase 1 predicate checking that @racket[τs1] and @racket[τs2] are equivalent, pairwise. Thus, 552 @racket[τs1] and @racket[τs2] must have the same length.}} 553 @item{@defproc[(same-types? [τs (listof type?)]) boolean?]{ 554 A phase 1 predicate for checking if a list of types are all the same.}} 555 @item{@defparam[current-type=? binary-type-pred binary-type-pred]{ 556 A phase 1 parameter for computing type equality. Is initialized to @racket[type=?].}} 557 @item{@defidform[#%type]{The default "kind" used to validate types.}} 558 @item{@defproc[(#%type? [x Any]) boolean?]{Phase 1 predicate recognizing @racket[#%type].}} 559 @item{@defproc[(type? [x Any]) boolean?]{A phase 1 predicate recognizing well-formed types. 560 Checks that @racket[x] is a syntax object and has syntax propety @racket[#%type].}} 561 @item{@defparam[current-type? type-pred type-pred]{A phase 1 parameter, initialized to @racket[type?], 562 used to recognize well-formed types. 563 Useful when reusing type rules in different languages. For example, 564 System F-omega may define this to recognize types with "star" kinds.}} 565 @item{@defproc[(any-type? [x Any]) boolean?]{A phase 1 predicate recognizing valid types. 566 Defaults to @racket[type?].}} 567 @item{@defparam[current-any-type? type-pred type-pred]{A phase 1 parameter, 568 initialized to @racket[any-type?], 569 used to validate (not necessarily well-formed) types. 570 Useful when reusing type rules in different languages. For example, 571 System F-omega may define this to recognize types with a any valid kind, 572 whereas @racket[current-type?] would recognize types with only the "star" kind.}} 573 @item{@defproc[(mk-type [stx syntax?]) type?]{ 574 Phase 1 function that marks a syntax object as a type by attaching @racket[#%type]. 575 Useful for defining your own type with arbitrary syntax that does not fit with 576 @racket[define-base-type] or @racket[define-type-constructor].}} 577 @item{@defthing[type stx-class]{A syntax class that calls @racket[current-type?] 578 to validate well-formed types. 579 Binds a @racket[norm] attribute to the type's expanded representation.}} 580 @item{@defthing[any-type stx-class]{A syntax class that calls @racket[current-any-type?] 581 to validate types. 582 Binds a @racket[norm] attribute to the type's expanded representation.}} 583 @item{@defthing[type-bind stx-class]{A syntax class recognizing 584 syntax objects with shape @racket[[x:id (~datum :) τ:type]]. 585 Binds a @racket[x] attribute to the binding identifier, and a @racket[type] attribute 586 to the type's expanded representation.}} 587 @item{@defthing[type-ctx stx-class]{A syntax class recognizing 588 syntax objects with shape @racket[(b:type-bind ...)]. 589 Binds a @racket[x] attribute to the binding identifiers, and a @racket[type] attribute 590 to the expanded representation of the types.}} 591 @item{@defthing[type-ann stx-class]{A syntax class recognizing 592 syntax objects with shape @racket[{τ:type}] where the braces are required. 593 Binds a @racket[norm] attribute to the type's expanded representation.}} 594 595 @item{@defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{ 596 Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e] using @tt{key1}.}} 597 598 @item{@defproc[(typeof [e expr-stx]) type-stx]{ 599 Phase 1 function returning type of @racket[e], at @tt{key1}.}} 600 601 ] 602 } 603 604 @section{@racket[require] and @racket[provide]-related Forms} 605 606 @defform[(typed-out x+ty+maybe-rename ...) 607 #:grammar 608 ([x+ty+maybe-rename 609 (code:line [x ty]) 610 (code:line [x : ty]) 611 (code:line [[x ty] out-x]) 612 (code:line [[x : ty] out-x])] 613 [x identifier?] 614 [out-x identifier?] 615 [ty type?])]{ 616 A provide-spec that adds type @racket[ty] to untyped @racket[x] and provides 617 that typed identifier as either @racket[x], or @racket[out-x] if it's specified. 618 619 Equivalent to a @racket[define-primop] that automatically provides its 620 definition.} 621 622 @defform[(extends base-lang option ...) 623 #:grammar 624 ([option (code:line #:except id ...) 625 (code:line #:rename [old new] ...)])]{ 626 Requires all forms from @racket[base-lang] and reexports them. Tries to 627 automatically handle conflicts for commonly used forms like @racket[#%app]. 628 The imported names are available for use in the current module, with a 629 @tt{base-lang:} prefix.} 630 @defform[(reuse name ... #:from base-lang) 631 #:grammar 632 ([name id 633 [old new]])]{ 634 Reuses @racket[name]s from @racket[base-lang].} 635 636 @; Sec: Suffixed Racket bindings ---------------------------------------------- 637 @section[#:tag "racket-"]{Suffixed Racket Bindings} 638 639 To help avoid name conflicts, Turnstile re-provides all Racket bindings with a 640 @litchar{-} suffix. These bindings are automatically used in some cases, e.g., 641 @racket[define-primop], but in general are useful for avoiding name conflicts, 642 particularly for commonly used macros like @racket[#%app]. 643 644 @; Sec: turnstile/lang ---------------------------------------------- 645 @section[#:tag "turnstilelang"]{@hash-lang[] @racketmodname[turnstile]/lang} 646 647 Languages implemented using @hash-lang[] @racketmodname[turnstile] 648 must manually provide @racket[#%module-begin] and other forms required by 649 Racket. 650 651 For convenience, Turnstile additionally supplies @hash-lang[] 652 @racketmodname[turnstile]@tt{/lang}. Languages implemented using this language 653 will automatically provide Racket's @racket[#%module-begin], 654 @racket[#%top-interaction], @racket[#%top], and @racket[require]. 655 656 @; Sec: Lower-level functions ------------------------------------------------- 657 @section{Lower-level Functions} 658 659 This section describes lower-level functions and parameters. It's usually not 660 necessary to call these directly, since @racket[define-typed-syntax] and other 661 forms already do so, but some type systems may require extending some 662 functionality. 663 664 @defproc[(infer [es (listof expr-stx)] 665 [#:ctx ctx (listof bindings) null] 666 [#:tvctx tvctx (listof tyvar-bindings) null] 667 [#:tag tag symbol? ':]) 668 (list tvs xs es τs)]{ 669 670 Phase 1 function expanding a list of expressions, in the given contexts and 671 computes their types. Returns the expanded expressions, their types, and 672 expanded identifiers from the contexts, e.g. 673 674 @racket[(infer (list #'(+ x 1)) #:ctx ([x : Int]))] 675 676 might return 677 678 @racket[(list #'() #'(x-) #'((#%plain-app x- 1)) #'(Int))]. 679 680 The context elements have the same shape as in @racket[define-typed-syntax]. 681 The contexts use @racket[let*] semantics, where each binding is in scope for 682 subsequent bindings. 683 684 Use the @tt{tag} keyword argument to specify the key for the 685 returned "type". The default key is @litchar{:}. For example, a programmer may 686 want to specify a @litchar{::} key when using @racket[infer] to compute the 687 kinds on types.} 688 689 @defproc[(subst [τ type-stx] 690 [x identifier?] 691 [e expr-stx] 692 [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{ 693 Phase 1 function that replaces occurrences of @racket[x], as determined by @racket[cmp], with 694 @racket[τ] in @racket[e].} 695 696 @defproc[(substs [τs (listof type-stx)] 697 [xs (listof identifier?)] 698 [e expr-stx] 699 [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{ 700 Phase 1 function folding @racket[subst] over the given @racket[τs] and @racket[xs].} 701 702 @defform[(type-error #:src srx-stx #:msg msg args ...)]{ 703 Phase 1 form that throws a type error using the specified information. @racket[msg] is a format string that references @racket[args].} 704 705 @section{Subtyping} 706 707 WARNING: very experimental 708 709 Types defined with @racket[define-type-constructor] and 710 @racket[define-binding-type] may specify variance information and subtyping 711 languages may use this information to help compute the subtype relation. 712 713 The possible variances are: 714 @defthing[covariant variance?] 715 @defthing[contravariant variance?] 716 @defthing[invariant variance?] 717 @defthing[irrelevant variance?] 718 719 @defproc[(variance? [v any/c]) boolean/c]{ 720 Predicate that recognizes the variance values.} 721 722 723 @section{Modes} 724 725 @defmodule[turnstile/mode #:use-sources (turnstile/mode)] 726 @(define mode-ev 727 (let ([ev (make-base-eval)]) 728 (ev '(require turnstile/mode)) 729 ev)) 730 731 Modes are typically used by the @racket[#:mode] and @racket[#:submode] 732 keywords in @racket[define-typed-syntax] (and related forms). When judgements 733 are parameterized by a @racket[mode] value, the parameter 734 @racket[current-mode] is set to that value for the extend of the 735 sub-premises. Additionally, the function @racket[mode-setup-fn] is called 736 before setting @racket[current-mode], and the function 737 @racket[mode-teardown-fn] is called after @racket[current-mode] is restored to 738 its previous value. 739 740 @defstruct*[mode ([setup-fn (-> any)] [teardown-fn (-> any)])]{ 741 Structure type for modes. Modes can be used to parameterize type judgements 742 or groups of type judgements, to give additional context and to help enable 743 flow-sensitive languages. 744 745 User defined modes should be defined as structs that inherit from @racket[mode]. 746 } 747 748 @defproc[(make-mode [#:setup setup-fn (-> any) void] 749 [#:teardown teardown-fn (-> any) void]) mode?]{ 750 Constructs a new @racket[mode] object with the given setup and teardown functions. 751 } 752 753 @defparam[current-mode mode mode? #:value (make-mode)]{ 754 A parameter that holds the current mode. Typically parameterized using the keywords 755 @racket[#:mode] and @racket[#:submode] from @racket[define-typed-syntax] forms. 756 } 757 758 @defform[(with-mode mode-expr body ...+) 759 #:contracts ([mode-expr mode?])]{ 760 The result of @racket[with-mode] is the result of the last @racket[_body]. 761 The parameter @racket[current-mode] is assigned to the result of 762 @racket[_mode-expr] for the extent of the @racket[_body] expressions. The 763 function @racket[mode-setup-fn] is called on the result of 764 @racket[_mode-expr] before @racket[current-mode] is set, and the function 765 @racket[mode-teardown-fn] is called after @racket[current-mode] is restored 766 to its previous value. 767 768 @examples[#:eval mode-ev 769 (define-struct (my-mode mode) ()) 770 (define M (make-my-mode (λ () (displayln "M setup")) 771 (λ () (displayln "M teardown")))) 772 (with-mode M 773 (displayln (current-mode)))]} 774 775 @defproc[(make-param-mode [param parameter?] [value any/c]) mode?]{ 776 Creates a @racket[mode] that assigns the given parameter to the given 777 value for the extent of the mode. 778 779 @examples[#:eval mode-ev 780 (define current-scope (make-parameter 'outer)) 781 (with-mode (make-param-mode current-scope 'inner) 782 (displayln (current-scope)))]} 783 784 785 @section{Miscellaneous Syntax Object Functions} 786 787 These are all phase 1 functions. 788 789 @defproc[(stx-length [stx syntax?]) exact-nonnegative-integer?]{Analogous to @racket[length].} 790 @defproc[(stx-length=? [stx1 syntax?] [stx2 syntax?]) boolean?]{ 791 Returns true if two syntax objects are of equal length.} 792 @defproc[(stx-andmap [p? (-> syntax? boolean?)] [stx syntax?]) (listof syntax?)]{ 793 Analogous to @racket[andmap].}