On this page:
2.1 Typing Unicode Characters
2.2 Forms
define-typed-syntax
define-typerule
define-syntax/  typecheck
syntax-parse/  typecheck
define-typed-variable-rename
define-typed-variable
define-primop
define-syntax-category
2.3 Forms for Defining Types
define-base-type
define-base-types
define-type-constructor
define-binding-type
define-internal-type-constructor
define-internal-binding-type
2.4 Type Operations
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
2.5 Syntax Patterns
~typecheck
~⊢
2.6 Syntax Classes
type
any-type
type-bind
type-ctx
type-ann
2.7 require and provide-related Forms
type-out
typed-out
extends
reuse
2.8 Suffixed Racket Bindings
2.9 #lang turnstile/  lang
2.10 #lang turnstile/  quicklang
2.11 #lang turnstile/  base
2.12 Lower-level Functions
infer
current-use-stop-list?
subst
substs
type-error
type->str
add-orig
get-orig
2.13 Subtyping
variance?
covariant
contravariant
invariant
irrelevant
2.14 Modes
mode
make-mode
current-mode
with-mode
make-param-mode
2.15 Miscellaneous Syntax Object Functions
stx-length
stx-length=?
stx-andmap
2.16 Special Identifiers
2.17 Non-Unicode Identifiers
<=
=>
>>
>>>
/  -
7.7

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-\.

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

2.2 Forms

syntax

(define-typed-syntax (name-id . pattern) 
  premise ...
  --------
  conclusion)
(define-typed-syntax name-id option ... rule ...+)
 
option = syntax-parse option
     
rule = 
[expr-pattern 
 premise ...
 --------
 conclusion]
  | 
[expr-pattern  type-pattern 
 premise ...
 --------
 ⇐-conclusion]
  | 
[expr-pattern  key pattern 
 premise ...
 --------
 ⇐-conclusion]
     
expr-pattern = syntax-parse syntax pattern
     
type-pattern = syntax-parse syntax pattern
     
expr-template = quasisyntax template
     
type-template = quasisyntax template
     
key = identifier?
     
premise = [ tc ... prem-options] ooo ...
  | [ctx-elem ...  tc ... prem-options] ooo ...
  | [ctx  tc ... prem-options] ooo ...
  | [ctx ctx  tc ... prem-options] ooo ...
  | [ . tc-elem] ooo ...
  | [ctx-elem ...  . tc-elem] ooo ...
  | [ctx  . tc-elem] ooo ...
  | [ctx ctx  . tc-elem] ooo ...
  | type-relation
  | #:mode mode-expr (premise ...)
  | #:submode fn-expr (premise ...)
  | syntax-parse pattern directive
     
ctx = (ctx-elem ...)
     
ctx-elem = [id  id key template ... ...] ooo ...
     
tc = tc-elem ooo ...
     
tc-elem = [expr-template  expr-pattern  type-pattern]
  | [expr-template  expr-pattern  key pattern]
  | [expr-template  expr-pattern ( key pattern) ooo ...]
  | [expr-template  expr-pattern  type-template]
  | [expr-template  expr-pattern  key template]
  | [expr-template  expr-pattern ( key template) ooo ...]
     
