From e68480f0e6f030f174a1c1229281c633c4044b5a Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 23 Sep 2016 14:14:53 -0400 Subject: [PATCH] docs: reference rough draft --- turnstile/scribblings/reference.scrbl | 176 ++++++++++++++++++++++---- 1 file changed, 150 insertions(+), 26 deletions(-) diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index c6fa94a..b7d4728 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -6,6 +6,8 @@ @title{Reference} +@section{Forms} + To type some of these unicode characters in DrRacket, type the following and then hit Control-@litchar{\}. @@ -17,51 +19,173 @@ the following and then hit Control-@litchar{\}. @item{@litchar{\succ} → @litchar{≻}} ] -@defform[ +@defform*[ #:literals (≫ ⊢ ⇒ ⇐ ≻ : --------) - (define-typed-syntax name-id option ... rule) + ((define-typed-syntax (name-id . pattern) ≫ + premise ... + -------- + conclusion) + (define-typed-syntax name-id option ... rule ...+)) #:grammar - ([option syntax-parse-option] + ([option (code:line @#,racket[syntax-parse] option)] [rule [pattern ≫ premise ... -------- conclusion] + [pattern ⇐ expected-type ≫ + premise + ... + -------- + ⇐-conclusion] [pattern ⇐ : expected-type ≫ premise ... -------- ⇐-conclusion]] + [pattern (code:line @#,racket[syntax-parse] @#,tech{syntax pattern})] [premise (code:line [⊢ inf ...] ooo ...) (code:line [ctx ⊢ inf ...] ooo ...) + (code:line [ctx-elem ... ⊢ inf ...] ooo ...) (code:line [ctx ctx ⊢ inf ...] ooo ...) - (code:line [type-template τ⊑ type-template #:for expr-template]) - (code:line [type-template τ⊑ type-template #:for expr-template] ooo)] + (code:line [⊢ . inf-elem] ooo ...) + (code:line [ctx ⊢ . inf-elem] ooo ...) + (code:line [ctx-elem ... ⊢ . inf-elem] ooo ...) + (code:line [ctx ctx ⊢ . inf-elem] ooo ...) + type-relation + (code:line @#,racket[syntax-parse] @#,tech{pattern directive})] [ctx (ctx-elem ...)] - [ctx-elem [id ≫ id : type-template] - [id ≫ id : type-template] ooo] - [inf (code:line [expr-template ≫ pattern ⇒ type-pattern] ooo ...) - (code:line [expr-template ≫ pattern ⇐ type-pattern] ooo ...)] - [conclusion [⊢ [_ ≫ expr-template ⇒ type-template]] + [ctx-elem (code:line [id ≫ id : type-template] ooo ...)] + [inf (code:line inf-elem ooo ...)] + [inf-elem [expr-template ≫ pattern ⇒ type-pattern] + [expr-template ≫ pattern ⇐ type-pattern]] + [type-relation (code:line [type-template τ⊑ type-template] ooo ...) + (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)] + [conclusion [⊢ expr-template ⇒ type-template] + [⊢ [_ ≫ expr-template ⇒ type-template]] + [≻ expr-template] [_ ≻ expr-template]] - [⇐-conclusion [⊢ [_ ≫ expr-template ⇐ _]]] + [⇐-conclusion [⊢ expr-template] + [⊢ [_ ≫ expr-template ⇐ _]]] [ooo ...]) ]{ -Defines a macro that can do typechecking. It's roughly an -extension of @racket[syntax-parse] that allows writing -type-judgement-like rules that interleave typechecking and -macro expansion. -To typecheck an expression @racket[e], it needs to expand it -to get its type. To express that, write the clause -@racket[[⊢ [e ≫ pattern ⇒ type-pattern]]]. An example use of -this would be @racket[[⊢ [e ≫ e- ⇒ τ_e]]], which binds the -pattern variables @racket[e-] and @racket[τ_e] to the expanded -version of @racket[e] and the type of it, respectively. +Defines a macro that additionally performs typechecking. It uses +@racket[syntax-parse] @tech{syntax patterns} and @tech{pattern directives} and + additionally allows writing type-judgement-like rules that interleave + typechecking and macro expansion. -To check that an expression @racket[e] has a given type -@racket[τ_expected], it also needs to expand it. To express -that, write the clause -@racket[[⊢ [e ≫ pattern ⇐ τ_expected]]]. An example of this -would be @racket[[e ≫ e- ⇐ Int]]. +Type checking is computed as part of macro expansion and the resulting type is + attached to an expanded expression. In addition, Turnstile supports + bidirectional declarations. For example +@racket[[⊢ e ≫ e- ⇒ τ]] states that expression @racket[e] expands to @racket[e-] + and has type @racket[τ], where @racket[e] is the input and, @racket[e-] and + @racket[τ] outputs. Put another way, @racket[e] is a syntax template position + and @racket[e-] @racket[τ] are syntax pattern positions. + +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). } + +@defform[(define-syntax-category name-id)]{ +Defines a new "category" of syntax by defining a series of forms and functions. +A language implemented with Turnstile will typically begin with + @racket[(define-syntax-category type)], which in turn defines: + @itemlist[ + @item{@racket[define-base-type]: A form for defining a base type. + A call @racket[(define-base-type τ)] additionally defines: + @itemlist[@item{@racket[τ]: An identifier macro representing type @racket[τ].} + @item{@racket[τ?]: A predicate recognizing type @racket[τ].} + @item{@racket[~τ]: A @tech{pattern expander} recognizing type @racket[τ].}]} + @item{@racket[define-base-types]: Defines multiple base types.} + @item{@racket[define-type-constructor]: A form for defining type constructors. + @defform[(define-type-constructor Name option ...) + #:grammar + ([option (code:line #:arity op n) + (code:line #:bvs op n) + (code:line #:arr tycon) + (code:line #:arg-variances expr) + (code:line #:extra-info stx)])]{ + Defining a type constructor @racket[τ] defines: + @itemlist[@item{@racket[τ]: An macro for constructing instance of type @racket[τ].} + @item{@racket[τ?]: A predicate recognizing type @racket[τ].} + @item{@racket[~τ]: A @tech{pattern expander} recognizing type @racket[τ].}] + The @racket[#:arity] argument specifies valid shapes of the type. For example + @racket[(define-type-constructor → #:arity >= 1)] defines an arrow type and + @racket[(define-type-constructor List #:arity = 1)] defines a list type. + + Use @racket[#:bvs] argument to define binding types, eg + @racket[(define-type-constructor ∀ #:bvs = 1 #:arity = 1)] defines a single-argument + ∀ type. + + The @racket[#:extra-info] argument is useful for attaching additional metainformation + to types, for example to implement pattern matching. + }} + @item{@racket[type=?]: An equality predicate for types that computes + structural @racket[free-identifier=?] equality.} + @item{Sets @racket[current-typecheck-relation] to @racket[type=?].} + @item{@racket[types=?]: An predicate for checking equality of lists of types.} + @item{@racket[same-types?]: A predicate for checking if a list of types are all the same.} + @item{@racket[current-type=?]: A parameter for computing type equality.} + @item{@racket[#%type]: A "kind" used to validate types.} + @item{@racket[is-type?]: A predicate used to validate types. Checks for @racket[#%type].} + @item{@racket[current-is-type?]: A parameter, initialized to @racket[is-type?], + used to validate types. Useful when reusing type rules in different languages.} + @item{@racket[mk-type]: Marks a syntax object as a type by attaching @racket[#%type].} + @item{@racket[type]: A syntax class that recognizes valid types.} + @item{@racket[type-bind]: A syntax class that recognizes syntax objects with shape @racket[[x:id (~datum :) τ:type]].} + @item{@racket[type-ctx]: A syntax class recognizing syntax objects with shape @racket[(b:type-bind ...)].} + @item{@racket[type-ann]: A syntax class recognizing syntax objects with shape @racket[{τ:type}].} + ] +} + +@section{Lower-level functions} + +This section describes lower-level functions. It's usually not necessary to call these directly, +since @racket[define-typed-syntax] and other forms already do so. + +@defparam[current-type-eval type-eval type-eval]{ + Parameter for controlling "type evaluation". A @racket[type-eval] function consumes and + produces syntax and defaults to @racket[syntax-local-expand-expression], + extended to store extra surface syntax information used for error reporting. + This is called before a type is attached to a syntax object.} + +@defparam[current-typecheck-relation type-pred type-pred]{ + Parameter for controlling type checking. A @racket[type-pred] function consumes + two types and returns true if they "type check". Not necessarily 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 function that calls + @racket[current-typecheck-relation].} + +@defproc[(typechecks? [τs1 (list/c type?)] [τs2 (list/c type?)]) boolean?]{ +Maps @racket[typecheck?] over lists of types.} + +@defproc[(assign-type [e expr-stx] [τ type-stx]) stx]{ +Calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e]} + +@defproc[(typeof [e expr-stx]) type-stx]{ +Returns type of @racket[e].} + +@defproc[(infer [es (listof expr-stx)] + [#:ctx ctx (listof bindings) null] + [#:tvctx tvctx (listof tyvar-bindings) null]) (list tvs xs es τs)]{ +Expands a list of expressions, in the given contexts and computes their types. + Returns the expanded expressions, their types, and expanded identifiers from the + contexts.} + +@defproc[(subst [τ type-stx] + [x id] + [e expr-stx] + [cmp (-> any/c any/c boolean?) bound-identifier=?]) expr-stx]{ +Replaces occurrences of @racket[x], as determined by @racket[cmp], with + @racket[τ] in @racket[e].} + +@defproc[(substs [τs (listof type-stx)] + [xs (listof id)] + [e expr-stx] + [cmp (-> any/c any/c boolean?) bound-identifier=?]) expr-stx]{ +Folds @racket[subst] over the given @racket[τs] and @racket[xs].} +