2 Special Form Reference

Typed Racket provides a variety of special forms above and beyond those in Racket. They are used for annotating variables with types, creating new types, and annotating expressions.

2.1Binding Forms🔗 i

loop, f, a, and var are names, type is a type. e is an expression and body is a block.

syntax
( let maybe-tvars(binding...)maybe-ret. body)
(let loopmaybe-ret(binding...). body)

binding = [vare]
| [var:typee]

maybe-tvars =
| #:forall(tvar...)
| #:∀(tvar...)

maybe-ret =
| :type0

Local bindings, like let , each with associated types.

In the first form, maybe-ret can only appear with maybe-tvars, so if you only want to specify the return type, you should set maybe-tvars to #:forall().

Examples:

> (let ([x:Zero 0])x)

- : Integer [more precisely: Zero]

0
> (let #:forall()([x:Zero 0]):Natural x)

- : Integer [more precisely: Zero]

0
> (let ([x:Zero 0]):Natural x)

eval:4:0: :: bad syntax

in: :

If polymorphic type variables are provided, they are bound in the type expressions for variable bindings.

Example:

> (let #:forall(A)([x:A0])x)

- : Integer [more precisely: Zero]

0

In the second form, type0 is the type of the result of loop (and thus the result of the entire expression as well as the final expression in body). Type annotations are optional.

Examples:

> (:filter-even(-> (Listof Natural )(Listof Natural )(Listof Natural )))

> (define (filter-evenlstaccum)
(if (null? lst)
accum
(let ([first :Natural (car lst)]
[rest :(Listof Natural )(cdr lst)])
(if (even? first )
(filter-evenrest (cons first accum))
(filter-evenrest accum)))))
> (filter-even(list 123456)null )

- : (Listof Nonnegative-Integer)

'(6 4 2)

Examples:

> (:filter-even-loop(-> (Listof Natural )(Listof Natural )))

> (define (filter-even-looplst)
(let loop:(Listof Natural )
([accum:(Listof Natural )null ]
[lst:(Listof Natural )lst])
(cond
[(null? lst)accum]
[(even? (car lst))(loop(cons (car lst)accum)(cdr lst))]
[else (loopaccum(cdr lst))])))
> (filter-even-loop(list 1234))

- : (Listof Nonnegative-Integer)

'(4 2)

syntax
( letrec (binding...). body)

syntax
( let* (binding...). body)

syntax
( let-values ([(var+type...)e]...). body)

syntax
( letrec-values ([(var+type...)e]...). body)

syntax
( let*-values ([(var+type...)e]...). body)

Type-annotated versions of letrec , let* , let-values , letrec-values , and let*-values . As with let , type annotations are optional.

syntax
( let/cc v:t. body)

syntax
( let/ec v:t. body)

Type-annotated versions of let/cc and let/ec . As with let , the type annotation is optional.

2.2Anonymous Functions🔗 i

syntax
( lambda maybe-tvarsformalsmaybe-ret. body)

formals = (formal...)
| (formal.... rst)

formal = var
| [vardefault-expr]
| [var:type]
| [var:typedefault-expr]
| keywordvar
| keyword[var:type]
| keyword[var:typedefault-expr]

rst = var
| [var:type*]
| [var:typeooobound]

maybe-tvars =
| #:forall(tvar...)
| #:∀(tvar...)
| #:forall(tvar...ooo)
| #:∀(tvar...ooo)

maybe-ret =
| :type

Constructs an anonymous function like the lambda form from racket/base, but allows type annotations on the formal arguments. If a type annotation is left out, the formal will have the type Any .

Examples:

> (lambda ([x:String ])(string-append x"bar"))

- : (-> String String)

#<procedure>
> (lambda (x[y:Integer ])(add1 y))

- : (-> Any Integer Integer)

#<procedure>
> (lambda (x)x)

- : (-> Any Any)

#<procedure>

Type annotations may also be specified for keyword and optional arguments:

Examples:

> (lambda ([x:String "foo"])(string-append x"bar"))

- : (->* () (String) (String : (Top | Bot)))

#<procedure:eval:15:0>
> (lambda (#:x[x:String ])(string-append x"bar"))

- : (-> #:x String String)

#<procedure:eval:16:0>
> (lambda (x#:y[y:Integer 0])(add1 y))

- : (-> Any [#:y Integer] Integer)

#<procedure:eval:17:0>
> (lambda ([x'default])x)

- : (->* () (Any) Any)

#<procedure:eval:18:0>

The lambda expression may also specify polymorphic type variables that are bound for the type expressions in the formals.

Examples:

> (lambda #:forall(A)([x:A])x)

- : (All (A) (-> A A))

#<procedure>
> (lambda #:∀(A)([x:A])x)

- : (All (A) (-> A A))

#<procedure>

In addition, a type may optionally be specified for the rest argument with either a uniform type or using a polymorphic type. In the former case, the rest argument is given the type (Listof type) where type is the provided type annotation.

Examples:

> (lambda (x. rst)rst)

- : (-> Any Any * (Listof Any))

#<procedure>
> (lambda (xrst:Integer *)rst)

- : (-> Any Integer * (Listof Integer))

#<procedure>
> (lambda #:forall(A... )(xrst:A... A)rst)

- : (All (A ...) (-> Any A ... A (List A ... A)))

#<procedure>

syntax
λ

An alias for lambda .

syntax
( case-lambda maybe-tvars[formalsbody]...)

A function of multiple arities. The formals are identical to those accepted by the lambda form except that keyword and optional arguments are not allowed.

Polymorphic type variables, if provided, are bound in the type expressions in the formals.

Note that each formals must have a different arity.

Example:

> (define add-map
(case-lambda
[([lst: (Listof Integer )])
(map add1 lst)]
[([lst1: (Listof Integer )]
[lst2: (Listof Integer )])
(map + lst1lst2)]))

To see how to declare a type for add-map, see the case-> type constructor.

syntax
case-λ

An alias for case-lambda .

2.3Loops🔗 i

syntax
( for void-ann-maybe(for-clause...)void-ann-maybeexpr...+)

void-ann-maybe =
| :Void

type-ann-maybe =
| :u

for-clause = [id:tseq-expr]
| [(binding...)seq-expr]
| [idseq-expr]
| #:whenguard
| #:unlessguard
| #:do[do-body...]
| break-clause
| #:splice(splicing-id. form)

binding = id
| [id:t]

break-clause = #:breakguard
| #:finalguard

Like for from racket/base, but each id has the associated type t. The latter ann-maybe will be used first, and then the previous one. Since the return type is always Void, annotating the return type of a for form is optional. Type annotations in clauses are optional for all for variants.

Examples:

> (for ([i'()])i)
> (for :Void([i'()])i)
> (for ([i'()]):Voidi)
> (for :Void([i'()]):Voidi)
> (for ([i'()]):Any i)

eval:29:0: :: bad syntax

in: :
> (for/or :False ([i'()]):False #f)

- : False

#f
> (for/or :Boolean ([i'()]):False #f)

- : Boolean

#f
> (for/or :False ([i'()]):Boolean #f)

eval:32:0: Type Checker: type mismatch

expected: False

given: Boolean

in: #f

syntax
( for/list type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/hash type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/hasheq type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/hasheqv type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/hashalw type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/vector type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/or type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/sum type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/product type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/last type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/set type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/list type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/hash type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/hasheq type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/hasheqv type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/hashalw type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/vector type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/or type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/sum type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/product type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/last type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/set type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

These behave like their non-annotated counterparts, with the exception that #:when clauses can only appear as the last for-clause. The return value of the entire form must be of type u. For example, a for/list form would be annotated with a Listof type. All annotations are optional.

syntax
( for/and type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for/first type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/and type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

syntax
( for*/first type-ann-maybe(for-clause...)type-ann-maybeexpr...+)

Like the above, except they are not yet supported by the typechecker.

syntax
( for/lists type-ann-maybe
([id:t]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

syntax
( for/fold type-ann-maybe
([id:tinit-expr]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

syntax
( for/foldr type-ann-maybe
([id:tinit-expr]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

maybe-result =
| #:resultresult-expr

These behave like their non-annotated counterparts. Unlike the above, #:when clauses can be used freely with these.

Changed in version 1.11 of package typed-racket-lib: Added the #:result form.

Changed in version 1.12 of package typed-racket-lib: Added for/foldr .

syntax
( for* void-ann-maybe(for-clause...)void-ann-maybeexpr...+)

syntax
( for*/lists type-ann-maybe
([id:t]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

syntax
( for*/fold type-ann-maybe
([id:tinit-expr]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

syntax
( for*/foldr type-ann-maybe
([id:tinit-expr]...maybe-result)
(for-clause...)
type-ann-maybe
expr...+)

maybe-result =
| #:resultresult-expr

These behave like their non-annotated counterparts.

Changed in version 1.11 of package typed-racket-lib: Added the #:result form.

Changed in version 1.12 of package typed-racket-lib: Added for*/foldr .

syntax
( do :u([id:tinit-exprstep-expr-maybe]...)
(stop?-exprfinish-expr...)
expr...+)

step-expr-maybe =
| step-expr

Like do from racket/base, but each id having the associated type t, and the final body expr having the type u. Type annotations are optional.

2.4Definitions🔗 i

syntax
( define maybe-tvarsvmaybe-anne)
(define maybe-tvarsheadermaybe-ann. body)

header = (function-name. formals)
| (header. formals)

formals = (formal...)
| (formal.... rst)

formal = var
| [vardefault-expr]
| [var:type]
| [var:typedefault-expr]
| keywordvar
| keyword[var:type]
| keyword[var:typedefault-expr]

rst = var
| [var:type*]
| [var:typeooobound]

maybe-tvars =
| #:forall(tvar...)
| #:∀(tvar...)
| #:forall(tvar...ooo)
| #:∀(tvar...ooo)

maybe-ann =
| :type

Like define from racket/base, but allows optional type annotations for the variables.

The first form defines a variable v to the result of evaluating the expression e. The variable may have an optional type annotation.

Examples:

> (define foo"foo")
> (define bar:Integer 10)

If polymorphic type variables are provided, then they are bound for use in the type annotation.

Example:

> (define #:forall(A)mt-seq:(Sequenceof A)empty-sequence )

The second form allows the definition of functions with optional type annotations on any variables. If a return type annotation is provided, it is used to check the result of the function.

Like lambda , optional and keyword arguments are supported.

Examples:

> (define (add[first :Integer ]
[second :Integer ]):Integer
(+ first second ))

> (define #:forall(A)
(poly-app[func:(AA-> A)]
[first :A]
[second :A]):A
(funcfirst second ))

The function definition form also allows curried function arguments with corresponding type annotations.

Examples:

> (define ((addx[x:Number ])[y:Number ])(+ xy))
> (define add2(addx2))
> (add25)

- : Number

7

Note that unlike define from racket/base, define does not bind functions with keyword arguments to static information about those functions.

2.5Structure Definitions🔗 i

syntax
( struct maybe-type-varsname-spec([f: t]...)options...)

maybe-type-vars =
| (v...)

name-spec = name-id
| name-idparent

options = #:transparent
| #:mutable
| #:prefab
| #:constructor-nameconstructor-id
| #:extra-constructor-nameconstructor-id
| #:propertyproperty-idproperty-expr
| #:type-nametype-id

Defines a structure with the name name-id, where the fields f have types t, similar to the behavior of struct from racket/base.

Examples:

> (struct camelia-sinensis([age: Integer ]))
> (struct camelia-sinensis-assamicacamelia-sinensis())

If type-id is not specified, name-id will be used for the name of the type associated with instances of the declared structure. Otherwise, type-id will be used for the type name, and using name-id in this case will cause a type error.

Examples:

> (struct apple()#:type-nameBigApple)
> (ann (apple)BigApple)

- : BigApple

#<apple>
> (ann (apple)apple)

eval:45:0: Type Checker: parse error in type;

type name `apple' is unbound

in: apple

type-id can be also used as an alias to name-id, i.e. it will be a transformer binding that encapsulates the same structure information as name-id does.

Examples:

> (struct avocado([amount: Integer ])#:type-nameAvocado)
> (struct hass-avocadoAvocado())
> (struct-copy Avocado(avocado0)[amount42])

- : Avocado

#<avocado>

When parent is present, the structure is a substructure of parent.

When maybe-type-vars is present, the structure is polymorphic in the type variables v. If parent is also a polymorphic struct, then there must be at least as many type variables as in the parent type, and the parent type is instantiated with a prefix of the type variables matching the amount it needs.

Examples:

> (struct (XY)2-tuple([first : X][second : Y]))
> (struct (XYZ)3-tuple2-tuple([third : Z]))

Options provided have the same meaning as for the struct form from racket/base (with the exception of #:type-name, as described above).

A prefab structure type declaration will bind the given name-id or type-id to a Prefab type. Unlike the struct form from racket/base, a non-prefab structure type cannot extend a prefab structure type.

Examples:

> (struct a-prefab([x: String ])#:prefab)
> (:type a-prefab)

(Prefab a-prefab String)
> (struct not-alloweda-prefab())

eval:53:0: Type Checker: Error in macro expansion -- parent

type not a valid structure name: a-prefab

in: ()

Changed in version 1.4 of package typed-racket-lib: Added the #:type-name option.

syntax
( define-struct maybe-type-varsname-spec([f: t]...)options...)

maybe-type-vars =
| (v...)

name-spec = name-id
| (name-idparent)

options = #:transparent
| #:mutable
| #:type-nametype-id

Legacy version of struct , corresponding to define-struct from racket/base.

Changed in version 1.4 of package typed-racket-lib: Added the #:type-name option.

2.6Names for Types🔗 i

syntax
( define-type nametmaybe-omit-def)
(define-type (namev...)tmaybe-omit-def)

maybe-omit-def = #:omit-define-syntaxes
|

The first form defines name as type, with the same meaning as t. The second form defines name to be a type constructor, whose parameters are v... and body is t. If no parameters are declared, the defined type constructor is equivalent to (define-type nametmaybe-omit-def). Type names may refer to other types defined in the same or enclosing scopes.

Examples:

> (define-type IntStr(U Integer String ))
> (define-type (ListofPairsA)(Listof (Pair AA)))

If #:omit-define-syntaxes is specified, no definition of name is created. In this case, some other definition of name is necessary.

If the body of the type definition refers to itself, then the type definition is recursive. Recursion may also occur mutually, if a type refers to a chain of other types that eventually refers back to itself.

Examples:

> (define-type BT(U Number (Pair BTBT)))

> (let ()
(define-type (EvenA)(U Null (Pairof A(OddA))))
(define-type (OddA)(Pairof A(EvenA)))
(: even-lst(EvenInteger ))
(define even-lst'(12))
even-lst)

- : (Even Integer)

'(1 2)

However, the recursive reference is only allowed when it is passed to a productive type constructor:

Examples:

> (define-type FooFoo)

eval:58:0: Type Checker: Error in macro expansion -- parse

error in type;

not in a productive position

variable: Foo

in: Foo
> (define-type Bar(U BarFalse ))

eval:59:0: Type Checker: Error in macro expansion -- parse

error in type;

not in a productive position

variable: Bar

in: False
> (define-type Bar(U (Listof Bar)False ))

2.7Generating Predicates Automatically🔗 i

syntax
( make-predicate t)

Evaluates to a predicate for the type t, with the type (Any -> Boolean : t). t may not contain function types, or types that may refer to mutable data such as (Vectorof Integer ).

syntax
( define-predicate namet)

Equivalent to (define name(make-predicate t)).

2.8Type Annotation and Instantiation🔗 i

syntax
( : vt)
(: v: t)

This declares that v has type t. The definition of v must appear after this declaration. This can be used anywhere a definition form may be used.

Examples:

> (: var1Integer )
> (: var2String )

The second form allows type annotations to elide one level of parentheses for function types.

Examples:

> (: var3: -> Integer )
> (: var4: String -> Integer )

syntax
( provide: [vt]...)

This declares that the vs have the types t, and also provides all of the vs.

syntax
#{v:t}

This declares that the variable v has type t. This is legal only for binding occurrences of v.

If a dispatch macro on #\{ already exists in the current readtable, this syntax will be disabled.

syntax
( ann et)

Ensure that e has type t, or some subtype. The entire expression has type t. This is legal only in expression contexts.

syntax
#{e::t}

A reader abbreviation for (ann et).

If a dispatch macro on #\{ already exists in the current readtable, this syntax will be disabled.

syntax
( cast et)

The entire expression has the type t, while e may have any type. The value of the entire expression is the value returned by e, protected by a contract ensuring that it has type t. This is legal only in expression contexts.

Examples:

> (cast 3Integer )

- : Integer

3
> (cast 3String )

(cast for #f): broke its own contract

promised: string?

produced: 3

in: string?

contract from: cast

blaming: cast

(assuming the contract is correct)

at: eval:66:0
> (cast (lambda ([x: Any ])x)(String -> String ))

- : (-> String String)

#<procedure:val>
> ((cast (lambda ([x: Any ])x)(String -> String ))"hello")

- : String

"hello"

The value is actually protected with two contracts. The second contract checks the new type, but the first contract is put there to enforce the old type, to protect higher-order uses of the value.

Examples:

> ((cast (lambda ([s: String ])s)(Any -> Any ))"hello")

- : Any

"hello"
> ((cast (lambda ([s: String ])s)(Any -> Any ))5)

(cast for val): contract violation

expected: string?

given: 5

in: the 1st argument of

(-> string? any)

contract from: typed-world

blaming: cast

(assuming the contract is correct)

at: eval:70:0

cast will wrap the value e in a contract which will affect the runtime performance of reading and updating the value. This is needed when e is a complex data type, such as a hash table. However, when the type of the value can be checked using a simple predicate, consider using assert instead.

syntax
( inst et...)
(inst et...tooobound)

Instantiate the type of e with types t... or with the poly-dotted types t... tooobound. e must have a polymorphic type that can be applied to the supplied number of type variables. For non-poly-dotted functions, however, fewer arguments can be provided and the omitted types default to Any . inst is legal only in expression contexts.

Examples:

> (foldl (inst cons Integer Integer )null (list 1234))

- : (Listof Integer)

'(4 3 2 1)
> (: my-cons(All (AB)(-> AB(Pairof AB))))
> (define my-conscons )
> (: foldl-list: (All (α)(Listof α)-> (Listof α)))

> (define (foldl-listlst)
(foldl (inst my-consα(Listof α))null lst))
> (foldl-list(list "1""2""3""4"))

- : (Listof String)

'("4" "3" "2" "1")
> (: foldr-list: (All (α)(Listof α)-> Any ))

> (define (foldr-listlst)
(foldr (inst my-consα)null lst))
> (foldr-list(list "1""2""3""4"))

- : Any

'("1" "2" "3" "4")
> (: my-values: (All (AB... )(AB... -> (values AB... B))))

> (define (my-valuesarg. args)
(apply (inst values AB... B)argargs))

syntax
( row-inst erow)

Instantiate the row-polymorphic type of e with row. This is legal only in expression contexts.

Examples:

> (: id(All (r#:row)
(-> (Class #:row-varr)(Class #:row-varr))))
> (define (idcls)cls)

> ((row-inst id(Row (field [xInteger ])))
(class object% (super-new )(field [x: Integer 0])))

- : (Class (field (x Integer)))

#<class:eval:84:0>

syntax
#{e@t...}

A reader abbreviation for (inst et... ).

syntax
#{e@t...tooobound}

A reader abbreviation for (inst et... tooobound).

2.9Require🔗 i

Here, m is a module spec, pred is an identifier naming a predicate, and maybe-renamed is an optionally-renamed identifier.

syntax
( require/typed mrt-clause...)

rt-clause = [maybe-renamedt]
|
[#:structmaybe-tvarsname-id([f: t]...)
struct-option...]
|
[#:structmaybe-tvars(name-idparent)([f: t]...)
struct-option...]
| [#:opaquetpred]
| [#:signaturename([id: t]...)]

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

maybe-tvars =
| (type-variable...)

struct-option = #:constructor-nameconstructor-id
| #:extra-constructor-nameconstructor-id
| #:type-nametype-id

This form requires identifiers from the module m, giving them the specified types.

The first case requires maybe-renamed, giving it type t.

The second and third cases require the struct with name name-id and creates a new type with the name type-id, or name-id if no type-id is provided, with fields f... , where each field has type t. The third case allows a parent structure type to be specified. The parent type must already be a structure type known to Typed Racket, either built-in or via require/typed . The structure predicate has the appropriate Typed Racket filter type so that it may be used as a predicate in if expressions in Typed Racket.

Examples:

> (module UNTYPEDracket/base
(define n100)

(struct IntTree
(elemleftright))

(provide n(struct-out IntTree)))

> (module TYPEDtyped/racket
(require/typed 'UNTYPED
[nNatural ]
[#:structIntTree
([elem: Integer ]
[left: IntTree]
[right: IntTree])]))

The fourth case defines a new opaque type t using the function pred as a predicate. (Module m must provide pred and pred must have type (Any -> Boolean ).) The type t is defined as precisely those values that pred returns #t for. Opaque types must be required lexically before they are used.

Examples:

> (require/typed racket/base
[#:opaqueEvtevt? ]
[alarm-evt (Real -> Evt)]
[sync (Evt-> Any )])
> evt?

- : (-> Any Boolean : Evt)

#<procedure:evt?>
> (sync (alarm-evt (+ 100(current-inexact-milliseconds ))))

- : Any

#<alarm-evt>

The #:signature keyword registers the required signature in the signature environment. For more information on the use of signatures in Typed Racket see the documentation for typed/racket/unit.

In all cases, the identifiers are protected with contracts which enforce the specified types. If this contract fails, the module m is blamed.

Some types, notably the types of predicates such as number? , cannot be converted to contracts and raise a static error when used in a require/typed form. Here is an example of using case-> in require/typed .

(require/typed racket/base
[file-or-directory-modify-seconds
(case->
[String -> Exact-Nonnegative-Integer ]
[String (Option Exact-Nonnegative-Integer )
->
(U Exact-Nonnegative-Integer Void )]
[String (Option Exact-Nonnegative-Integer )(-> Any )
->
Any ])])

file-or-directory-modify-seconds has some arguments which are optional, so we need to use case-> .

Changed in version 1.4 of package typed-racket-lib: Added the #:type-name option.
Changed in version 1.6: Added syntax for struct type variables, only works in unsafe requires.
Changed in version 1.12: Added default type Any for omitted inst args.

syntax
( require/typed/provide mrt-clause...)

Similar to require/typed , but also provides the imported identifiers. Uses outside of a module top-level raise an error.

Examples:

> (module evtstyped/racket
(require/typed/provide racket/base
[#:opaqueEvtevt? ]
[alarm-evt (Real -> Evt)]
[sync (Evt-> Any )]))
> (require 'evts)
> (sync (alarm-evt (+ 100(current-inexact-milliseconds ))))

- : Any

#<alarm-evt>

2.10Other Forms🔗 i

syntax
with-handlers

Identical to with-handlers from racket/base but provides additional annotations to assist the typechecker.

syntax
with-handlers*

Identical to with-handlers* from racket/base but provides additional annotations to assist the typechecker.

Added in version 1.12 of package typed-racket-lib.

procedure
( default-continuation-prompt-tag )
→(-> (Prompt-Tagof Any (Any -> Any )))

Identical to default-continuation-prompt-tag , but additionally protects the resulting prompt tag with a contract that wraps higher-order values, such as functions, that are communicated with that prompt tag. If the wrapped value is used in untyped code, a contract error will be raised.

Examples:

> (module typedtyped/racket
(provide do-abort)
(: do-abort(-> Void ))
(define (do-abort)
(abort-current-continuation
;typed, and thus contracted, prompt tag
(default-continuation-prompt-tag )
(λ: ([x: Integer ])(+ 1x)))))

> (module untypedracket
(require 'typed)
(call-with-continuation-prompt
(λ ()(do-abort))
(default-continuation-prompt-tag )
;the function cannot be passed an argument
(λ (f)(f3))))
> (require 'untyped)

default-continuation-prompt-tag: broke its own contract

Attempted to use a higher-order value passed as `Any` in

untyped code: #<procedure>

in: the range of

(-> (prompt-tag/c Any #:call/cc Any))

contract from: untyped

blaming: untyped

(assuming the contract is correct)

syntax
( #%module-begin form...)

Legal only in a module begin context. The #%module-begin form of typed/racket checks all the forms in the module, using the Typed Racket type checking rules. All provide forms are rewritten to insert contracts where appropriate. Otherwise, the #%module-begin form of typed/racket behaves like #%module-begin from racket.

syntax
( #%top-interaction . form)

Performs type checking of forms entered at the read-eval-print loop. The #%top-interaction form also prints the type of form after type checking.

2.11Special Structure Type Properties🔗 i

value
prop:procedure :struct-type-property?

Unlike many other structure type properties, prop:procedure does not have predefined types for its property values. When a structure is assocatied with prop:procedure , its constructors’ return type is an intersection type of the structure type and a function type specified by the property value.

Examples:

> (struct animal([a: Number ][b: (-> Number Number )])
#:propertyprop:procedure
(struct-field-index b))
> (animal2add1 )

- : (∩ (-> Number Number) animal)

#<procedure:add1>

> (struct plant([a: Number ])
#:propertyprop:procedure
(lambda ([me: plant][a1: String ]): Number
(+ (plant-ame)(string-length a1))))
> (plant31)

- : (∩ (-> String Number) plant)

#<procedure:plant>

In other words, a variable that refers to a function is not allowed

Unlike in Racket, only one of the following types of expressions are allowed in Typed Racket: a nonnegative literal, (struct-index-fieldfield-name), or a lambda expression. Note that in the last case, if the type annotation on the codomain is not supplied, the type checker will use Any as the return type.

Similar to other structure type properties, when a structure’s base structure specifies a value for prop:procedure , the structure inherits that value if it does not specify its own.

Examples:

> (struct catanimal([c: Number ]))
> (cat2add1 42)

- : (∩ (-> Number Number) cat)

#<procedure:add1>
> (struct a-catcat())
> (a-cat2add1 42)

- : (∩ (-> Number Number) a-cat)

#<procedure:add1>

Function types for procedural structures do not enforce subtyping relations. A substructure can specify a different field index or a procedure that has a arity and/or types different from its base structures for prop:procedure .

Examples:

> (struct b-catcat([d: (-> Number String )])
#:propertyprop:procedure (struct-field-index d))
> (b-cat2add1 42number->string )

- : (∩ (-> Number String) b-cat)

#<procedure:number->string>

top ← prev up next →