The turnstile language

7.7

top ← prev up next →

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