www

guide.scrbl (19778B)

---

 #lang scribble/manual
 
 @(require scribble/example racket/sandbox
           (for-label racket/base
                      (except-in turnstile/turnstile ⊢ mk-~ mk-?))
           "doc-utils.rkt" "common.rkt")
 
 @title{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.
 
 @section[#:tag "judgements"]{A New Type Judgement}
 
 Turnstile's syntax borrows from that of conventional type
 judgements. Specifically, programmers may implement typed languages using a
 declarative syntax that interleaves program rewriting (i.e., macro expansion)
 and type checking. These new rules rely on two core
 @cite{bidirectional} judgements:
 @itemlist[#:style 'ordered
           @item{@verbatim|{Γ ⊢ e ≫ e- ⇒ τ}|
            reads: "In context Γ, @racket[e] expands to @racket[e-] and has type
            τ."}
           @item{@verbatim|{Γ ⊢ e ≫ e- ⇐ τ}|
            reads: "In context Γ, @racket[e] expands to @racket[e-] and must
            have type τ."
 
            The key difference is that τ is an output in the first relation and
            an input in the second relation.
 
            As will be shown below, these input and output positions
            conveniently correspond to @tech:stx-pats and @tech:stx-templates,
            respectively.}]
 
 For example, here are some rules that check and rewrite simply-typed
 lambda-calculus terms to the untyped lambda-calculus.
 
 @verbatim|{
       [x ≫ x- : τ] ∈ Γ
 [VAR] -----------------
       Γ ⊢ x ≫ x- ⇒ τ
            
       Γ,[x ≫ x- : τ1] ⊢ e ≫ e- ⇒ τ2
 [LAM] -------------------------------
       Γ ⊢ λx:τ1.e ≫ λx-.e- ⇒ τ1 → τ2
 
       Γ ⊢ e1 ≫ e1- ⇒ τ1 → τ2
       Γ ⊢ e2 ≫ e2- ⇐ τ1
 [APP] -------------------------
       Γ ⊢ e1 e2 ≫ e1- e2- ⇒ τ2
 }|
 
 @; Sec: define-typed-syntax ---------------------------------------------------
 @section[#:tag "define-typed-syntax"]{@racket[define-typed-syntax]}
 
 Here are implementations of the above rules using Turnstile 
 (we extended the forms to define multi-arity functions):
 
 @label-code["Initial function and application definitions"
 @#reader scribble/comment-reader
 (racketblock0
 ;; [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 above code assumes some existing bindings:
 @itemlist[
  @item{@racket[→], a programmer-defined (or imported) type constructor, 
   see @secref{tycon};}
  @item{@racket[~→], a @tech:pat-expander associated with the @racket[→] type
   constructor;}
  @item{@racket[type], a @tech:stx-class for recognizing valid types that is 
   pre-defined by Turnstile;}
  @item{and core Racket forms suffixed with @litchar{-}, for example
   @racket[λ-], that are also predefined by Turnstile.}
  ]
 
 The @racket[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 @|tech:stx-template|.
 
 More specifically, @racket[define-typed-syntax] is roughly an extension of 
 @racket[define-syntax-parser] in that:
 @itemlist[
  @item{a programmer may specify @racket[syntax-parse]
   options, e.g., @racket[#:datum-literals];}
  @item{pattern positions may use any @racket[syntax-parse] combinators, e.g. 
   @racket[~and], @racket[~seq], or custom-defined @tech:pat-expanders;}
  @item{and the premises may be interleaved with @racket[syntax-parse]
   @tech:pat-directives, e.g., @racket[#:with] or @racket[#:when].}]
 
 @; Subsec: Type rules vs define-typed-syntax ----------------------------------
 @subsection{Type rules vs @racket[define-typed-syntax]}
 
 The @racket[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 @secref{judgements} section, Turnstile
 @racket[define-typed-syntax] definitions differ in a few ways:
 
 @itemlist[ @item{Each premise and conclusion must be enclosed in brackets.}
 
 @item{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
 @racket[(λ ([x:id : τ_in:type] ...) e)] pattern and the output part
 corresponds to the @racket[(λ- (x- ...) e-)] and @racket[(→ τ_in.norm
 ... τ_out)] templates. A @racket[≫] delimiter separates the input pattern
 from the premises while @racket[⇒] in the conclusion associates the type
 with the output expression.}
 
  @item{The @racket[define-typed-syntax] definitions do not thread through an
 explicit type environment @racket[Γ].  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 @racket[⊢], analogous to
 @racket[let].}
 
  @item{Since type environments obey lexical scope, an explicit implementation of
   the @tt{[VAR]} rule is unneeded.}]
 
 @; Subsec: define-typed-syntax premises ---------------------------------------
 @subsection{@racket[define-typed-syntax] premises}
 
 Like their type rule counterparts, a @racket[define-typed-syntax] definition
 supports two @cite{bidirectional}-style type checking judgements in its
 premises.
 
 A @racket[[⊢ e ≫ e- ⇒ τ]] judgement expands expression @racket[e], binds its
 expanded form to @racket[e-], and its type to @racket[τ]. In other words, 
 @racket[e] is an input syntax template, and @racket[e-] and @racket[τ] are
 output patterns.
 
 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).
 
 For example, in the definition of @code{#%app} from section
 @secref{define-typed-syntax}, the first premise, @racket[[⊢ e_fn ≫ e_fn- ⇒ (~→
 τ_in ... τ_out)]], expands function @racket[e_fn], binds it to pattern variable
 @racket[e_fn-], and binds its input types to @racket[(τ_in ...)] and its output
 type to @racket[τ_out]. Macro expansion stops with a type error if
 @racket[e_fn] does not have a function type.
 
 The second @racket[#%app] premise then uses the @racket[⇐] 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 @racket[λ] definition from that section also utilizes a @racket[⇒] premise,
 except it must add bindings to the type environment, which are written to the
 left of the @racket[⊢]. 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 @racket[norm] @tech:attribute comes from the
 @racket[type] syntax class and is bound to the expanded representation of the
 type. This is used to avoid double-expansions of the types.)
 
 @; Subsec: syntax-parse directives as premises --------------------------------
 @subsection{@racket[syntax-parse] directives as premises}
 
 A @racket[define-typed-syntax] definition may also use @racket[syntax-parse]
 options and @|tech:pat-directives| in its premises. Here is a modified
 @racket[#%app] that reports a more precise error for an arity mismatch:
 
 @label-code["Function application with a better error message" @#reader
 scribble/comment-reader
 (racketblock0
 ;; [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]))]
 
 @; Sec: Defining Types --------------------------------------------------------
 @section[#:tag "tycon"]{Defining Types}
 
 The rules from section @secref{define-typed-syntax} require a function type
 constructor. Turnstile includes convenient forms for defining such type
 constructors, e.g. @racket[define-type-constructor]:
 
 @label-code["The function type"
 (racketblock0
  (define-type-constructor → #:arity > 0))]
 
 The @racket[define-type-constructor] declaration defines the @racket[→]
 function type as a macro that takes at least one argument, along with a
 @racket[~→] @tech:pat-expander matching on that type in @|tech:stx-pats|.
 
 @; Sec: Defining check rules---------------------------------------------------
 @section{Defining @racket[⇐] Rules}
 
 The rules from from @secref{judgements} are incomplete. Specifically,
 @\racket[⇐] clauses appear in the premises but never in the conclusion.
 
 To complete the rules, we can add a general @racket[⇐] rule (sometimes called a
 subsumption rule) that dispatches to the appropriate @racket[⇒] rule:
 
 @verbatim|{
        Γ ⊢ e ≫ e- ⇒ τ2
        τ1 = τ2
 [FLIP] -----------------
        Γ ⊢ e ≫ e- ⇐ τ1
 }|
 
 Similarly, Turnstile uses an implicit @racket[⇐] rule so programmers need not
 specify a @racket[⇐] variant of every rule. If a programmer writes an explicit
 @racket[⇐] rule, then it is used instead of the default. Writing an explicit
 @racket[⇐] rule is useful for implementing (local) type inference or type
 annotations. Here is an extended lambda that adds a
 @racket[⇐] clause.
 
 @label-code["lambda with inference, and ann"
 @#reader scribble/comment-reader
 (racketblock0
 ;; [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 
 @racket[define-typed-syntax] syntax, analogous to @racket[syntax-parse] (whereas
 @seclink["define-typed-syntax"]{the simpler syntax from section 1.2} resembles
 @racket[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 
 @racket[⇐] 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 @racket[ann], which invokes the @racket[⇐]
 clause of a type rule.
 
 @; Sec: Defining primitive ops ------------------------------------------------
 @section{Defining Primitive Operations (Primops)}
 
 The previous sections have defined type rules for @racket[#%app] and @racket[λ],
 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:
 
 @label-code["defining a base type, literal, and primop"
 @#reader scribble/comment-reader
 (racketblock0
 (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 @racket[Int], and attaches type information
 to both @racket[+] and integer literals.
 
 @racket[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 "@tt{-}"
 suffix and (that corresponding Racket function is) used as the macro
 output. Alternatively, a programmer may explicitly specify separate surface and
 target identifiers (see @racket[define-primop] in the reference).
 
 @; Sec: A Complete Language  --------------------------------------------------
 @section[#:tag "stlc"]{A Complete Language}
 
 We can now write well-typed programs! Here is the complete
 language implementation, with some examples:
 
 @margin-note{Languages implemented using @hash-lang[] @racketmodname[turnstile]
 must additionally provide @racket[#%module-begin] and other forms required by
 Racket. Use @hash-lang[] @racketmodname[turnstile]@tt{/lang} to automatically
 provide some default forms. See the section on @secref{turnstilelang} for more
 details.}
 
 @; using `racketmod` because `examples` doesnt work with provide
 @(racketmod0 #:file "STLC"
 turnstile
 (provide → Int λ #%app #%datum + ann)
 
 (define-base-type Int)
 (define-type-constructor → #:arity > 0)
  
 (define-primop + : (→ Int Int Int))
 
 (code:comment "[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])
  
 (code:comment "[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-)]])
 
 (code:comment "[ANN]")
 (define-typed-syntax (ann e (~datum :) τ:type) ≫
   [⊢ e ≫ e- ⇐ τ.norm]
   --------
   [⊢ e- ⇒ τ.norm])
 
 (code:comment "[DATUM]")
 (define-typed-syntax #%datum
   [(_ . n:integer) ≫
    --------
    [⊢ (#%datum- . n) ⇒ Int]]
   [(_ . x) ≫
    --------
    [#:error (type-error #:src #'x
                         #:msg "Unsupported literal: ~v" #'x)]]))
 
 @;TODO: how to run examples with the typeset code?
 @(define stlc-eval
   (parameterize ([sandbox-output 'string]
                  [sandbox-error-output 'string]
                  [sandbox-eval-limits #f])
     (make-base-eval #:lang 'turnstile/examples/stlc+lit)))
 
 @examples[#:eval stlc-eval #:label "STLC Examples:" #:no-inset
   1
   (eval:error "1")
   (+ 1 2)
   (eval:error (+ 1 (λ ([x : Int]) x)))
   (eval:error (λ (x) x))
   (ann (λ (x) x) : (→ Int Int))
   ((ann (λ (x) x) : (→ Int Int)) 1)
   (((λ ([f : (→ Int Int Int)]) 
       (λ ([x : Int][y : Int]) 
         (f x y))) 
     +) 
    1 2)
   ]
 
 
 @; Sec: Extending a Language  -------------------------------------------------
 @section[#:tag "stlcsub"]{Extending a Language}
 
 Since the @tt{STLC} language from @secref{stlc} is implemented as just a series
 of macros, like any other Racket @hash-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.
 
 @(racketmod0 #:file "STLC+SUB" #:escape UNSYNTAX
 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)
     (code:comment "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)))
 
 (code:comment "[IF]")
 (define-typed-syntax (if e_tst e1 e2) ≫
   [⊢ e_tst ≫ e_tst- ⇒ _] (code:comment "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 @racket[sub?] function
 and sets it as the @racket[current-typecheck-relation]. Thus it is able to reuse
 the @racket[λ] and @racket[#%app] rules from the previous sections without
 modification. The @racket[extends] clause is useful for declaring this. It
 automatically @racket[require]s and @racket[provide]s the previous rules and
 re-exports them with the new language.
 
 The new language does not reuse @racket[#%datum] and @racket[+], however, since
 subtyping requires updates these forms. Specifically, the new language defines
 a hierarchy of numeric base types, gives @racket[+] a more general type, and
 redefines @racket[#%datum] to assign more precise types to numeric literals.
 Observe that @racket[#%datum] dispatches to @tt{STLC}'s datum in the "else"
 clause, using the @racket[≻] 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) @racket[join]
 function, which is needed by conditional forms like @racket[if]. The 
 @racket[if] definition uses the @racket[current-join] parameter, to
 make it reusable by other languages. Observe that the output type in the 
 @racket[if] definition uses @racket[unquote]. In general, all @tech:stx-template
 positions in Turnstile are @racket[quasisyntax]es.
 
 @(define stlc+sub-eval
   (parameterize ([sandbox-output 'string]
                  [sandbox-error-output 'string]
                  [sandbox-eval-limits #f])
     (make-base-eval #:lang 'turnstile/examples/stlc+sub)))
 
 @examples[#:eval stlc+sub-eval #:label "STLC+SUB Examples:" #:no-inset
  ((λ ([x : Top]) x) -1)
  ((λ ([x : Num]) x) -1)
  ((λ ([x : Int]) x) -1)
  (eval:error ((λ ([x : Nat]) x) -1))
  ((λ ([f : (→ Int Int)]) (f -1)) add1)
  ((λ ([f : (→ Nat Int)]) (f 1)) add1)
  (eval:error ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
  ((λ ([f : (→ Nat Num)]) (f 1)) add1)
  (eval:error ((λ ([f : (→ Int Nat)]) (f 1)) add1))
  (eval:error ((λ ([f : (→ Int Int)]) (f 1.1)) add1))
   ]