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]
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 ...)
syntax
(invoke-unit unit-expr)
(invoke-unit unit-expr (import sig-spec ...))
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) ...)
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 ...)
syntax
(define-unit unit-id (import sig-spec ...) (export sig-spec ...) init-depends-decl unit-body-expr-or-defn ...)
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
syntax
(define-compound-unit id (import link-binding ...) (export link-id ...) (link linkage-decl ...))
syntax
(define-compound-unit/infer id (import link-binding ...) (export infer-link-export ...) (link infer-linkage-decl ...))
syntax
(invoke-unit/infer unit-spec)
unit-spec = unit-id | (link link-unit-id ...)
syntax
(define-values/invoke-unit/infer maybe-exports unit-spec)
maybe-exports =
| (export sig-sepc ...) unit-spec = unit-id | (link link-unit-id ...)
syntax
(unit-from-context sig-spec)
syntax
(define-unit-from-context id sig-spec)
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 ...)
> (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
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
Signatures are not runtime values and therefore do not need to be protected by contracts.
> (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.
> (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])])) eval:6:0: Type Checker: Error in macro expansion -- required
signature extends an untyped signature
required signature: a-sub^
extended signature: a^
in: UNTYPED-2
Requiring a signature from an untyped module that contains variable definitions is an error in Typed Racket.
> (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.
> (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.
> (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.
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.
> (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.