Type expander library🔗ℹ

This library is implemented using literate programming. The implementation details are presented in the Type expander: Implementation document.

It enhances typed/racket with type expanders, which are special macros that can appear wherever a regular type is usually expected, and must expand to a type. Type expanders are to types what match expanders are to match patterns.

It is based on Asumu Takikawa’s type expanders (see also his original pull request). Asumu Takikawa’s work attempted to integrate type expanders directly into Typed/Racket. This project instead implements type expanders as a library, which does not need any changes to the core Typed/Racket codebase. This shows the extensibility of Typed/Racket thanks to macros, and could serve as the basis for other projects which need to alter how Typed/Racket handles types.

The input for a type expander is the syntax used to call it, just as the input to a macro is the syntax used to call it. The output should be a type, which can itself contain type expanders.

This library works by shadowing the definitions of :, define, lambda etc. from typed/racket with versions which support type expanders.

1 #lang and module languages based on type-expander🔗ℹ

1.1 #lang combining type-expander and typed/racket🔗ℹ

1.2 Module language combining type-expander and typed/racket🔗ℹ

1.3 #lang and module language combining type-expander and typed/racket/base🔗ℹ

2 Defining new type expanders🔗ℹ

For example, one could define the HomogeneousList type expander, which accepts a type t and an integer n, and produces a List type with n elements, each of type t:

