1 The Turnstile Guide🔗ℹ

This guide introduces Turnstile with the implementation of a simply-typed core language. It then reuses the simply-typed language implementation to implement a language with subtyping.

1.1 A New Type Judgement🔗ℹ

For example, here are some rules that check and rewrite simply-typed lambda-calculus terms to the untyped lambda-calculus.

1.2 define-typed-syntax🔗ℹ

Here are implementations of the above rules using Turnstile (we extended the forms to define multi-arity functions):

Initial function and application definitions

; [LAM]

(define-typed-syntax (λ ([x:id : τ_in:type] ...) e) ≫

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

-------

[⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)])

; [APP]

(define-typed-syntax (#%app e_fn e_arg ...) ≫

[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]

[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...

--------

[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])

The define-typed-syntax form resembles a conventional Racket macro definition: the above rules begin with an input pattern, where the leftmost identifier is the name of the macro, which is followed by a series of premises that specify side conditions and bind local pattern variables, and concludes with an output syntax template.

1.2.1 Type rules vs define-typed-syntax🔗ℹ

The define-typed-syntax form extends typical Racket macros by interleaving type checking computations, possibly written using a type judgement syntax, directly into the macro definition.

Compared to the type rules in the A New Type Judgement section, Turnstile define-typed-syntax definitions differ in a few ways:

• Each premise and conclusion must be enclosed in brackets.

• A conclusion is "split" into its inputs (at the top) and outputs (at the bottom) to resemble other Racket macro-definition forms. In other words, pattern variable scope flows top-to-bottom, enabling the programmers to read the code more easily.

  For example, the input part of the [LAM] rule’s conclusion corresponds to the (λ ([x:id : τ_in:type] ...) e) pattern and the output part corresponds to the (λ- (x- ...) e-) and (→ τ_in.norm ... τ_out) templates. A ≫ delimiter separates the input pattern from the premises while ⇒ in the conclusion associates the type with the output expression.

• The define-typed-syntax definitions do not thread through an explicit type environment Γ. Rather, Turnstile reuses Racket’s lexical scope as the type environment and programmers should only write new type environment bindings to the left of the ⊢, analogous to let.

• Since type environments obey lexical scope, an explicit implementation of the [VAR] rule is unneeded.

1.2.2 define-typed-syntax premises🔗ℹ

Like their type rule counterparts, a define-typed-syntax definition supports two [bidirectional]-style type checking judgements in its premises.

A [⊢ e ≫ e- ⇒ τ] judgement expands expression e, binds its expanded form to e-, and its type to τ. In other words, e is an input syntax template, and e- and τ are output patterns.

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

For example, in the definition of #%app from section define-typed-syntax, the first premise, [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)], expands function e_fn, binds it to pattern variable e_fn-, and binds its input types to (τ_in ...) and its output type to τ_out. Macro expansion stops with a type error if e_fn does not have a function type.

The second #%app premise then uses the ⇐ to check that the given inputs have types that match the expected types. Again, a type error is reported if the types do not match.

The λ definition from that section also utilizes a ⇒ premise, except it must add bindings to the type environment, which are written to the left of the ⊢. The lambda body is then type checked in this context.

Observe how ellipses may be used in exactly the same manner as other Racket macros. (The norm attribute comes from the type syntax class and is bound to the expanded representation of the type. This is used to avoid double-expansions of the types.)

1.2.3 syntax-parse directives as premises🔗ℹ

A define-typed-syntax definition may also use syntax-parse options and pattern directives in its premises. Here is a modified #%app that reports a more precise error for an arity mismatch:

Function application with a better error message

; [APP]

(define-typed-syntax (#%app e_fn e_arg ...) ≫

[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]

#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])

(format "arity mismatch, expected ~a args, given ~a"

(stx-length #'[τ_in ...]) #'[e_arg ...])

[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...

--------

[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])

1.3 Defining Types🔗ℹ

The rules from section define-typed-syntax require a function type constructor. Turnstile includes convenient forms for defining such type constructors, e.g. define-type-constructor:

The function type

(define-type-constructor → #:arity > 0)

The define-type-constructor declaration defines the → function type as a macro that takes at least one argument, along with a ~→ pattern expander matching on that type in syntax patterns.

1.4 Defining ⇐ Rules🔗ℹ

The rules from from A New Type Judgement are incomplete. Specifically, ⇐ clauses appear in the premises but never in the conclusion.

To complete the rules, we can add a general ⇐ rule (sometimes called a subsumption rule) that dispatches to the appropriate ⇒ rule:

Similarly, Turnstile uses an implicit ⇐ rule so programmers need not specify a ⇐ variant of every rule. If a programmer writes an explicit ⇐ rule, then it is used instead of the default. Writing an explicit ⇐ rule is useful for implementing (local) type inference or type annotations. Here is an extended lambda that adds a ⇐ clause.

lambda with inference, and ann

; [LAM]

(define-typed-syntax λ #:datum-literals (:)

; ⇒ rule (as before)

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

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

-------

[⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]

; ⇐ rule (new)

[(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫

[[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]

---------

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

(define-typed-syntax (ann e (~datum :) τ:type) ≫

[⊢ e ≫ e- ⇐ τ.norm]

--------

[⊢ e- ⇒ τ.norm])

This revised lambda definition uses an alternate, multi-clause define-typed-syntax syntax, analogous to syntax-parse (whereas the simpler syntax from section 1.2 resembles define-simple-macro).

The first clause is the same as before. The second clause has an additional input type pattern and the clause matches only if both patterns match, indicating that the type of the expression can be inferred. Observe that the second lambda clause’s input parameters have no type annotations. Since the lambda body’s type is already known, the premise in the second clause uses the ⇐ arrow. Finally, the conclusion specifies only the expanded syntax object because the input type is automatically attached to that output.

We also define an annotation form ann, which invokes the ⇐ clause of a type rule.

1.5 Defining Primitive Operations (Primops)🔗ℹ

The previous sections have defined type rules for #%app and λ, as well as a function type, but we cannot write any well-typed programs yet since there are no base types. Let’s fix that:

defining a base type, literal, and primop

(define-base-type Int)

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

(define-typed-syntax #%datum

[(_ . n:integer) ≫

--------

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

[(_ . x) ≫

--------

[#:error (type-error #:src #'x

#:msg "Unsupported literal: ~v" #'x)]])

The code above defines a base type Int, and attaches type information to both + and integer literals.

define-primop creates an identifier macro that attaches the specified type to the specified identifier. When only one identifier is specified, it is used as both the name of the typed operation, and appended with a "-" suffix and (that corresponding Racket function is) used as the macro output. Alternatively, a programmer may explicitly specify separate surface and target identifiers (see define-primop in the reference).

1.6 A Complete Language🔗ℹ

We can now write well-typed programs! Here is the complete language implementation, with some examples:

Languages implemented using #lang turnstile must additionally provide #%module-begin and other forms required by Racket. Use #lang turnstile/lang to automatically provide some default forms. See the section on #lang turnstile/lang for more details.

"STLC"

#lang turnstile

(provide → Int λ #%app #%datum + ann)

(define-base-type Int)

(define-type-constructor → #:arity > 0)

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

; [APP]

(define-typed-syntax (#%app e_fn e_arg ...) ≫

[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]

#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])

(format "arity mismatch, expected ~a args, given ~a"

(stx-length #'[τ_in ...]) #'[e_arg ...])

[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...

--------

[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])

; [LAM]

(define-typed-syntax λ #:datum-literals (:)

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

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

-------

[⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]

[(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫

[[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]

---------

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

; [ANN]

(define-typed-syntax (ann e (~datum :) τ:type) ≫

[⊢ e ≫ e- ⇐ τ.norm]

--------

[⊢ e- ⇒ τ.norm])

; [DATUM]

(define-typed-syntax #%datum

[(_ . n:integer) ≫

--------

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

[(_ . x) ≫

--------

[#:error (type-error #:src #'x

#:msg "Unsupported literal: ~v" #'x)]])

1.7 Extending a Language🔗ℹ

Since the STLC language from A Complete Language is implemented as just a series of macros, like any other Racket #lang, its forms may be imported and exported and may be easily reused in other languages. Let’s see how we can reuse the above implementation to implement a subtyping language.

"STLC+SUB"

#lang turnstile

(extends STLC #:except #%datum +)

(provide Top Num Nat + add1 #%datum if)

(define-base-types Top Num Nat)

(define-primop + : (→ Num Num Num))

(define-primop add1 : (→ Int Int))

(define-typed-syntax #%datum

[(_ . n:nat) ≫

--------

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

[(_ . n:integer) ≫

--------

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

[(_ . n:number) ≫

--------

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

[(_ . x) ≫

--------

[≻ (STLC:#%datum . x)]])

(begin-for-syntax

(define (sub? t1 t2)

; need this because recursive calls made with unexpanded types

(define τ1 ((current-type-eval) t1))

(define τ2 ((current-type-eval) t2))

(or ((current-type=?) τ1 τ2)

(Top? τ2)

(syntax-parse (list τ1 τ2)

[(_ ~Num) ((current-sub?) τ1 #'Int)]

[(_ ~Int) ((current-sub?) τ1 #'Nat)]

[((~→ τi1 ... τo1) (~→ τi2 ... τo2))

(and (subs? #'(τi2 ...) #'(τi1 ...))

((current-sub?) #'τo1 #'τo2))]

[_ #f])))

(define current-sub? (make-parameter sub?))

(current-typecheck-relation sub?)

(define (subs? τs1 τs2)

(and (stx-length=? τs1 τs2)

(stx-andmap (current-sub?) τs1 τs2)))

(define (join t1 t2)

(cond

[((current-sub?) t1 t2) t2]

[((current-sub?) t2 t1) t1]

[else #'Top]))

(define current-join (make-parameter join)))

; [IF]

(define-typed-syntax (if e_tst e1 e2) ≫

[⊢ e_tst ≫ e_tst- ⇒ _] ; a non-false value is truthy

[⊢ e1 ≫ e1- ⇒ τ1]

[⊢ e2 ≫ e2- ⇒ τ2]

--------

[⊢ (if- e_tst- e1- e2-) ⇒ #,((current-join) #'τ1 #'τ2)])

This language uses subtyping instead of type equality as its "typecheck relation". Specifically, the language defines a sub? function and sets it as the current-typecheck-relation. Thus it is able to reuse the λ and #%app rules from the previous sections without modification. The extends clause is useful for declaring this. It automatically requires and provides the previous rules and re-exports them with the new language.

The new language does not reuse #%datum and +, however, since subtyping requires updates these forms. Specifically, the new language defines a hierarchy of numeric base types, gives + a more general type, and redefines #%datum to assign more precise types to numeric literals. Observe that #%datum dispatches to STLC’s datum in the "else" clause, using the ≻ conclusion form, which dispatches to another (typed) macro. In this manner, the new typed language may still define and invoke macros like any other Racket program.

Since the new language uses subtyping, it also defines a (naive) join function, which is needed by conditional forms like if. The if definition uses the current-join parameter, to make it reusable by other languages. Observe that the output type in the if definition uses unquote. In general, all syntax template positions in Turnstile are quasisyntaxes.