{"size": 42216, "ext": "scrbl", "max_stars_repo_path": "turnstile-doc/turnstile/scribblings/reference.scrbl", "max_stars_repo_name": "drsooch/macrotypes", "max_stars_repo_stars_event_min_datetime": "2017-01-27T05:56:09.000Z", "max_stars_repo_stars_event_max_datetime": "2022-03-09T09:26:12.000Z", "max_issues_repo_path": "turnstile-doc/turnstile/scribblings/reference.scrbl", "max_issues_repo_name": "drsooch/macrotypes", "max_issues_repo_issues_event_min_datetime": "2017-01-31T15:37:50.000Z", "max_issues_repo_issues_event_max_datetime": "2021-12-30T02:23:50.000Z", "max_forks_repo_path": "turnstile-doc/turnstile/scribblings/reference.scrbl", "max_forks_repo_name": "drsooch/macrotypes", "max_forks_repo_forks_event_min_datetime": "2017-03-22T17:20:40.000Z", "max_forks_repo_forks_event_max_datetime": "2021-09-01T11:31:16.000Z"}
{"max_stars_count": 115, "max_issues_count": 90, "max_forks_count": 15, "avg_line_length": 42.1317365269, "max_line_length": 174, "alphanum_fraction": 0.6493272693}
#lang scribble/manual

@(require scribble/example racket/sandbox
          (for-label (except-in racket/base <= =>)
                     syntax/id-table
                     turnstile/mode turnstile/no-unicode
                     (except-in turnstile/main mk-~ mk-? /- <= =>))
          "doc-utils.rkt" "common.rkt")

@title{The Turnstile Reference}

@section{Typing Unicode Characters}

