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.1 Binding Forms
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 ...) . body)
(let loop maybe-ret (binding ...) . body)
binding = [var e] | [var : type e] maybe-tvars =
| #:forall (tvar ...) | #:∀ (tvar ...) maybe-ret =
| : type0
> (: filter-even (-> (Listof Natural) (Listof Natural) (Listof Natural)))
> (define (filter-even lst accum) (if (null? lst) accum (let ([first : Natural (car lst)] [rest : (Listof Natural) (cdr lst)]) (if (even? first) (filter-even rest (cons first accum)) (filter-even rest accum))))) > (filter-even (list 1 2 3 4 5 6) null) - : (Listof Nonnegative-Integer)
'(6 4 2)
> (: filter-even-loop (-> (Listof Natural) (Listof Natural)))
> (define (filter-even-loop lst) (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 (loop accum (cdr lst))]))) > (filter-even-loop (list 1 2 3 4)) - : (Listof Nonnegative-Integer)
'(4 2)
If polymorphic type variables are provided, they are bound in the type expressions for variable bindings.
> (let #:forall (A) ([x : A 0]) x) - : Integer [more precisely: Zero]
0
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)
2.2 Anonymous Functions
syntax
(lambda maybe-tvars formals maybe-ret . body)
formals = (formal ...) | (formal ... . rst) formal = var | [var default-expr] | [var : type] | [var : type default-expr] | keyword var | keyword [var : type] | keyword [var : type default-expr] rst = var | [var : type *] | [var : type ooo bound] maybe-tvars =
| #:forall (tvar ...) | #:∀ (tvar ...) | #:forall (tvar ... ooo) | #:∀ (tvar ... ooo) maybe-ret =
| : type
> (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:
> (lambda ([x : String "foo"]) (string-append x "bar")) - : (->* () (String) (String : (Top | Bot)))
#<procedure:eval:12:0>
> (lambda (#:x [x : String]) (string-append x "bar")) - : (-> #:x String String)
#<procedure:eval:13:0>
> (lambda (x #:y [y : Integer 0]) (add1 y)) - : (-> Any [#:y Integer] Integer)
#<procedure:eval:14:0>
> (lambda ([x 'default]) x) - : (->* () (Any) Any)
#<procedure:eval:15:0>
The lambda expression may also specify polymorphic type variables that are bound for the type expressions in the formals.
> (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.
> (lambda (x . rst) rst) - : (-> Any Any * (Listof Any))
#<procedure>
> (lambda (x rst : Integer *) rst) - : (-> Any Integer * (Listof Integer))
#<procedure>
> (lambda #:forall (A ...) (x rst : A ... A) rst) - : (All (A ...) (-> Any A ... A (List A ... A)))
#<procedure>
syntax
(λ formals . body)
syntax
(case-lambda maybe-tvars [formals body] ...)
Polymorphic type variables, if provided, are bound in the type expressions in the formals.
Note that each formals must have a different arity.
> (define add-map (case-lambda [([lst : (Listof Integer)]) (map add1 lst)] [([lst1 : (Listof Integer)] [lst2 : (Listof Integer)]) (map + lst1 lst2)]))
To see how to declare a type for add-map, see the case-> type constructor.
2.3 Loops
syntax
(for type-ann-maybe (for-clause ...) expr ...+)
type-ann-maybe =
| : u for-clause = [id : t seq-expr] | [(binding ...) seq-expr] | [id seq-expr] | #:when guard binding = id | [id : t]
syntax
(for/list type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hash type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hasheq type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hasheqv type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/vector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/or type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/sum type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/product type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/last type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/set type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/list type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hash type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hasheq type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hasheqv type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/vector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/or type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/sum type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/product type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/last type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/set type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/and type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/first type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/and type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/first type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/lists type-ann-maybe ([id : t] ... maybe-result) (for-clause ...) expr ...+)
syntax
(for/fold type-ann-maybe ([id : t init-expr] ... maybe-result) (for-clause ...) expr ...+)
maybe-result =
| #:result result-expr
Changed in version 1.11 of package typed-racket-lib: Added the #:result form.
syntax
(for* void-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/lists type-ann-maybe ([id : t] ... maybe-result) (for-clause ...) expr ...+)
syntax
(for*/fold type-ann-maybe ([id : t init-expr] ... maybe-result) (for-clause ...) expr ...+)
maybe-result =
| #:result result-expr
Changed in version 1.11 of package typed-racket-lib: Added the #:result form.
syntax
(do : u ([id : t init-expr step-expr-maybe] ...) (stop?-expr finish-expr ...) expr ...+)
step-expr-maybe =
| step-expr
2.4 Definitions
syntax
(define maybe-tvars v maybe-ann e)
(define maybe-tvars header maybe-ann . body)
header = (function-name . formals) | (header . formals) formals = (formal ...) | (formal ... . rst) formal = var | [var default-expr] | [var : type] | [var : type default-expr] | keyword var | keyword [var : type] | keyword [var : type default-expr] rst = var | [var : type *] | [var : type ooo bound] maybe-tvars =
| #:forall (tvar ...) | #:∀ (tvar ...) | #:forall (tvar ... ooo) | #:∀ (tvar ... ooo) maybe-ann =
| : type
The first form defines a variable v to the result of evaluating the expression e. The variable may have an optional type annotation.
If polymorphic type variables are provided, then they are bound for use in the type annotation.
> (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.
> (define (add [first : Integer] [rest : Integer]) : Integer (+ first rest))
> (define #:forall (A) (poly-app [func : (A A -> A)] [first : A] [rest : A]) : A (func first rest))
The function definition form also allows curried function arguments with corresponding type annotations.
Note that unlike define from racket/base, define does not bind functions with keyword arguments to static information about those functions.
2.5 Structure Definitions
syntax
(struct maybe-type-vars name-spec ([f : t] ...) options ...)
maybe-type-vars =
| (v ...) name-spec = name-id | name-id parent options = #:transparent | #:mutable | #:prefab | #:constructor-name constructor-id | #:extra-constructor-name constructor-id | #:property property-id property-expr | #:type-name type-id
> (struct camelia-sinensis ([age : Integer])) > (struct camelia-sinensis-assamica camelia-sinensis ())
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.
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.
> (struct a-prefab ([x : String]) #:prefab) > (:type a-prefab) (Prefab a-prefab String)
> (struct not-allowed a-prefab ()) eval:36: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-vars name-spec ([f : t] ...) options ...)
maybe-type-vars =
| (v ...) name-spec = name-id | name-id parent options = #:transparent | #:mutable | #:type-name type-id
Changed in version 1.4 of package typed-racket-lib: Added the #:type-name option.
syntax
(define-struct/exec name-spec ([f : t] ...) [e : proc-t] maybe-type-name)
name-spec = name-id | name-id parent maybe-type-name =
| #:type-name type-id
Changed in version 1.4 of package typed-racket-lib: Added the #:type-name option.
2.6 Names for Types
syntax
(define-type name t maybe-omit-def)
(define-type (name v ...) t maybe-omit-def)
maybe-omit-def = #:omit-define-syntaxes |
> (define-type IntStr (U Integer String)) > (define-type (ListofPairs A) (Listof (Pair A A)))
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.
> (define-type BT (U Number (Pair BT BT)))
> (let () (define-type (Even A) (U Null (Pairof A (Odd A)))) (define-type (Odd A) (Pairof A (Even A))) (: even-lst (Even Integer)) (define even-lst '(1 2)) even-lst) - : (Even Integer)
'(1 2)
However, the recursive reference may not occur immediately inside the type:
> (define-type Foo Foo) eval:41:0: Type Checker: Error in macro expansion -- parse
error in type;
recursive types are not allowed directly inside their
definition
in: Foo
> (define-type Bar (U Bar False)) eval:42:0: Type Checker: Error in macro expansion -- parse
error in type;
recursive types are not allowed directly inside their
definition
in: False
2.7 Generating Predicates Automatically
syntax
(make-predicate t)
syntax
(define-predicate name t)
2.8 Type Annotation and Instantiation
The second form allows type annotations to elide one level of parentheses for function types.
syntax
(provide: [v t] ...)
syntax
#{v : t}
If a dispatch macro on #\{ already exists in the current readtable, this syntax will be disabled.
syntax
(ann e t)
syntax
#{e :: t}
If a dispatch macro on #\{ already exists in the current readtable, this syntax will be disabled.
syntax
(cast e t)
> (cast 3 Integer) - : Integer
3
> (cast 3 String) broke its own contract
promised: string?
produced: 3
in: string?
contract from: cast
blaming: cast
(assuming the contract is correct)
at: eval:48.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.
> ((cast (lambda ([s : String]) s) (Any -> Any)) "hello") - : Any
"hello"
> ((cast (lambda ([s : String]) s) (Any -> Any)) 5) 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:52.0
> (foldl (inst cons Integer Integer) null (list 1 2 3 4)) - : (Listof Integer)
'(4 3 2 1)
> (: my-cons (All (A B) (-> A B (Pairof A B)))) > (define my-cons cons) > (: foldl-list : (All (α) (Listof α) -> (Listof α)))
> (define (foldl-list lst) (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-list lst) (foldr (inst my-cons α) null lst)) > (foldr-list (list "1" "2" "3" "4")) - : Any
'("1" "2" "3" "4")
> (: my-values : (All (A B ...) (A B ... -> (values A B ... B))))
> (define (my-values arg . args) (apply (inst values A B ... B) arg args))
syntax
(row-inst e row)
> (: id (All (r #:row) (-> (Class #:row-var r) (Class #:row-var r)))) > (define (id cls) cls)
> ((row-inst id (Row (field [x Integer]))) (class object% (super-new) (field [x : Integer 0]))) - : (Class (field (x Integer)))
#<class:eval:66:0>
syntax
#{e @ t ...}
syntax
#{e @ t ... t ooo bound}
2.9 Require
Here, m is a module spec, pred is an identifier naming a predicate, and maybe-renamed is an optionally-renamed identifier.
syntax
(require/typed m rt-clause ...)
rt-clause = [maybe-renamed t] |
[#:struct maybe-tvars name-id ([f : t] ...) struct-option ...] |
[#:struct maybe-tvars (name-id parent) ([f : t] ...) struct-option ...] | [#:opaque t pred] | [#:signature name ([id : t] ...)] maybe-renamed = id | (orig-id new-id) maybe-tvars =
| (type-variable ...) struct-option = #:constructor-name constructor-id | #:extra-constructor-name constructor-id | #:type-name type-id
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.
> (module UNTYPED racket/base (define n 100) (struct IntTree (elem left right)) (provide n (struct-out IntTree)))
> (module TYPED typed/racket (require/typed 'UNTYPED [n Natural] [#:struct IntTree ([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.
> (require/typed racket/base [#:opaque Evt evt?] [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 m rt-clause ...)
> (module evts typed/racket (require/typed/provide racket/base [#:opaque Evt evt?] [alarm-evt (Real -> Evt)] [sync (Evt -> Any)])) > (require 'evts) > (sync (alarm-evt (+ 100 (current-inexact-milliseconds)))) - : Any
#<alarm-evt>
2.10 Other Forms
syntax
syntax
Added in version 1.12 of package typed-racket-lib.
> (module typed typed/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]) (+ 1 x)))))
> (module untyped racket (require 'typed) (call-with-continuation-prompt (λ () (do-abort)) (default-continuation-prompt-tag) ; the function cannot be passed an argument (λ (f) (f 3)))) > (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 ...)
syntax
(#%top-interaction . form)