5 Typed Units

6.11

5 Typed Units

Warning: the features described in this section are experimental and may not work correctly. Some of the features may change by the next release.

Typed Racket provides support for modular programming with the units and signatures provided by the racket/unit library.

5.1 Special forms

(require typed/racket/unit)

package: typed-racket-lib

The special forms below are provided by the typed/racket/unit and typed/racket modules, but not by typed/racket/base. The typed/racket/unit module additionally provides all other bindings from racket/unit.

syntax
(define-signature id extension-decl
(sig-elem ...))

extension-decl =
| extends sig-id

sig-elem = [id : type]

Binds an identifier to a signature and registers the identifier in the signature environment with the specified type bindings. Sigantures in Typed Racket allow only specifications of variables and their types. Variable and syntax definitions are not allowed in the define-signature form. This is only a limitation of the define-signature form in Typed Racket.

As in untyped Racket, the extends clause includes all elements of extended signature and any implementation of the new signature can be used as an implementation of the extended signature.

syntax
(unit
  (import sig-spec ...)
  (export sig-spec ...)
  init-depends-decl
  unit-body-expr-or-defn
  ...)

sig-spec = sig-id
| (prefix id sig-spec)
| (rename sig-spec (id id) ...)
| (only sig-spec id ...)
| (except sig-spec id ...)

init-depends-decl =
| (init-depend sig-id ...)

The typed version of the Racket unit form. Unit expressions in Typed Racket do not support tagged signatures with the tag keyword.

syntax
(invoke-unit unit-expr)
(invoke-unit unit-expr (import sig-spec ...))

The typed version of the Racket invoke-unit form.

syntax
(define-values/invoke-unit unit-expr
(import def-sig-spec ...)
(export def-sig-spec ...))

def-sig-spec = sig-id
| (prefix id def-sig-spec)
| (rename def-sig-spec (id id) ...)

The typed version of the Racket define-values/invoke-unit form. In Typed Racket define-values/invoke-unit is only allowed at the top-level of a module.

syntax
(compound-unit
  (import link-binding ...)
  (export link-id ...)
  (link linkage-decl ...))

link-binding = (link-id : sig-id)

linkage-decl = ((link-binding ...) unit-expr link-id ...)

The typed version of the Racket compound-unit form.

syntax
(define-unit unit-id
  (import sig-spec ...)
  (export sig-spec ...)
  init-depends-decl
  unit-body-expr-or-defn
  ...)

The typed version of the Racket define-unit form.

syntax
(compound-unit/infer
  (import infer-link-import ...)
  (export infer-link-export ...)
  (link infer-linkage-decl ...))

infer-link-import = sig-id
| (link-id : sig-id)

infer-link-export = link-id
| sig-id

infer-linkage-decl =
((link-binding ...) unit-id
                    tagged-link-id ...)
| unit-id

The typed version of the Racket compound-unit/infer form.

syntax
(define-compound-unit id
  (import link-binding ...)
  (export link-id ...)
  (link linkage-decl ...))

The typed version of the Racket define-compound-unit form.

syntax
(define-compound-unit/infer id
  (import link-binding ...)
  (export infer-link-export ...)
  (link infer-linkage-decl ...))

The typed version of the Racket define-compound-unit/infer form.

syntax
(invoke-unit/infer unit-spec)

unit-spec = unit-id
| (link link-unit-id ...)

The typed version of the Racket invoke-unit/infer form.

syntax
(define-values/invoke-unit/infer maybe-exports unit-spec)

maybe-exports =
| (export sig-sepc ...)

unit-spec = unit-id
| (link link-unit-id ...)

The typed version of the Racket define-values/invoke-unit/infer form. Like the define-values/invoke-unit form above, this form is only allowed at the toplevel of a module.

syntax
(unit-from-context sig-spec)

The typed version of the Racket unit-from-context form.

syntax
(define-unit-from-context id sig-spec)

The typed version of the Racket define-unit-from-context form.

5.2 Types

syntax
(Unit
  (import sig-id ...)
  (export sig-id ...)
  optional-init-depend-clause
  optional-body-type-clause)

optional-init-depend-clause =
| (init-depend sig-id ...)

optional-body-type-clause =
| type
| (Values type ...)

The type of a unit with the given imports, exports, initialization dependencies, and body type. Omitting the init-depend clause is equivalent to an init-depend clause that contains no signatures. The body type is the type of the last expression in the unit’s body. If a unit contains only definitions and no expressions its body type is Void. Omitting the body type is equivalent to specifying a body type of Void.

Example:

> (module Unit-Types typed/racket
    (define-signature fact^ ([fact : (-> Natural Natural)]))
    (: use-fact@ (Unit (import fact^)
                       (export)
                       Natural))
    (define use-fact@ (unit (import fact^) (export) (fact 5))))

syntax
UnitTop

The supertype of all unit types. Values of this type cannot be linked or invoked. The primary use of is for the reflective operation unit?

5.3 Interacting with Untyped Code

syntax
(require/typed m rt-clause ...)