type-relation = [type-template τ= type-template] ooo ...
  | [type-template τ= type-template #:for expr-template] ooo ...
  | [type-template τ⊑ type-template] ooo ...
  | [type-template τ⊑ type-template #:for expr-template] ooo ...
     
prem-options = 
  | #:mode mode-expr
  | #:submode fn-expr
     
conclusion = [ expr-template  type-template]
  | [ expr-template  key template]
  | [ expr-template ( key template) ooo ...]
  | [ expr-template]
  | [#:error expr-template]
     
⇐-conclusion = [ expr-template]
     
ooo = ...
Generates a macro definition that also performs type checking. The macro is generated from syntax-parse syntax patterns and pattern directives, along with type-judgement-like clauses that interleave typechecking and macro expansion. The resulting macro type checks its surface syntax as part of macro expansion and the resulting type is attached to the expanded expression.

Premises

Bidirectional judgements

Turnstile define-typed-syntax rules use bidirectional type checking judgements:
  • [ e e- τ] declares that expression e expands to e- and has type τ, where e is the input and, e- and τ outputs. Syntactically, e is a syntax template position and e- and τ are syntax pattern positions.

  • Dually, one may write [ e e- τ] to check that e has type τ. Here, both e and τ are inputs (templates) and only e- is an output (pattern).

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.

syntax

(define-typerule ....)

syntax

(define-syntax/typecheck ....)

Aliases for define-typed-syntax.

syntax

(syntax-parse/typecheck stx option ... rule ...+)

A syntax-parse-like form that supports define-typed-syntax-style clauses. In particular, see the "rule" part of define-typed-syntax’s grammar above.

syntax

(define-typed-variable-rename typed-var  untyped-var : type)

Defines typed-var as a variable with type type that erases to untyped-var. Supports set!. Generally typed definition forms will expand to a combination of an untyped define and this form.

syntax

(define-typed-variable id typed-e  τ)

(define-typed-variable id typed-e)
(define-typed-variable id untyped-e  τ)
Defines id as a typed, top-level name. id expands to another binding that is bound to the supplied expression.

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))])

syntax

(define-primop typed-op-id τ)