(define-type-expander (HomogeneousList stx)

(syntax-case stx ()

[(_ t n)

(number? (syntax-e #'n))

(with-syntax ([(tᵢ ...) (stx-map (const #'t)

(range (syntax-e #'n)))])

#'(List tᵢ ...))]))

2.1 Attaching type expanders to existing identifiers🔗ℹ

It allows attaching type expanders to existing identifiers, without shadowing them. It is used for example to attach the type expanders for quote, quasiquote, syntax and quasisyntax which are described below, and also for the curry type expander.

3 Using a type expander🔗ℹ

The HomogeneousList type expander defined above could be used in many of typed/racket’s forms.

(define-type three-ints (HomogeneousList 3 Integer))

(define (incr3 [x : three-ints]) : (HomogeneousList 3 Integer)

(map add1 x))

(ann (incr3 '(1 2 3)) (HomogeneousList 3 Integer))

Type expanders can produce types which may contain other uses of type expanders, much in the same way as macros can expand to code calling other macros. The type expander can also produce directly a call to another type expander, just as a macro can expand to a call to another macro, without any extra surrounding syntax.

Contrarily to macros, if a call to a type expander is in the first position of more arguments, then the nested call is first expanded, and can produce the name of a second expander which will use the outer arguments, or can simply produce a polymorphic type which will be applied to the arguments. More than two levels of nesting are possible.

4 Debugging type expanders🔗ℹ

Currently, when debugging information is enabled, the type expander prints at each step a human-readable representation of the syntax object it is about to expand, and once an expansion step finishes, it prints the original syntax object as well as its expanded form. The identifiers are adorned with superscripts indicating the scopes present on them. See the documentation for the debugging tool +scopes for more details.

5 Compile-time aspects of type expanders🔗ℹ

The property value must be a procedure of arity 1 or 2, or an exact-nonnegative-integer? designating a field index within the structure which contains such a procedure. If the procedure’s arity includes 2, then the first argument is the structure itself (which satisfies prop:type-expander?), and the second argument is the syntax object to transform. Otherwise, the single argument is the syntax object to transform.

The procedure serves as a syntax transformer when expanding the use of a type expander. If the type expander was in the first position of a syntax list (i.e. it looks like a macro or function call), then the whole syntax list is passed as an argument. Otherwise, just the identifier is passed as an argument, exactly as what would be done when calling an identifier macro. The procedure can support other use patterns if desired, so that it would be possible in principle to implement special type forms that behave in a way similar to set! Transformers.

5.1 Syntax class for :🔗ℹ

The colon syntax class is provided for-syntax by this library, and can be used in syntax-parse patterns, using c:colon for example. It matches both the original : and the new :, but not other : identifiers.

It can be used to write macros which expect either : identifier.

5.2 Syntax classes for types🔗ℹ

Future versions may implement this as a non-flat contract, in order to be able to check that in a macro’s result, the syntax for a type is not used as an expression, and vice versa.

6 multi-id🔗ℹ

Type expanders are supported by the multi-id library. It is therefore easy to define an identifier which acts as a type expander and match expander as well as a regular racket macro and/or identifier macro. This can be useful to define feature-rich data structures, which need to provide all of the above features.

7 Expansion model for type expanders🔗ℹ

The expansion model for type expanders is similar to the expansion model for macros. There are a few differences, however, which are presented below.

• When a form like (f args ... . rest) is encountered, if its first element, f, is a type expander, the type expander is applied to the whole form. If f is a special identifier (e.g. like Let or Rec), then the form is handled according to the special identifier’s rules. Otherwise, the f form is expanded, and the result (e args ... . rest) is expanded once again (e being the result of the expansion of f).

  In comparison, the “official” macro expander for Racket would, in the last case, expand f on its own, and then expand the arguments one by one without re-considering the form as a whole.

  With the type expander, during the second expansion pass for the form, if the e identifier is a type expander it is applied to the whole form. If e is a special identifier, the form is processed following that identifier’s rules. Otherwise, the e form is left intact, and the arguments args ... and rest are expanded each in turn.

  In comparison, the “official” macro expander would have fully expanded e in isolation (e.g. as an identifier macro), without letting it take over the arguments.

• With the “official” macro expander, all forms at the same lexical scoping level are expanded before expanding the contents of let forms.

  In contrast, the type expander expands the contents of Let forms in the same order as other forms. It further replaces the Let forms by their contents, so that the following type:

  ((Let ([Foo Pairof]) Foo) Number String)

  gets expanded by replacing (Let ([Foo Pairof]) Foo) by its contents (i.e. the Foo identifier in this case):

  (Foo Number String)

  The Foo identifier is still bound to Pairof, so this new type expression gets expanded to:

  (Pairof Number String)

  This means that identifiers bound by Let forms can escape their scope, but are still attached to their defining scope.

• With the current implementation of the type expander, syntax-local-value ignores types bound by Let forms. A future version of this library will (hopefully) either fix this problem, or provide an alternative syntax-local-type-value which takes those bindings into account.

8 Built-in type expanders🔗ℹ

There are several built-in expanders. Some are documented here, while others are listed in (part ("(lib type-expander/type-expander.hl.rkt)" "Cases_handled_by_expand-type")). Their API should be considered unstable, and may change in the future.

8.1 Let🔗ℹ

8.2 Letrec🔗ℹ

8.3 Let*🔗ℹ

8.4 Λ🔗ℹ

(define-type-expander (gen-id gen-stx-id)

(auto-syntax-case gen-stx-id ()

[formals (let () . body)]))

where id and gen-stx-id are fresh unique identifiers.

Since Λ relies on auto-syntax-case, the syntax pattern variables bound by formals can also be used outside of syntax templates, in which case they evaluate to (syntax->datum #'pvar).

8.5 Quasiquote🔗ℹ

The type expander library also adds support for quasiquoting in types: The type `(a (1 b) ,String) is expanded to (List 'a (List 1 'b) String).

The quote, quasiquote, syntax and quasisyntax identifiers are interpreted specially within type expressions. The quote identifier can be used to describe a type matching containing only the quoted value. Similarly, syntax can be used to describe the type of the quoted syntax object, without the need to insert Syntaxof by hand around each part of the type. Note that the type #'(a b c) will match the syntax object #'(a b c), but not the syntax object #’(a b . (c)), i.e. the generated type is sensitive to the distinction between syntax pairs and syntax lists. It is possible that a future version of this library provides another type expander which accepts both. The quasiquote and quasisyntax forms allow the use of unquote and unsyntax, respectively.

8.6 Currying type expanders🔗ℹ

The curry special type-expander form can be used to curry in some arguments to a type expander.

9 Common issues (FAQ)🔗ℹ

• Explicitly requiring typed/racket causes an error:

  > (require typed/racket type-expander)

  module: identifier already imported from a different source in:   λ:   type-expander   typed/racket

  A required module can shadow the definitions provided by the #lang language, but it cannot shadow the definitions provided by other explicitly required modules.

  The solution is to avoid explicitly requiring typed/racket, or to subtract from it the identifiers that would otherwise be shadowed anyway:

  (require racket/require

  (subtract-in typed/racket type-expander)

  type-expander)

• An error complains that a type expander is unbound:

  > (module main typed/racket     (module m type-expander/lang       (provide foo)       (define-type-expander (foo stx) #'Void))     (require 'm)     (: v foo)     (define v (void)))

  Type Checker: parse error in type;  type name `foo' is unbound

  This error will be raised if the type-expander library is not required. It is best to double-check that a (require type-expander) form is present, and that it is present at the appropriate meta-level (it should be loaded at the same meta-level as the use of (: var type), (define var : type value)).

  In the example above, the problem is that the module main requires 'm, but does not require type-expander. The : in (: v foo) therefore comes from typed/racket, and does not know how to use the foo type expander.

• Q: Can I write a recursive type-level function?

  A: Yes, but be sure that it is not infinitely recursive, as the expansion would never terminate, unlike typed/racket’s Rec, which allows truly recursive types.

  Furthermore, it is best to ponder the risk of combinatorial explosion, for example in typed/racket, ((∀ (X) (List X X)) Number) expands internally to the type (List Number Number). Nesting this pattern a few times will produce a type having an in-memory representation whose size is exponential in the size of the original type declaration. A type expander can easily produce a very large type, which will bring the type checker to a crawl and/or crash it.

10 Overloaded typed/racket primitives🔗ℹ

11 Unimplemented typed/racket primitives (will be overloaded in later versions).🔗ℹ

12 Deprecated export of colon via type-expander🔗ℹ

13 Using contract syntax to specify types🔗ℹ

Furthermore, using ,τ anywhere outside of a quoted datum will leave the type τ unchaged, allowing the user to manually convert to types only the parts which cannot be converted automatically.