rt-clause = [maybe-renamed t]
|
[#:struct name ([f : t] ...)
struct-option ...]
|
[#:struct (name parent) ([f : t] ...)
struct-option ...]
| [#:opaque t pred]
| [#:signature name ([id : t] ...)]

maybe-renamed = id
| (orig-id new-id)

struct-option = #:constructor-name constructor-id
| #:extra-constructor-name constructor-id

The #:signature clause of require/typed requires the given signature and registers it in the signature environment with the specified bindings. Unlike other identifiers required with require/typed, signatures are not protected by contracts.

Signatures are not runtime values and therefore do not need to be protected by contracts.

Examples:

> (module UNTYPED-1 racket
    (provide a^)
    (define-signature a^ (a)))
> (module TYPED-1 typed/racket
    (require/typed 'UNTYPED-1
                   [#:signature a^ ([a : Integer])])
    (unit (import a^) (export) (add1 a)))

Typed Racket will infer whether the named signature extends another signature. It is an error to require a signature that extends a signature not present in the signature environment.

Examples:

> (module UNTYPED-2 racket
    (provide a-sub^)
    (define-signature a^ (a1))
    (define-signature a-sub^ extends a^ (a2)))
> (module TYPED-2 typed/racket
    (require/typed 'UNTYPED-2
                   [#:signature a-sub^
                     ([a1 : Integer]
                      [a2 : String])]))
build/user/6.11/pkgs/typed-racket-lib/typed-racket/base-env/
prims-contract.rkt:180:7: Type Checker: Error in macro
expansion -- required signature extends an untyped signature
  required signature: a-sub^
  extended signature: a^
  in: (require-typed-signature a-sub^ (a1 a2) (Integer
String) (quote UNTYPED-2))

Requiring a signature from an untyped module that contains variable definitions is an error in Typed Racket.

Examples:

> (module UNTYPED racket
    (provide bad^)
    (define-signature bad^ (bad (define-values (bad-ref) (car bad)))))
> (module TYPED typed/racket
    (require/typed 'UNTYPED
                   [#:signature bad^
                     ([bad : (Pairof Integer Integer)]
                      [bad-ref : Integer])]))
eval:8:0: Type Checker: Error in macro expansion -- untyped
signatures containing definitions are prohibited
  in: UNTYPED

5.4 Limitations

5.4.1 Signature Forms

Unlike Racket’s define-signature form, in Typed Racket define-signature only supports one kind of signature element that specifies the types of variables in the signature. In particular Typed Racket’s define-signature form does not support uses of define-syntaxes, define-values, or define-values-for-export . Requiring an untyped signature that contains definitions in a typed module will result in an error.

Examples:

> (module UNTYPED racket
    (provide bad^)
    (define-signature bad^ ((define-values (bad) 13))))
> (module TYPED typed/racket
    (require/typed 'UNTYPED
                   [#:signature bad^ ([bad : Integer])]))
eval:10:0: Type Checker: Error in macro expansion -- untyped
signatures containing definitions are prohibited
  in: UNTYPED

5.4.2 Contracts and Unit Static Information

Unit values that flow between typed and untyped contexts are wrapped in unit/c contracts to guard the unit’s imports, exports, and result upon invocation. When identifers that are additionally bound to static information about a unit, such as those defined by define-unit, flow between typed and untyped contexts contract application can result the static information becoming inaccessible.

Examples:

> (module UNTYPED racket
    (provide u@)
    (define-unit u@ (import) (export) "Hello!"))
> (module TYPED typed/racket
    (require/typed 'UNTYPED
                   [u@ (Unit (import) (export) String)])
    (invoke-unit/infer u@))
eval:12:0: untyped-invoke-unit/infer: unknown unit
definition
  at: u@
  in: (untyped-invoke-unit/infer u@)

When an identifier bound to static unit information flows from a typed module to an untyped module, however, the situation is worse. Because unit static information is bound to an identifier as a macro definition, any use of the typed unit is disallowed in untyped contexts.

Examples:

> (module TYPED typed/racket
    (provide u@)
    (define-unit u@ (import) (export) "Hello!"))
> (module UNTYPED racket
    (require 'TYPED)
    u@)
eval:14:0: Type Checker: Macro u@ from typed module used in
untyped code
  in: u@

5.4.3 Signatures and Internal Definition Contexts

Typed Racket’s define-signature form is allowed in both top-level and internal definition contexts. As the following example shows, defining signatures in internal definiition contexts can be problematic.

Example:

> (module TYPED typed/racket
    (define-signature a^ ())
    (define u@
      (let ()
        (define-signature a^ ())
        (unit (import a^) (export) (init-depend a^) 5)))
    (invoke-unit u@ (import a^)))
eval:15:0: Type Checker: type mismatch
  expected: (Unit (import a^) (export) (init-depend a^)
AnyValues)
  given: (Unit (import a^) (export) (init-depend a^)
Positive-Byte)
  in: a^

Even though the unit imports a signature named a^, the a^ provided for the import refers to the top-level a^ signature and the type system prevents invoking the unit. This issue can be avoided by defining signatures only at the top-level of a module.

5.4.4 Tagged Signatures

Various unit forms in Racket allow for signatures to be tagged to support the definition of units that import or export the same signature multiple times. Typed Racket does not support the use of tagged signatures, using the tag keyword, anywhere in the various unit forms described above.

5.4.5 Structural Matching and Other Unit Forms

Typed Racket supports only those unit forms described above. All other bindings exported by racket/unit are not supported in the type system. In particular, the structural matching forms including unit/new-import-export and unit/s are unsupported.

top ← prev up next →

1	Type Reference
2	Special Form Reference
3	Libraries Provided With Typed Racket
4	Typed Classes
5	Typed Units
6	Utilities
7	Exploring Types
8	Typed Racket Syntax Without Type Checking
9	Typed Regions
10	Optimization in Typed Racket
11	Unsafe Typed Racket operations
12	Legacy Forms
13	Compatibility Languages
14	Experimental Features

5.1	Special forms
5.2	Types
5.3	Interacting with Untyped Code
5.4	Limitations