On this page:
The turnstile language
8.12

The turnstile language🔗ℹ

Stephen Chang <stchang at racket-lang dot org>,
Alex Knauth <alexander at knauth dot org>,
Ben Greenman <types at ccs dot neu dot edu>,
Milo Turner <iitalics at gmail dot com>,
and Michael Ballantyne <mballantyne at ccs dot neu dot edu>

 #lang turnstile package: turnstile-lib

Turnstile aims to help Racket programmers create typed languages. It does so with extensions of Racket’s macro-definition forms that facilitate implementation of type rules alongside normal macro code. As a result, the macros implementing a new language directly type check the program during expansion, obviating the need to create and call out to a separate type checker. Thus, a complete typed language implementation remains a series of macro definitions that may be imported and exported in the standard way that Racket programmers are accustomed to.

    1 The Turnstile Guide

      1.1 A New Type Judgement

      1.2 define-typed-syntax

        1.2.1 Type rules vs define-typed-syntax

        1.2.2 define-typed-syntax premises

        1.2.3 syntax-parse directives as premises

      1.3 Defining Types

      1.4 Defining Rules

      1.5 Defining Primitive Operations (Primops)

      1.6 A Complete Language

      1.7 Extending a Language

    2 The Turnstile Reference

      2.1 Typing Unicode Characters

      2.2 Forms

      2.3 Forms for Defining Types

      2.4 Type Operations

      2.5 Syntax Patterns

      2.6 Syntax Classes

      2.7 require and provide-related Forms

      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

      2.13 Subtyping

      2.14 Modes

      2.15 Miscellaneous Syntax Object Functions

      2.16 Special Identifiers

      2.17 Non-Unicode Identifiers

    3 Rackunit-Style Test Forms for Turnstile

      3.1 Expression Test Forms

      3.2 Top-Level Test Forms

      3.3 Other Debugging Forms

    Bibliography