@; evaluator
@(define the-eval
  (parameterize ([sandbox-output 'string]
                 [sandbox-error-output 'string]
                 [sandbox-eval-limits #f])
    (make-base-eval #:lang 'turnstile)))


@; misc utilities
@(define-syntax-rule (defstxclass id . after)
  (defidform #:kind "syntax class" id . after))


@; syntax category stuff
@(define (def-stx-cat name)
   ; i don't think (tt ..) is the right style, but i can't
   ; figure out how to display it monospace without making "type"
   ; a link
   (racket (define-syntax-category #,(tt name))))

@define[(section/from-stx-cat name)
  @list[
    @section[name]
    @margin-note{
      @bold{Note: } The forms in this section are generated by @def-stx-cat{type}.
      See @racket[define-syntax-category] for more information. }
  ]]

@; insert link?
@; https://docs.racket-lang.org/drracket/Keyboard_Shortcuts.html
Turnstile utilizes unicode. Here are DrRacket keyboard shortcuts for the
relevant characters. Type (any unique prefix of) the following
and then press Control-@litchar{\} or Alt-@litchar{\}.

@itemlist[
  @item{@litchar{\vdash} → @litchar{⊢}}
  @item{@litchar{\gg} → @litchar{≫}}
  @item{@litchar{\rightarrow} → @litchar{→}}
  @item{@litchar{\Rightarrow} → @litchar{⇒}}
  @item{@litchar{\Leftarrow} → @litchar{⇐}}
  @item{@litchar{\succ} → @litchar{≻}}
]

See also @secref{no-unicode} for non-unicode aliases.

@section{Forms}

@; define-typed-syntax---------------------------------------------------------
@defform*[
  #:literals (≫ ⊢ ⇒ ⇐ ≻ --------)
  ((define-typed-syntax (name-id . pattern) ≫
     premise ...
     --------
     conclusion)
   (define-typed-syntax name-id option ... rule ...+))
  #:grammar
  ([option (code:line @#,racket[syntax-parse] option)]
   [rule [expr-pattern ≫
          premise ...
          --------
          conclusion]
         [expr-pattern ⇐ type-pattern ≫
          premise ...
          --------
          ⇐-conclusion]
         [expr-pattern ⇐ key pattern ≫
          premise ...
          --------
          ⇐-conclusion]]
   [expr-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)]
   [type-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)]
   [expr-template (code:line @#,racket[quasisyntax] @#,tech:template)]
   [type-template (code:line @#,racket[quasisyntax] @#,tech:template)]
   [key identifier?]
   [premise (code:line [⊢ tc ... prem-options] ooo ...)
            (code:line [ctx-elem ... ⊢ tc ... prem-options] ooo ...)
            (code:line [ctx ⊢ tc ... prem-options] ooo ...)
            (code:line [ctx ctx ⊢ tc ... prem-options] ooo ...)
            (code:line [⊢ . tc-elem] ooo ...)
            (code:line [ctx-elem ... ⊢ . tc-elem] ooo ...)
            (code:line [ctx ⊢ . tc-elem] ooo ...)
            (code:line [ctx ctx ⊢ . tc-elem] ooo ...)
            type-relation
            (code:line #:mode mode-expr (premise ...))
            (code:line #:submode fn-expr (premise ...))
            (code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
   [ctx (ctx-elem ...)]
   [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)]
   [tc (code:line 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 (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 ...)]
   [prem-options (code:line)
                 (code:line #:mode mode-expr)
                 (code:line #: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 @racket[syntax-parse] @tech:stx-pats and @tech:pat-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.

@; ----------------------------------------------------------------------------
@bold{Premises}

@italic{Bidirectional judgements}

Turnstile @racket[define-typed-syntax] rules use bidirectional type checking
judgements:
@itemlist[
  @item{@racket[[⊢ e ≫ e- ⇒ τ]] declares that expression @racket[e] expands to
@racket[e-] and has type @racket[τ], where @racket[e] is the input and,
@racket[e-] and @racket[τ] outputs. Syntactically, @racket[e] is a syntax
template position and @racket[e-] and @racket[τ] are syntax pattern positions.}

  @item{Dually, one may write @racket[[⊢ e
≫ e- ⇐ τ]] to check that @racket[e] has type @racket[τ]. Here, both @racket[e]
and @racket[τ] are inputs (templates) and only @racket[e-] is an
output (pattern).}]

Each bidirectional arrow has a generalized form that associates a key with a
value, e.g., @racket[[⊢ 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, @litchar{:}, i.e., the "type" key, is used.

@italic{Contexts}

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 a pattern
matching the expansion of @racket[x] and the interleaved @racket[key ...] and
@racket[pat ...] are arbitrary key-value pairs, e.g. a @litchar{:} key and type
pattern.

A context has @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 (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 @racket[x ... y ...] will not work as expected.

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

@italic{Modes}

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

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

See @secref{Modes} for more details.

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


@; ----------------------------------------------------------------------------
@bold{Conclusion}

Bidirectional judgements below the conclusion line invert their inputs and
outputs so that both positions in @racket[[⊢ e- ⇒ τ]] are syntax templates and
means that @racket[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 @racket[≻] conclusion form is useful in many scenarios where the rule being
implemented may not want to attach type information. E.g.,

@itemlist[#:style 'ordered

@item{when a rule's output is another typed macro.

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

@racketblock0[
(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 @racket[≻] since the body already
carries its own type. The second clause uses @racket[≻] because it defers to
@tt{typed-let}, which will attach type information.}

@item{when a rule extends another.

This is related to the first example. For example, here is a @racket[#%datum]
that extends another with more typed literals (see also @secref{stlcsub}).

@racketblock0[

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

@item{for top-level forms.

For example, here is a basic typed version of @racket[define]:

@racketblock0[

(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 @racket[define-typed-variable-rename] in order to
attach type information to the top-level @tt{x} identifier, so the
@racket[define] forms themselves do not need type information.}

]}

@bold{Note: } @racket[define-typed-syntax] is generated
by @def-stx-cat{type}. See @racket[define-syntax-category] for more information.


@; ----------------------------------------------------------------------------

@deftogether[(@defform[(define-typerule ....)]
              @defform[(define-syntax/typecheck ....)])]{
Aliases for @racket[define-typed-syntax].}


@; syntax-parse/typecheck------------------------------------------------------
@defform[(syntax-parse/typecheck stx option ... rule ...+)]{
A @racket[syntax-parse]-like form that supports
@racket[define-typed-syntax]-style clauses. In particular, see the
"rule" part of @racket[define-typed-syntax]'s grammar above.}


@; define-typed-variable-rename -----------------------------------------------

@defform[(define-typed-variable-rename typed-var ≫ untyped-var : type)]{

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

@; define-typed-variable -----------------------------------------------

@defform*[((define-typed-variable id typed-e ⇐ τ)
           (define-typed-variable id typed-e)
           (define-typed-variable id untyped-e ⇒ τ))]{

Defines @racket[id] as a typed, top-level name. @racket[id] expands to another
binding that is bound to the supplied expression.

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

With middle variant, @racket[id] has the type of @racket[typed-e].

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

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

Here is an example @racket[typed-λ] and @racket[typed-define] that expands to 
 @racket[typed-λ] and @racket[define-typed-variable].

@racketblock[
(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 --------------------------------------------------------------
@defform*[((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 @racket[typed-op-id] by attaching type @racket[τ] to (untyped)
identifier @racket[op-id], e.g.:

@racketblock[(define-primop typed+ + : (→ Int Int))]

When not specified, @racket[op-id] is @racket[typed-op-id] suffixed with
@litchar{-} (see @secref{racket-}).}

@; define-syntax-category -----------------------------------------------------
@defform*[((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 @def-stx-cat{type}, which in turn
defines the forms and functions below.

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

If no keys are specified, @racket[key1] is @litchar{:} and @racket[key2] is
@litchar{::}. If only @racket[key1] is given, then @racket[key2] is
@racket[key1] appended to itself.

Defining another category, e.g., @def-stx-cat{kind} defines a separate set of forms
and functions, e.g., @racket[define-kinded-syntax], @racket[define-base-kind], @racket[kind=?], etc.

@italic{The following forms and functions are automatically defined by a
@def-stx-cat{type} declaration:}
@(for/list ([x (in-list '(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))]
            [i (in-naturals)])
   (if (zero? i)
       (racket #,x)
       (list ", " (racket #,x))))

@; @item{@racket[define-typed-syntax], as described above. Uses
@; @racket[current-typecheck-relation] @racket[current-type-eval] for
@; typechecking, and uses @litchar{:} as the key when an explicit key is not specificed in type judgements.}


@; Forms for Defining Types --------------------------------------
@section/from-stx-cat{Forms for Defining Types}

@defform*[((define-base-type base-type-name-id option ...)
           (define-base-type base-type-name-id key tag option ...))
           #:grammar
           ([option (code:line #:runtime)])]{
   Defines a base type. @racket[(define-base-type τ)] in turn defines:
  @itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].}
            @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
            @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]}

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

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

@defform[(define-base-types base-type-name-id ...)]{
  Defines multiple base types, each using the default key and options.}

@defform[(define-type-constructor name-id option ...)
          #:grammar
         ([option (code:line #:arity op n)
                  (code:line #:runtime)
                  (code:line #:arg-variances expr)
                  (code:line #:extra-info stx)])]{
  Defines a type constructor (that does not bind type variables).
  Defining a type constructor @racket[τ] subsequently defines:
  @itemlist[

    @item{@racket[τ], a macro for constructing an instance of type @racket[τ],
          with the specified arity.  Validates inputs and expands to
          @racket[τ-], attaching @racket[#%type] at @tt{key2}.}

    @item{@racket[τ-], 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 @racket[define-internal-type-constructor].}

    @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
          @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type
          @racket[τ].}]

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

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

    The @racket[#: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 @racket[invariant], @racket[contravariant],
    @racket[covariant], and @racket[irrelevant].

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

    Example:

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

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

@defform[(define-binding-type name-id option ...)
          #:grammar
         ([option (code:line #:arity op n)
                  (code:line #:bvs op n)
                  (code:line #:arr kindcon)
                  (code:line #:arg-variances expr)
                  (code:line #:extra-info stx)])]{
    Similar to @racket[define-type-constructor], except
    @racket[define-binding-type] defines a type that binds type variables.
    Defining a type constructor @racket[τ] defines:

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

    The default @racket[#:arity] is @racket[= 1]
    and the default @racket[#:bvs] is @racket[>= 0].

    Use the @racket[#:arr] argument to define a type with kind annotations
    on the type variables. The @racket[#: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.}

@defform[(define-internal-type-constructor name-id option ...)
          #:grammar
         ([option (code:line #:arg-variances expr)
                  (code:line #:extra-info stx)])]{

  Like @racket[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.}}

@defform[(define-internal-binding-type name-id option ...)
          #:grammar
         ([option (code:line #:arr kindcon)
                    (code:line #:arg-variances expr)
                    (code:line #:extra-info stx)])]{
  Analogous to @racket[define-internal-type-constructor], but for binding types.}

@; --------------------------------------------------------



@; Type Operations --------------------------------------------------------
@section/from-stx-cat{Type Operations}

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

@defparam[current-type-eval type-eval (-> syntax? syntax?)]{
    A phase 1 parameter for controlling "type evaluation". A @racket[type-eval]
    function consumes and produces syntax. It is typically used to convert a type
    into a canonical representation. The @racket[(current-type-eval)] is called
    immediately before attaching a type to a syntax object, i.e., by
    @racket[assign-type].

    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.

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

@defparam[current-typecheck-relation type-cmp (-> type? type? boolean?)]{
    A phase 1 parameter for controlling type checking, used by
    @racket[define-typed-syntax]. A @racket[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 @racket[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.}

@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{
    A phase 1 function that calls @racket[current-typecheck-relation]. The first
    argument is the given type and the second is the expected type.}

@defproc[(typechecks? [τs1 (or/c (listof type?) (stx-listof type?))]
                [τs2 (or/c (listof type?) (stx-listof type?))]) boolean?]{
    Phase 1 function mapping @racket[typecheck?] over lists of types,
    pairwise. @racket[τs1] and @racket[τs2] must have the same length. The first
    list contains the given types and the second list contains the expected
    types.}

@defparam[current-type=? type-cmp (-> type? type? immutable-bound-id-table? immutable-bound-id-table? boolean?)]{
    A phase 1 parameter for customizing the behavior of @racket[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
    @racket[current-type=?] under a binding form, pass extended environments mapping the
    binders to a new unique value (compared by @racket[eq?]).
}

@defproc[(type=? [τ1 type?] [τ2 type?]) boolean?]{
    A phase 1 equality predicate for types that computes structural,
    @racket[free-identifier=?] equality, but includes alpha-equivalence.

@examples[#:eval the-eval
    (define-base-type Int)
    (define-base-type String)
    (begin-for-syntax (displayln (type=? #'Int #'Int)))
    (begin-for-syntax (displayln (type=? #'Int #'String)))
    (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)))))
    (begin-for-syntax
      (displayln
        (type=? ((current-type-eval) #'(∀ (X) (∀ (Y) (→ X Y))))
                ((current-type-eval) #'(∀ (Y) (∀ (X) (→ Y X)))))))
    (begin-for-syntax
      (displayln
        (type=? ((current-type-eval) #'(∀ (Y) (∀ (X) (→ Y X))))
                ((current-type-eval) #'(∀ (X) (∀ (X) (→ X X)))))))
]}

@defproc[(types=? [τs1 (listof type?)][τs2 (listof type?)]) boolean?]{
    A phase 1 predicate checking that @racket[τs1] and @racket[τs2] are equivalent, pairwise. Thus,
    @racket[τs1] and @racket[τs2] must have the same length.}

@defproc[(same-types? [τs (listof type?)]) boolean?]{
    A phase 1 predicate for checking if a list of types are all the same.}

@defproc[(type? [x syntax?]) boolean?]{
    A phase 1 predicate recognizing well-formed types. Checks that @racket[x] is
    a syntax object and has syntax propety @racket[#%type].}

@defparam[current-type? type-pred (-> syntax? boolean?)]{
    A phase 1 parameter, initialized to @racket[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.}

@defproc[(any-type? [x syntax?]) boolean?]{
    A phase 1 predicate recognizing valid types. Defaults to @racket[type?].}

@defparam[current-any-type? type-pred (-> syntax? boolean?)]{
    A phase 1 parameter, initialized to @racket[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 @racket[current-type?] would recognize types with only the "star" kind.}

@defproc[(assign-type [e syntax?] [τ type?]) syntax?]{
    Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches
    it to @racket[e] using @tt{key1}.}

@defproc[(typeof [e syntax?]) type?]{
    Phase 1 function returning type of @racket[e], at @tt{key1}.}

@defidform[#%type]{The default "kind" used to validate types.}
@defproc[(#%type? [x any/c]) boolean?]{Phase 1 predicate recognizing @racket[#%type].}

@defproc[(mk-type [stx syntax?]) type?]{
    Phase 1 function that marks a syntax object as a type by attaching @racket[#%type].
    Useful for defining your own type with arbitrary syntax that does not fit with
    @racket[define-base-type] or @racket[define-type-constructor].}


@; ---------------------------------------------------
@section{Syntax Patterns}
@; ~typecheck ---------------------------------------------
@defform[(~typecheck premise ...)]{
A @racket[syntax-parse] @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
that supports typechecking syntax.

For example the pattern

@racketblock[
  (~typecheck
   [⊢ a ≫ a- ⇒ τ_a]
   [⊢ b ≫ b- ⇐ τ_a])]

typechecks @racket[a] and @racket[b], expecting @racket[b] to have the
type of @racket[a], and binding @racket[a-] and @racket[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.

@(let ([ev (make-base-eval)])
   (ev '(require turnstile))
   @examples[
     #:eval ev
     (begin-for-syntax
       (struct clause [stx- result-type])
       (code:comment "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)])))
     ])}

@; ~⊢ ---------------------------------------------
@defform*[[(~⊢ tc ...)]]{
A shorthand @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
for @racket[(~typcheck [⊢ tc ...])].

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

@(let ([ev (make-base-eval)])
   (ev '(require turnstile))
   @examples[
     #:eval ev
     (begin-for-syntax
       (struct clause [stx- result-type])
       (code:comment "f : Stx -> Clause")
       (define (f stx)
         (syntax-parse stx
           [(~and [condition:expr body:expr]
                  (~⊢ condition ≫ condition- ⇐ Bool)
                  (~⊢ body ≫ body- ⇒ τ_body))
            (clause #'[condition- body-] #'τ_body)])))
     ])}


@; syntax classes ---------------------------------
@section/from-stx-cat{Syntax Classes}

@defstxclass[type]{A syntax class that calls @racket[current-type?]
  to validate well-formed types. Binds a @racket[norm] attribute to the type's expanded representation.}
@defstxclass[any-type]{A syntax class that calls @racket[current-any-type?]
  to validate types. Binds a @racket[norm] attribute to the type's expanded representation.}
@defstxclass[type-bind]{A syntax class recognizing syntax objects with
  shape @racket[[x:id (~datum :) τ:type]]. Binds a @racket[x] attribute to the binding identifier,
  and a @racket[type] attribute to the type's expanded representation.}
@defstxclass[type-ctx]{A syntax class recognizing syntax objects with
  shape @racket[(b:type-bind ...)]. Binds a @racket[x] attribute to the binding identifiers,
  and a @racket[type] attribute to the expanded representation of the types.}
@defstxclass[type-ann]{A syntax class recognizing
  syntax objects with shape @racket[{τ:type}] where the braces are required.
  Binds a @racket[norm] attribute to the type's expanded representation.}


@; require and provide-related forms --------------------
@section{@racket[require] and @racket[provide]-related Forms}

@defform[(type-out ty-id ...)]{
A @racket[provide]-spec that, for each given @racket[ty-id], provides @racket[ty-id],
and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-expander @racket[~ty-id].}

@bold{Note: } @racket[type-out] is generated by @def-stx-cat{type}.
See @racket[define-syntax-category] for more information.

@defform[(typed-out x+ty+maybe-rename ...)
         #:grammar
         ([x+ty+maybe-rename
          (code:line [x ty])
           (code:line [x : ty])
           (code:line [[x ty] out-x])
           (code:line [[x : ty] out-x])]
          [x identifier?]
          [out-x identifier?]
          [ty type?])]{
A provide-spec that adds type @racket[ty] to untyped @racket[x] and provides
that typed identifier as either @racket[x], or @racket[out-x] if it's specified.

Equivalent to a @racket[define-primop] that automatically provides its
definition.}

@defform[(extends base-lang option ...)
           #:grammar
         ([option (code:line #:except id ...)
                  (code:line #:rename [old new] ...)])]{
Requires all forms from @racket[base-lang] and reexports them. Tries to
 automatically handle conflicts for commonly used forms like @racket[#%app].
The imported names are available for use in the current module, with a
 @tt{base-lang:} prefix.}
@defform[(reuse name ... #:from base-lang)
         #:grammar
         ([name id
                [old new]])]{
Reuses @racket[name]s from @racket[base-lang].}

@; Sec: Suffixed Racket bindings ----------------------------------------------
@section[#:tag "racket-"]{Suffixed Racket Bindings}

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

@; Sec: turnstile/lang ----------------------------------------------
@section[#:tag "turnstilelang"]{@hash-lang[] @racketmodname[turnstile]/lang}

Deprecated: see @secref{turnstilequicklang}.

@; Sec: turnstile/quicklang ----------------------------------------------
@section[#:tag "turnstilequicklang"]{@hash-lang[] @racketmodname[turnstile]/quicklang}

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

For convenience, Turnstile additionally supplies @hash-lang[]
@racketmodname[turnstile]@tt{/quicklang}. Languages implemented using this language
will automatically provide Racket's @racket[#%module-begin],
@racket[#%top-interaction], @racket[#%top], @racket[require],
and some require transformers, e.g., @racket[rename-in].

@; Sec: turnstile/base ----------------------------------------------
@section[#:tag "turnstilebase"]{@hash-lang[] @racketmodname[turnstile]/base}

Only provides @racketmodname[racket/base] at phase 1.
Does not provide @racketmodname[syntax/parse] at phase 1.

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

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

@; Sec: Lower-level functions -------------------------------------------------
@section{Lower-level Functions}

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

@defproc[(infer [es (listof expr-stx)]
                [#:ctx ctx (listof binding-stx) null]
                [#:tvctx tvctx (listof tyvar-binding-stx) null]
                [#:tag tag symbol? ':]
                [#:stop-list? stop-list? boolean? #t])
                (list tvs xs es τs)]{

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.

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

might return

@racket[(list #'() #'(x-) #'((#%plain-app + x- 1)) #'(Int))].

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

Use the @tt{tag} keyword argument to specify the key for the
returned "type". The default key is @litchar{:}. For example, a programmer may
want to specify a @litchar{::} key when using @racket[infer] to compute the
kinds on types.}

The @racket[#:stop-list?] argument controls an optimization to avoid unnecessary
re-expansion. When @racket[#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 @racket[#f] when @racket[infer] is used to infer kinds.

@defparam[current-use-stop-list? flag boolean? #:value #t]{
An additional means to control the stop-list optimization. Set to @racket[#f] to disable.
Useful for languages with features like dependent types where full expansion is always
needed.
}

@defproc[(subst [τ syntax?]
                [x identifier?]
                [e syntax?]
                [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{
Phase 1 function that replaces occurrences of @racket[x], as determined by @racket[cmp], with
 @racket[τ] in @racket[e].}

@defproc[(substs [τs (listof syntax?)]
                 [xs (listof identifier?)]
                 [e syntax?]
                 [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{
Phase 1 function folding @racket[subst] over the given @racket[τs] and @racket[xs].}

@defform[(type-error #:src srx-stx #:msg msg args ...)]{
Phase 1 form that throws a type error using the specified information. @racket[msg] is a format string that references @racket[args].}

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

@(let ([ev (make-base-eval)])
   (ev '(require turnstile))
   (ev '(define-base-type Int))
   (ev '(define-type-constructor → #:arity = 2))
   @examples[#:eval ev
     (begin-for-syntax
       (define t ((current-type-eval) #'(→ Int Int)))
       (displayln (type->str t)))])
}

@deftogether[(@defproc[(add-orig [e syntax?] [orig syntax?]) syntax?]
              @defproc[(get-orig [e syntax?]) syntax?])]{
Phase 1 functions for manipulation the @racket['orig] property. @racket[add-orig] returns
the syntax @racket[_e] with @racket[_orig] added. @racket[get-orig] returns the last added
@racket['orig] on @racket[_e], or returns itself if none were added.
}

@section{Subtyping}

WARNING: very experimental

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

@defproc[(variance? [v any/c]) boolean?]{
 Predicate that recognizes the variance values.}

@deftogether[(
  @defthing[covariant variance?]
  @defthing[contravariant variance?]
  @defthing[invariant variance?]
  @defthing[irrelevant variance?])]{
The different possible variances.
}


@section{Modes}

WARNING: experimental

@defmodule[turnstile/mode #:use-sources (turnstile/mode)]
@(define mode-ev
   (let ([ev (make-base-eval)])
     (ev '(require turnstile/mode))
     ev))

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

@defstruct*[mode ([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 @racket[mode].
}

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

@defparam[current-mode mode mode? #:value (make-mode)]{
  A parameter that holds the current mode. Typically parameterized using the keywords
  @racket[#:mode] and @racket[#:submode] from @racket[define-typed-syntax] forms.
}

@defform[(with-mode mode-expr body ...+)
         #:contracts ([mode-expr mode?])]{
  The result of @racket[with-mode] is the result of the last @racket[_body].
  The parameter @racket[current-mode] is assigned to the result of
  @racket[_mode-expr] for the extent of the @racket[_body] expressions. The
  function @racket[mode-setup-fn] is called on the result of
  @racket[_mode-expr] before @racket[current-mode] is set, and the function
  @racket[mode-teardown-fn] is called after @racket[current-mode] is restored
  to its previous value.

  @examples[#:eval mode-ev
    (define-struct (my-mode mode) ())
    (define M (make-my-mode (λ () (displayln "M setup"))
                            (λ () (displayln "M teardown"))))
    (with-mode M
      (displayln (current-mode)))]}

@defproc[(make-param-mode [param parameter?] [value any/c]) mode?]{
  Creates a @racket[mode] that assigns the given parameter to the given
  value for the extent of the mode.

  @examples[#:eval mode-ev
    (define current-scope (make-parameter 'outer))
    (with-mode (make-param-mode current-scope 'inner)
      (displayln (current-scope)))]}


@section{Miscellaneous Syntax Object Functions}

These are all phase 1 functions.

@defproc[(stx-length [stx syntax?]) exact-nonnegative-integer?]{Analogous to @racket[length].}
@defproc[(stx-length=? [stx1 syntax?] [stx2 syntax?]) boolean?]{
 Returns true if two syntax objects are of equal length.}
@defproc[(stx-andmap [p? (-> syntax? boolean?)] [stx syntax?]) (listof syntax?)]{
Analogous to @racket[andmap].}

@section{Special Identifiers}

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

@defidform[⇐]{This and the following ids throw a syntax error when used in an invalid context.}
@defidform[⇒]{}
@defidform[≫]{}
@defidform[≻]{}
@defidform[⊢]{}

@section[#:tag "no-unicode"]{Non-Unicode Identifiers}

@defmodule[turnstile/no-unicode #:use-sources (turnstile/no-unicode)]

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

@defidform[<=]{Alias for @racket[⇐].}
@defidform[=>]{Alias for @racket[⇒].}
@defidform[>>]{Alias for @racket[≫].}
@defidform[>>>]{Alias for @racket[≻].}
@defidform[/-]{Alias for @racket[⊢].}
