2 The Turnstile Reference

2.1 Typing Unicode Characters

Turnstile utilizes unicode. Here are DrRacket keyboard shortcuts for the relevant characters. Type (any unique prefix of) the following and then press Control-\ or Alt-\.

• \vdash → ⊢

• \gg → ≫

• \rightarrow → →

• \Rightarrow → ⇒

• \Leftarrow → ⇐

• \succ → ≻

See also Non-Unicode Identifiers for non-unicode aliases.

2.2 Forms

Premises

Bidirectional judgements

Each bidirectional arrow has a generalized form that associates a key with a value, e.g., [⊢ e ≫ e- (⇒ key pat) ...]. A programmer may use this generalized form 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, :, i.e., the "type" key, is used.

Contexts

A context may be specified to the left of the turnstile. A context element has shape [⊢ x ≫ x- key pat ... ...] where x- is a pattern matching the expansion of x and the interleaved key ... and pat ... are arbitrary key-value pairs, e.g. a : key and type pattern.

A context has 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 (if properly ordered). In addition, Turnstile allows writing two separate contexts, grouped by parens, where bindings in first are in scope for the second. This is often convenient for scenarios that Racket’s pattern language cannot express, e.g., when there two distinct groups of bindings, a pattern x ... y ... will not work as expected.

For convenience, lone identifiers written to the left of the turnstile are automatically treated as type variables.

Modes

The keyword #:mode, when appearing at end of a typechecking rule, sets the parameter current-mode to the mode object supplied by mode-expr, for the extent of that rule. #:mode, when appearing as its own premise, sets the current-mode parameter for the extent of all the grouped sub-premises.

The keyword #:submode is similar to #:mode, but it calls (fn-expr (current-mode)) to obtain the new mode object. Thus, #:mode (fn-expr (current-mode)) is identical to #:submode fn-expr.

See Modes for more details.

WARNING: #:mode is unaware of the backtracking behavior of syntax-parse. If pattern backtracking escapes a #:mode group, it may leave current-mode in an undesirable state.

Conclusion

Bidirectional judgements below the conclusion line invert their inputs and outputs so that both positions in [⊢ e- ⇒ τ] are syntax templates and means that e- is the output of the generated macro and it has type τ attached. The generalized key-value form of the bidirectional judgements may also be used in the conclusion.

The ≻ conclusion form is useful in many scenarios where the rule being implemented may not want to attach type information. E.g.,

1. when a rule’s output is another typed macro.

   For example, here is a hypothetical typed-let* that is implemented in terms of a typed-let:

   (define-typed-syntax typed-let*

   [(_ () e_body) ≫

   --------

   [≻ e_body]]

   [(_ ([x e] [x_rst e_rst] ...) e_body) ≫

   --------

   [≻ (typed-let ([x e]) (typed-let* ([x_rst e_rst] ...) e_body))]])

   The conclusion in the first clause utilizes ≻ since the body already carries its own type. The second clause uses ≻ because it defers to typed-let, which will attach type information.