(define-primop typed-op-id : τ)
(define-primop typed-op-id op-id τ)
(define-primop typed-op-id op-id : τ)
(define-primop typed-op-id #:as op-id τ)
(define-primop typed-op-id #:as op-id : τ)
Defines typed-op-id by attaching type τ to (untyped) identifier op-id, e.g.:

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

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

syntax

(define-syntax-category name-id)

(define-syntax-category key1 name-id)
(define-syntax-category key1 name-id key2)
Defines a new "category" of syntax by defining a series of forms and functions. Turnstile pre-declares (define-syntax-category type), which in turn defines the forms and functions below.

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.

syntax

(define-base-type base-type-name-id option ...)

(define-base-type base-type-name-id key tag option ...)
 
option = #:runtime
Defines a base type. (define-base-type τ) in turn defines:
  • τ, an identifier macro representing type τ.

  • τ?, a phase 1 predicate recognizing type τ.

  • , a phase 1 pattern expander recognizing type τ.

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.

syntax

(define-base-types base-type-name-id ...)

Defines multiple base types, each using the default key and options.

syntax

(define-type-constructor name-id option ...)

 
option = #:arity op n
  | #:runtime
  | #:arg-variances expr
  | #:extra-info stx
Defines a type constructor (that does not bind type variables). Defining a type constructor τ subsequently defines:
  • τ, a macro for constructing an instance of type τ, with the specified arity. Validates inputs and expands to τ-, attaching #%type at key2.

  • τ-, an internal macro that expands to the internal (i.e., fully expanded) type representation. Does not validate inputs or attach any extra properties. This macro is useful when creating a separate kind system, see define-internal-type-constructor.

  • τ?, a phase 1 predicate recognizing type τ.

  • , a phase 1 pattern expander recognizing type τ.

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:

(define-type-constructor  #:arity >= 1
 #:arg-variances
 (λ (stx)
   (syntax-parse stx
     [(_ τ_in ... τ_out)
      (append
       (make-list (stx-length #'[τ_in ...]) contravariant)
       (list covariant))])))

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

syntax

(define-binding-type name-id option ...)

 
option = #:arity op n
  | #:bvs op n
  | #:arr kindcon
  | #:arg-variances expr
  | #:extra-info stx
Similar to define-type-constructor, except define-binding-type defines a type that binds type variables. Defining a type constructor τ defines:

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.

syntax

(define-internal-type-constructor name-id option ...)

 
option = #:arg-variances expr
  | #:extra-info stx
Like define-type-constructor, except the surface macro is not defined. Use this form, for example, when creating a separate kind system so that you can still use other Turnstile conveniences like pattern expanders.

syntax

(define-internal-binding-type name-id option ...)

 
option = #:arr kindcon
  | #:arg-variances expr
  | #:extra-info stx
Analogous to define-internal-type-constructor, but for binding types.

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.

parameter

(current-type-eval)  (-> syntax? syntax?)

(current-type-eval type-eval)  void?
  type-eval : (-> syntax? syntax?)
A phase 1 parameter for controlling "type evaluation". A type-eval function consumes and produces syntax. It is typically used to convert a type into a canonical representation. The (current-type-eval) is called immediately before attaching a type to a syntax object, i.e., by assign-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.

parameter

(current-typecheck-relation)  (-> type? type? boolean?)

(current-typecheck-relation type-cmp)  void?
  type-cmp : (-> type? type? boolean?)
A phase 1 parameter for controlling type checking, used by define-typed-syntax. A type-cmp function consumes two types—the first is the given type and the second is the expected type—and returns true if they "type check". It defaults to type=? though it does not have to be a symmetric relation. Useful for reusing rules that differ only in the type check operation, e.g., equality vs subtyping.

procedure

(typecheck? τ1 τ2)  boolean?

  τ1 : type?
  τ2 : type?
A phase 1 function that calls current-typecheck-relation. The first argument is the given type and the second is the expected type.

procedure

(typechecks? τs1 τs2)  boolean?

  τs1 : (or/c (listof type?) (stx-listof type?))
  τs2 : (or/c (listof type?) (stx-listof type?))
Phase 1 function mapping typecheck? over lists of types, pairwise. τs1 and τs2 must have the same length. The first list contains the given types and the second list contains the expected types.

A phase 1 parameter for customizing the behavior of type=?. In addition to the types to compare, it receives environments used to map type variables in each type respectively to a common representation. When making a recursive call to current-type=? under a binding form, pass extended environments mapping the binders to a new unique value (compared by eq?).

procedure

(type=? τ1 τ2)  boolean?

  τ1 : type?
  τ2 : type?
A phase 1 equality predicate for types that computes structural, free-identifier=? equality, but includes alpha-equivalence.

Examples:
> (define-base-type Int)
> (define-base-type String)
> (begin-for-syntax (displayln (type=? #'Int #'Int)))

#t

> (begin-for-syntax (displayln (type=? #'Int #'String)))

#f

> (define-type-constructor  #:arity > 0)
> (define-binding-type  #:arity = 1 #:bvs = 1)
> (begin-for-syntax
    (displayln
      (type=? ((current-type-eval) #'( (X) X))
              ((current-type-eval) #'( (Y) Y)))))

#t

> (begin-for-syntax
    (displayln
      (type=? ((current-type-eval) #'( (X) ( (Y) ( X Y))))
              ((current-type-eval) #'( (Y) ( (X) ( Y X)))))))

#t

> (begin-for-syntax
    (displayln
      (type=? ((current-type-eval) #'( (Y) ( (X) ( Y X))))
              ((current-type-eval) #'( (X) ( (X) ( X X)))))))

#f

procedure

(types=? τs1 τs2)  boolean?

  τs1 : (listof type?)
  τs2 : (listof type?)
A phase 1 predicate checking that τs1 and τs2 are equivalent, pairwise. Thus, τs1 and τs2 must have the same length.

procedure

(same-types? τs)  boolean?

  τs : (listof type?)
A phase 1 predicate for checking if a list of types are all the same.

procedure

(type? x)  boolean?

  x : syntax?
A phase 1 predicate recognizing well-formed types. Checks that x is a syntax object and has syntax propety #%type.

parameter

(current-type?)  (-> syntax? boolean?)

(current-type? type-pred)  void?
  type-pred : (-> syntax? boolean?)
A phase 1 parameter, initialized to type?, used to recognize well-formed types. Useful when reusing type rules in different languages. For example, System F-omega may define this to recognize types with "star" kinds.

procedure

(any-type? x)  boolean?

  x : syntax?
A phase 1 predicate recognizing valid types. Defaults to type?.

parameter

(current-any-type?)  (-> syntax? boolean?)

(current-any-type? type-pred)  void?
  type-pred : (-> syntax? boolean?)
A phase 1 parameter, initialized to any-type?, used to validate (not necessarily well-formed) types. Useful when reusing type rules in different languages. For example,System F-omega may define this to recognize types with a any valid kind, whereas current-type? would recognize types with only the "star" kind.

procedure

(assign-type e τ)  syntax?

  e : syntax?
  τ : type?
Phase 1 function that calls current-type-eval on τ and attaches it to e using key1.

procedure

(typeof e)  type?

  e : syntax?
Phase 1 function returning type of e, at key1.

syntax

#%type

The default "kind" used to validate types.

procedure

(#%type? x)  boolean?

  x : any/c
Phase 1 predicate recognizing #%type.

procedure

(mk-type stx)  type?

  stx : syntax?
Phase 1 function that marks a syntax object as a type by attaching #%type. Useful for defining your own type with arbitrary syntax that does not fit with define-base-type or define-type-constructor.

2.5 Syntax Patterns

syntax

(~typecheck premise ...)

A syntax-parse pattern expander that supports typechecking syntax.

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.

Example:
> (begin-for-syntax
    (struct clause [stx- result-type])
    ; f : Stx -> Clause
    (define (f stx)
      (syntax-parse stx
        [(~and [condition:expr body:expr]
               (~typecheck
                [ condition  condition-  Bool]
                [ body  body-  τ_body]))
         (clause #'[condition- body-] #'τ_body)])))

syntax

(~⊢ tc ...)

A shorthand pattern expander for (~typcheck [ tc ...]).

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

Example:
> (begin-for-syntax
    (struct clause [stx- result-type])
    ; f : Stx -> Clause
    (define (f stx)
      (syntax-parse stx
        [(~and [condition:expr body:expr]
               (~⊢ condition  condition-  Bool)
               (~⊢ body  body-  τ_body))
         (clause #'[condition- body-] #'τ_body)])))

2.6 Syntax Classes

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

syntax class

type

A syntax class that calls current-type? to validate well-formed types. Binds a norm attribute to the type’s expanded representation.

syntax class

any-type

A syntax class that calls current-any-type? to validate types. Binds a norm attribute to the type’s expanded representation.

syntax class

type-bind

A syntax class recognizing syntax objects with shape [x:id (~datum :) τ:type]. Binds a x attribute to the binding identifier, and a type attribute to the type’s expanded representation.

syntax class

type-ctx

A syntax class recognizing syntax objects with shape (b:type-bind ...). Binds a x attribute to the binding identifiers, and a type attribute to the expanded representation of the types.

syntax class

type-ann

A syntax class recognizing syntax objects with shape {τ:type} where the braces are required. Binds a norm attribute to the type’s expanded representation.

2.7 require and provide-related Forms

syntax

(type-out ty-id ...)

A provide-spec that, for each given ty-id, provides ty-id, and provides for-syntax a predicate ty-id? and a pattern expander ~ty-id.

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

syntax

(typed-out x+ty+maybe-rename ...)

 
x+ty+maybe-rename = [x ty]
  | [x : ty]
  | [[x ty] out-x]
  | [[x : ty] out-x]
     
x = identifier?
     
out-x = identifier?
     
ty = type?
A provide-spec that adds type ty to untyped x and provides that typed identifier as either x, or out-x if it’s specified.

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

syntax

(extends base-lang option ...)

 
option = #:except id ...
  | #:rename [old new] ...
Requires all forms from base-lang and reexports them. Tries to automatically handle conflicts for commonly used forms like #%app. The imported names are available for use in the current module, with a base-lang: prefix.

syntax

(reuse name ... #:from base-lang)

 
name = id
  | [old new]
Reuses names from base-lang.

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.

procedure

(infer es    
  [#:ctx ctx    
  #:tvctx tvctx    
  #:tag tag    
  #:stop-list? stop-list?])  (list tvs xs es τs)
  es : (listof expr-stx)
  ctx : (listof binding-stx) = null
  tvctx : (listof tyvar-binding-stx) = null
  tag : symbol? = ':
  stop-list? : boolean? = #t
Phase 1 function expanding a list of expressions, in the given contexts and computes their types. Returns the expanded expressions, their types, and expanded identifiers from the contexts, e.g.

(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.

parameter

(current-use-stop-list?)  boolean?

(current-use-stop-list? flag)  void?
  flag : boolean?
 = #t
An additional means to control the stop-list optimization. Set to #f to disable. Useful for languages with features like dependent types where full expansion is always needed.

procedure

(subst τ x e [cmp])  expr-stx

  τ : syntax?
  x : identifier?
  e : syntax?
  cmp : (-> identifier? identifier? boolean?)
   = bound-identifier=?
Phase 1 function that replaces occurrences of x, as determined by cmp, with τ in e.

procedure

(substs τs xs e [cmp])  expr-stx

  τs : (listof syntax?)
  xs : (listof identifier?)
  e : syntax?
  cmp : (-> identifier? identifier? boolean?)
   = bound-identifier=?
Phase 1 function folding subst over the given τs and xs.

syntax

(type-error #:src srx-stx #:msg msg args ...)

Phase 1 form that throws a type error using the specified information. msg is a format string that references args.

procedure

(type->str τ)  string?

  τ : type?
Phase 1 function that produces a string representation of the given type τ. Creates a string by traversing the syntax property 'orig, which can be manipulated with add-orig. type->str is used in typechecking error messages.

Example:
> (begin-for-syntax
    (define t ((current-type-eval) #'( Int Int)))
    (displayln (type->str t)))

(→ Int Int)

procedure

(add-orig e orig)  syntax?

  e : syntax?
  orig : syntax?

procedure

(get-orig e)  syntax?

  e : syntax?
Phase 1 functions for manipulation the 'orig property. add-orig returns the syntax e with orig added. get-orig returns the last added 'orig on e, or returns itself if none were added.

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.

procedure

(variance? v)  boolean?

  v : any/c
Predicate that recognizes the variance values.

The different possible variances.

2.14 Modes

WARNING: experimental

 (require turnstile/mode) package: turnstile-lib

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.

struct

(struct mode (setup-fn teardown-fn))

  setup-fn : (-> any)
  teardown-fn : (-> any)
Structure type for modes. Modes can be used to parameterize type judgements or groups of type judgements, to give additional context and to help enable flow-sensitive languages.

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

procedure

(make-mode [#:setup setup-fn    
  #:teardown teardown-fn])  mode?
  setup-fn : (-> any) = void
  teardown-fn : (-> any) = void
Constructs a new mode object with the given setup and teardown functions.

parameter

(current-mode)  mode?

(current-mode mode)  void?
  mode : mode?
 = (make-mode)
A parameter that holds the current mode. Typically parameterized using the keywords #:mode and #:submode from define-typed-syntax forms.

syntax

(with-mode mode-expr body ...+)

 
  mode-expr : mode?
The result of with-mode is the result of the last body. The parameter current-mode is assigned to the result of mode-expr for the extent of the body expressions. The function mode-setup-fn is called on the result of mode-expr before current-mode is set, and the function mode-teardown-fn is called after current-mode is restored to its previous value.

Examples:
> (define-struct (my-mode mode) ())
> (define M (make-my-mode (λ () (displayln "M setup"))
                          (λ () (displayln "M teardown"))))
> (with-mode M
    (displayln (current-mode)))

M setup

#<my-mode>

M teardown

procedure

(make-param-mode param value)  mode?

  param : parameter?
  value : any/c
Creates a mode that assigns the given parameter to the given value for the extent of the mode.

Examples:
> (define current-scope (make-parameter 'outer))
> (with-mode (make-param-mode current-scope 'inner)
    (displayln (current-scope)))

inner

2.15 Miscellaneous Syntax Object Functions

These are all phase 1 functions.

procedure

(stx-length stx)  exact-nonnegative-integer?

  stx : syntax?
Analogous to length.

procedure

(stx-length=? stx1 stx2)  boolean?

  stx1 : syntax?
  stx2 : syntax?
Returns true if two syntax objects are of equal length.

procedure

(stx-andmap p? stx)  (listof syntax?)

  p? : (-> syntax? boolean?)
  stx : syntax?
Analogous to andmap.

2.16 Special Identifiers

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

syntax

This and the following ids throw a syntax error when used in an invalid context.

syntax

syntax

syntax

syntax

2.17 Non-Unicode Identifiers

 (require turnstile/no-unicode) package: turnstile-lib

The following identifiers are non-unicode aliases to other Turnstile ids.

syntax

<=

Alias for .

syntax

=>

Alias for .

syntax

>>

Alias for .

syntax

>>>

Alias for .

syntax

/-

Alias for .