2. when a rule extends another.

   This is related to the first example. For example, here is a #%datum that extends another with more typed literals (see also Extending a Language).

   (define-typed-syntax typed-datum

   [(_ . n:integer) ≫

   --------

   [⊢ (#%datum- . n) ⇒ Int]]

   [(_ . x) ≫

   --------

   [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])

   (define-typed-syntax extended-datum

   [(_ . s:str) ≫

   --------

   [⊢ (#%datum- . s) ⇒ String]]

   [(_ . x) ≫

   --------

   [≻ (typed-datum . x)]])

3. for top-level forms.

   For example, here is a basic typed version of define:

   (define-typed-syntax define

   [(_ x:id e) ≫

   [⊢ e ≫ e- ⇒ τ]

   #:with y (generate-temporary #'x)

   --------

   [≻ (begin-

   (define-typed-variable-rename x ≫ y : τ)

   (define- y e-))]])

   This macro creates an indirection define-typed-variable-rename in order to attach type information to the top-level x identifier, so the define forms themselves do not need type information.

Note: define-typed-syntax is generated by (define-syntax-category type). See define-syntax-category for more information.

With the ⇐ variant, typed-e is checked to have type τ. id also has type τ.

With middle variant, id has the type of typed-e.

With the ⇒ variant, both id and untyped-e are assigned type τ (using assign-type).

The difference between define-typed-variable and define-typed-variable-rename is that the latter assumes that an untyped name already exists. In contrast, define-typed-variable uses generate-temporary to first define an untyped name, and then uses define-typed-variable-rename to define the typed name in terms of the untyped name. E.g., define-primop essentially just uses define-typed-variable-rename, but a typed define needs more.

Here is an example typed-λ and typed-define that expands to typed-λ and define-typed-variable.

(define-typerule typed-λ

[(_ ([x:id (~datum :) τ:type] ...) e) ≫

[[x ≫ x- : τ.norm] ... ⊢ e ≫ e- ⇒ τout]

--------------

[⊢ (λ- (x- ...) e-) ⇒ (-> τ.norm ... τout)]]

[(_ (x:id ...) e) ⇐ (~-> τin ... τout) ≫

[[x ≫ x- : τin] ... ⊢ e ≫ e- ⇐ τout]

--------------

[⊢ (λ- (x- ...) e-)]])

(define-typerule

(define (f:id [x:id (~datum :) τin:type] ...) (~datum :) τout:type e) ≫

--------

[≻ (define-typed-variable f (typed-λ (x ...) e) ⇐ (-> τin.norm ... τout.norm))])

(define-primop typed+ + : (→ Int Int))

When not specified, op-id is typed-op-id suffixed with - (see Suffixed Racket Bindings).

Each category of syntax is associated with two keys: key1 is used when attaching values in the category to other syntax, e.g., attaching types to terms, and key2 is used for attaching an additional syntax property to values in the category, e.g. using #%type to indicate well-formedness.

If no keys are specified, key1 is : and key2 is ::. If only key1 is given, then key2 is key1 appended to itself.

Defining another category, e.g., (define-syntax-category kind) defines a separate set of forms and functions, e.g., define-kinded-syntax, define-base-kind, kind=?, etc.

The following forms and functions are automatically defined by a (define-syntax-category type) declaration: define-typed-syntax, define-base-type, define-base-types, define-type-constructor, define-binding-type, define-internal-type-constructor, define-internal-binding-type, current-type-eval, current-typecheck-relation, typecheck?, typechecks?, current-type=?, type=?, types=?, same-types?, type?, current-type?, any-type?, current-any-type?, assign-type, typeof, #%type, #%type?, mk-type, type, any-type, type-bind, type-ctx, type-ann

2.3 Forms for Defining Types

Note: The forms in this section are generated by (define-syntax-category type). See define-syntax-category for more information.

Types defined with define-base-type are automatically tagged with a key2-keyed (as specified in the define-syntax-category declaration) #%type syntax property (essentially, a default kind), unless the second form above is used, in which case the specified tag is attached to the type using the specified key.

The #:runtime argument dictates that, rather than throwing an error, type evaluates to a value at runtime.

The #:arity argument specifies the valid shapes for the type. For example (define-type-constructor → #:arity >= 1) defines an arrow type and (define-type-constructor Pair #:arity = 2) defines a pair type. The default arity is = 1.

The #:runtime argument dictates that, rather than throwing an error, type evaluates to a value at runtime.

The #:arg-variances argument is a transformer converting a syntax object of the type to a list of variances for the arguments to the type constructor.

The possible variances are invariant, contravariant, covariant, and irrelevant.

If #:arg-variances is not specified, invariant is used for all positions.

Example:

The #:extra-info argument is useful for attaching additional metainformation to types, for example to communicate accessors to a pattern matching form.

The #:arity and #:bvs arguments specify the valid shapes for the type. For example (define-binding-type ∀ #:arity = 1 #:bvs = 1) defines a type with shape (∀ (X) τ), where τ may reference X.

The default #:arity is = 1 and the default #:bvs is >= 0.

Use the #:arr argument to define a type with kind annotations on the type variables. The #:arr argument is an "arrow" that "saves" the annotations after a type is expanded and annotations are erased, analogous to how → "saves" the type annotations on a lambda.

2.4 Type Operations

Note: The forms in this section are generated by (define-syntax-category type). See define-syntax-category for more information.

It’s not important to immediately understand all these definitions. Some, like type? and mk-type, are more "low-level" and are mainly used by the other forms. The most useful forms are probably define-typed-syntax, and the type-defining forms define-base-type, define-type-constructor, and define-binding-type.

It defaults to full expansion, i.e., (lambda (stx) (local-expand stx 'expression null)), and also stores extra surface syntax information used for error reporting.

One should extend current-type-eval if canonicalization of types depends on combinations of different types, e.g., type lambdas and type application in F-omega.

2.5 Syntax Patterns

For example the pattern

(~typecheck

[⊢ a ≫ a- ⇒ τ_a]

[⊢ b ≫ b- ⇐ τ_a])

typechecks a and b, expecting b to have the type of a, and binding a- and b- to the expanded versions.

This is most useful in places where you want to do typechecking in something other than a type rule, like in a function or a syntax class.

For example the pattern (~⊢ a ≫ a- ⇒ τ_a) typechecks a, binding the expanded version to a- and the type to τ_a.

2.6 Syntax Classes

Note: The forms in this section are generated by (define-syntax-category type). See define-syntax-category for more information.

2.7 require and provide-related Forms

Note: type-out is generated by (define-syntax-category type). See define-syntax-category for more information.

Equivalent to a define-primop that automatically provides its definition.

2.8 Suffixed Racket Bindings

To help avoid name conflicts, Turnstile re-provides all Racket bindings with a - suffix. These bindings are automatically used in some cases, e.g., define-primop, but in general are useful for avoiding name conflicts, particularly for commonly used macros like #%app.

2.9 #lang turnstile/lang

Deprecated: see #lang turnstile/quicklang.

2.10 #lang turnstile/quicklang

Languages implemented using #lang turnstile are responsible for defining and providing certain forms required by Racket, e.g., #%module-begin.

For convenience, Turnstile additionally supplies #lang turnstile/quicklang. Languages implemented using this language will automatically provide Racket’s #%module-begin, #%top-interaction, #%top, require, and some require transformers, e.g., rename-in.

2.11 #lang turnstile/base

Only provides racket/base at phase 1. Does not provide syntax/parse at phase 1.

In contrast, full turnstile provides all of racket and syntax/parse at phase 1.

turnstile/base may load faster than full turnstile (roughly 15% for an empty file, with Racket 7).

2.12 Lower-level Functions

This section describes lower-level functions and parameters. It’s usually not necessary to call these directly, since define-typed-syntax and other forms already do so, but some type systems may require extending some functionality.

(infer (list #'(+ x 1))  #:ctx #'([x : Int]))

might return

(list #'()  #'(x-)  #'((#%plain-app + x- 1))  #'(Int)).

The context elements have the same shape as in define-typed-syntax. The contexts use let* semantics, where each binding is in scope for subsequent bindings.

Use the tag keyword argument to specify the key for the returned "type". The default key is :. For example, a programmer may want to specify a :: key when using infer to compute the kinds on types.

The #:stop-list? argument controls an optimization to avoid unnecessary re-expansion. When #t, expansion for typechecking stops once Racket kernel forms are reached. Note that because types are expected to be in fully expanded form, this flag should be #f when infer is used to infer kinds.

2.13 Subtyping

WARNING: very experimental

Types defined with define-type-constructor and define-binding-type may specify variance information and subtyping languages may use this information to help compute the subtype relation.

2.14 Modes

WARNING: experimental

Modes are typically used by the #:mode and #:submode keywords in define-typed-syntax (and related forms). When judgements are parameterized by a mode value, the parameter current-mode is set to that value for the extent of the sub-premises. Additionally, the function mode-setup-fn is called before setting current-mode, and the function mode-teardown-fn is called after current-mode is restored to its previous value.

User defined modes should be defined as structs that inherit from mode.

2.15 Miscellaneous Syntax Object Functions

These are all phase 1 functions.

2.16 Special Identifiers

The following identifiers are bound (at phase 1) but are only valid within other Turnstile forms like define-typed-syntax.