Use prefix -> in the TR Guide examples

Also some minor fixes like using the more common
case-> form rather than case-lambda.
This commit is contained in:
Asumu Takikawa 2014-02-14 17:12:36 -05:00
parent f59a122841
commit 1c5f6714a8
8 changed files with 55 additions and 54 deletions

View File

@ -36,18 +36,21 @@ form from @racketmodname[racket]---when porting a program from
@racketmodname[racket] to @racketmodname[typed/racket], uses of @racketmodname[racket] to @racketmodname[typed/racket], uses of
@racket[struct] should be changed to @racket[struct:]. @racket[struct] should be changed to @racket[struct:].
@racketblock[(: distance (pt pt -> Real))] @racketblock[(: distance (-> pt pt Real))]
This declares that @racket[distance] has the type @racket[(pt pt -> Real)]. This declares that @racket[distance] has the type @racket[(-> pt pt Real)].
@;{@racket[distance] must be defined at the top-level of the module containing @;{@racket[distance] must be defined at the top-level of the module containing
the declaration.} the declaration.}
The type @racket[(pt pt -> Real)] is a function type, that is, the type The type @racket[(-> pt pt Real)] is a function type, that is, the type
of a procedure. The input type, or domain, is two arguments of of a procedure. The input type, or domain, is two arguments of
type @racket[pt], which refers to an instance of the @racket[pt] type @racket[pt], which refers to an instance of the @racket[pt]
structure. The @racket[->] both indicates that this is a function structure. The @racket[->] indicates that this is a function
type and separates the domain from the range, or output type, in this type. The range type, or output type, is the last element in the
case @racket[Real]. function type, in this case @racket[Real].
If you are familiar with @rtech{contracts}, the notation for function
types is similar to function contract combinators.
@racketblock[ @racketblock[
(define (distance p1 p2) (define (distance p1 p2)
@ -75,13 +78,13 @@ typed/racket
(struct: leaf ([val : Number])) (struct: leaf ([val : Number]))
(struct: node ([left : Tree] [right : Tree])) (struct: node ([left : Tree] [right : Tree]))
(: tree-height (Tree -> Integer)) (: tree-height (-> Tree Integer))
(define (tree-height t) (define (tree-height t)
(cond [(leaf? t) 1] (cond [(leaf? t) 1]
[else (max (+ 1 (tree-height (node-left t))) [else (max (+ 1 (tree-height (node-left t)))
(+ 1 (tree-height (node-right t))))])) (+ 1 (tree-height (node-right t))))]))
(: tree-sum (Tree -> Number)) (: tree-sum (-> Tree Number))
(define (tree-sum t) (define (tree-sum t)
(cond [(leaf? t) (leaf-val t)] (cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t)) [else (+ (tree-sum (node-left t))

View File

@ -71,8 +71,8 @@ converted to a contract:
@interaction[#:eval the-eval @interaction[#:eval the-eval
(require/typed racket/base (require/typed racket/base
[object-name (case-> (Struct-Type-Property -> Symbol) [object-name (case-> (-> Struct-Type-Property Symbol)
(Regexp -> (U String Bytes)))]) (-> Regexp (U String Bytes)))])
] ]
This function type by cases is a valid type, but a corresponding This function type by cases is a valid type, but a corresponding
@ -85,8 +85,8 @@ of type precision at use sites:
@interaction[#:eval the-eval @interaction[#:eval the-eval
(require/typed racket/base (require/typed racket/base
[object-name ((U Struct-Type-Property Regexp) [object-name (-> (U Struct-Type-Property Regexp)
-> (U String Bytes Symbol))]) (U String Bytes Symbol))])
(object-name #rx"a regexp") (object-name #rx"a regexp")
] ]

View File

@ -50,7 +50,7 @@ in both top-level and internal contexts.
(define: (id [z : Number]) : Number z)] (define: (id [z : Number]) : Number z)]
Here, @racket[x] has the type @racket[Number], and @racket[id] has the Here, @racket[x] has the type @racket[Number], and @racket[id] has the
type @racket[(Number -> Number)]. In the body of @racket[id], type @racket[(-> Number Number)]. In the body of @racket[id],
@racket[z] has the type @racket[Number]. @racket[z] has the type @racket[Number].
@subsection{Annotating Local Binding} @subsection{Annotating Local Binding}
@ -87,14 +87,14 @@ of @racket[Number]s.
@racketblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))] @racketblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))]
This function has the type @racket[(String Number #,** -> Number)]. This function has the type @racket[(-> String Number #,** Number)].
Functions defined by cases may also be annotated: Functions defined by cases may also be annotated:
@racketblock[(case-lambda: [() 0] @racketblock[(case-lambda: [() 0]
[([x : Number]) x])] [([x : Number]) x])]
This function has the type This function has the type
@racket[(case-lambda (-> Number) (Number -> Number))]. @racket[(case-> (-> Number) (-> Number Number))].
@subsection{Annotating Single Variables} @subsection{Annotating Single Variables}
@ -152,7 +152,7 @@ values.
Here @racket[x] has the inferred type @racket[Integer], and @racket[y] Here @racket[x] has the inferred type @racket[Integer], and @racket[y]
has the inferred type @racket[(Listof Integer)]. The @racket[loop] has the inferred type @racket[(Listof Integer)]. The @racket[loop]
variable has type @racket[(Integer (Listof Integer) -> Integer)]. variable has type @racket[(-> Integer (Listof Integer) Integer)].
@subsection[#:tag "when-annotations?"]{When do you need type annotations?} @subsection[#:tag "when-annotations?"]{When do you need type annotations?}
@ -177,12 +177,12 @@ Here are examples that correspond to each of the cases above:
Example 1: Example 1:
@racketblock[ @racketblock[
(: fn (String -> Symbol)) (: fn (-> String Symbol))
(define (fn str) _...) (define (fn str) _...)
] ]
Example 2: Example 2:
@racketblock[ @racketblock[
(: fn (String -> Symbol)) (: fn (-> String Symbol))
(define fn (lambda (str) _...)) (define fn (lambda (str) _...))
] ]
Example 3: Example 3:
@ -204,9 +204,9 @@ type-check.
Any type can be given a name with @racket[define-type]. Any type can be given a name with @racket[define-type].
@racketblock[(define-type NN (Number -> Number))] @racketblock[(define-type NN (-> Number Number))]
Anywhere the name @racket[NN] is used, it is expanded to Anywhere the name @racket[NN] is used, it is expanded to
@racket[(Number -> Number)]. Type names may not be recursive. @racket[(-> Number Number)]. Type names may not be recursive.
@(close-eval the-eval) @(close-eval the-eval)

View File

@ -19,7 +19,7 @@ fails.
To illustrate, consider the following code: To illustrate, consider the following code:
@racketblock+eval[#:eval the-eval @racketblock+eval[#:eval the-eval
(: flexible-length ((U String (Listof Any)) -> Integer)) (: flexible-length (-> (U String (Listof Any)) Integer))
(define (flexible-length str-or-lst) (define (flexible-length str-or-lst)
(if (string? str-or-lst) (if (string? str-or-lst)
(string-length str-or-lst) (string-length str-or-lst)
@ -66,7 +66,7 @@ For example, consider the REPL's type printout for @racket[string?]:
@interaction[#:eval the-eval string?] @interaction[#:eval the-eval string?]
The type @racket[(Any -> Boolean : String)] has three parts. The first The type @racket[(-> Any Boolean : String)] has three parts. The first
two are the same as any other function type and indicate that the two are the same as any other function type and indicate that the
predicate takes any value and returns a boolean. The third part, after predicate takes any value and returns a boolean. The third part, after
the @racket[_:], is a @tech{filter} that tells the typechecker two the @racket[_:], is a @tech{filter} that tells the typechecker two
@ -94,7 +94,7 @@ For example, the @racket[_flexible-length] function from earlier can
be re-written to use @racket[cond] with no additional effort: be re-written to use @racket[cond] with no additional effort:
@racketblock+eval[#:eval the-eval @racketblock+eval[#:eval the-eval
(: flexible-length/cond ((U String (Listof Any)) -> Integer)) (: flexible-length/cond (-> (U String (Listof Any)) Integer))
(define (flexible-length/cond str-or-lst) (define (flexible-length/cond str-or-lst)
(cond [(string? str-or-lst) (string-length str-or-lst)] (cond [(string? str-or-lst) (string-length str-or-lst)]
[else (length str-or-lst)])) [else (length str-or-lst)]))

View File

@ -28,7 +28,7 @@ language:
typed/racket typed/racket
(struct: pt ([x : Real] [y : Real])) (struct: pt ([x : Real] [y : Real]))
(: distance (pt pt -> Real)) (: distance (-> pt pt Real))
(define (distance p1 p2) (define (distance p1 p2)
(sqrt (+ (sqr (- (pt-x p2) (pt-x p1))) (sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
(sqr (- (pt-y p2) (pt-y p1)))))) (sqr (- (pt-y p2) (pt-y p1))))))

View File

@ -47,7 +47,7 @@ typed/racket
(require/typed "distance.rkt" (require/typed "distance.rkt"
[#:struct pt ([x : Real] [y : Real])] [#:struct pt ([x : Real] [y : Real])]
[distance (pt pt -> Real)]) [distance (-> pt pt Real)])
(distance (pt 3 5) (p 7 0)) (distance (pt 3 5) (p 7 0))
] ]
@ -58,7 +58,7 @@ and allows us to use the structure type as if it were defined with
@racket[struct:]. @racket[struct:].
The second clause in the example above specifies that a given The second clause in the example above specifies that a given
binding @racket[_distance] has the given type @racket[(pt pt -> Real)]. binding @racket[_distance] has the given type @racket[(-> pt pt Real)].
Note that the @racket[require/typed] form can import bindings Note that the @racket[require/typed] form can import bindings
from any module, including those that are part of the Racket standard from any module, including those that are part of the Racket standard
@ -67,7 +67,7 @@ library. For example,
@racketmod[ @racketmod[
typed/racket typed/racket
(require/typed racket/base [add1 (Integer -> Integer)]) (require/typed racket/base [add1 (-> Integer Integer)])
] ]
is a valid use of the @racket[require/typed] form and imports @racket[add1] is a valid use of the @racket[require/typed] form and imports @racket[add1]
@ -113,14 +113,14 @@ and a typed module that uses it:
@interaction[#:eval the-eval @interaction[#:eval the-eval
(module client typed/racket (module client typed/racket
(require/typed 'increment [increment (Integer -> Integer)]) (require/typed 'increment [increment (-> Integer Integer)])
(increment 5)) (increment 5))
] ]
This combined program is not correct. All uses of @racket[_increment] This combined program is not correct. All uses of @racket[_increment]
in Typed Racket are correct under the assumption that the in Typed Racket are correct under the assumption that the
@racket[_increment] function upholds the @racket[(Integer -> Integer)] @racket[_increment] function upholds the @racket[(-> Integer Integer)]
type. Unfortunately, our @racket[_increment] implementation does not type. Unfortunately, our @racket[_increment] implementation does not
actually uphold this assumption, because the function actually produces actually uphold this assumption, because the function actually produces
strings. strings.

View File

@ -49,14 +49,14 @@ Finally, any value is itself a type:
@section{Function Types} @section{Function Types}
We have already seen some examples of function types. Function types We have already seen some examples of function types. Function types
are constructed using @racket[->], with the argument types before the are constructed using @racket[->], where the last type is the result
arrow and the result type after. Here are some example function type and the others are the argument types.
types: Here are some example function types:
@racketblock[ @racketblock[
(Number -> Number) (-> Number Number)
(String String -> Boolean) (-> String String Boolean)
(Char -> (values String Natural)) (-> Char (values String Natural))
] ]
The first type requires a @racket[Number] as input, and produces a The first type requires a @racket[Number] as input, and produces a
@ -121,7 +121,7 @@ a real number. Therefore, the following code is acceptable to the
type checker: type checker:
@racketblock[ @racketblock[
(: f (Real -> Real)) (: f (-> Real Real))
(define (f x) (* x 0.75)) (define (f x) (* x 0.75))
(: x Integer) (: x Integer)
@ -137,8 +137,8 @@ union, so @racket[String] is a subtype of @racket[(U String Number)].
One function type is a subtype of another if they have the same number One function type is a subtype of another if they have the same number
of arguments, the subtype's arguments are more permissive (is a supertype), and the of arguments, the subtype's arguments are more permissive (is a supertype), and the
subtype's result type is less permissive (is a subtype). subtype's result type is less permissive (is a subtype).
For example, @racket[(Any -> String)] is a subtype of @racket[(Number For example, @racket[(-> Any String)] is a subtype of @racket[(-> Number
-> (U String #f))]. (U String #f))].
@;@section{Occurrence Typing} @;@section{Occurrence Typing}
@ -155,7 +155,7 @@ written like this:
@racketmod[ @racketmod[
typed/racket typed/racket
(: sum-list ((Listof Number) -> Number)) (: sum-list (-> (Listof Number) Number))
(define (sum-list l) (define (sum-list l)
(cond [(null? l) 0] (cond [(null? l) 0]
[else (+ (car l) (sum-list (cdr l)))])) [else (+ (car l) (sum-list (cdr l)))]))
@ -178,7 +178,7 @@ typed/racket
(define-type (Opt a) (U None (Some a))) (define-type (Opt a) (U None (Some a)))
(: find (Number (Listof Number) -> (Opt Number))) (: find (-> Number (Listof Number) (Opt Number)))
(define (find v l) (define (find v l)
(cond [(null? l) (None)] (cond [(null? l) (None)]
[(= v (car l)) (Some v)] [(= v (car l)) (Some v)]
@ -220,7 +220,7 @@ write a function that takes the length of a list of numbers:
@racketmod[ @racketmod[
typed/racket typed/racket
(: list-number-length ((Listof Number) -> Integer)) (: list-number-length (-> (Listof Number) Integer))
(define (list-number-length l) (define (list-number-length l)
(if (null? l) (if (null? l)
0 0
@ -230,7 +230,7 @@ and also a function that takes the length of a list of strings:
@racketmod[ @racketmod[
typed/racket typed/racket
(: list-string-length ((Listof String) -> Integer)) (: list-string-length (-> (Listof String) Integer))
(define (list-string-length l) (define (list-string-length l)
(if (null? l) (if (null? l)
0 0
@ -245,7 +245,7 @@ We can abstract over the type of the element as follows:
@racketmod[ @racketmod[
typed/racket typed/racket
(: list-length (All (A) ((Listof A) -> Integer))) (: list-length (All (A) (-> (Listof A) Integer)))
(define (list-length l) (define (list-length l)
(if (null? l) (if (null? l)
0 0
@ -268,7 +268,7 @@ the type variable @racket[_a] to annotate the argument
@racket[_x]: @racket[_x]:
@racketblock[ @racketblock[
(: my-id (All (a) (a -> a))) (: my-id (All (a) (-> a a)))
(define my-id (lambda: ([x : a]) x)) (define my-id (lambda: ([x : a]) x))
] ]
@ -276,10 +276,10 @@ Lexical scope also implies that type variables can be shadowed,
such as in the following example: such as in the following example:
@racketblock[ @racketblock[
(: my-id (All (a) (a -> a))) (: my-id (All (a) (-> a a)))
(define my-id (define my-id
(lambda: ([x : a]) (lambda: ([x : a])
(: helper (All (a) (a -> a))) (: helper (All (a) (-> a a)))
(define helper (define helper
(lambda: ([y : a]) y)) (lambda: ([y : a]) y))
(helper x))) (helper x)))

View File

@ -31,7 +31,7 @@ We can define such functions in Typed Racket as well:
@racketmod[ @racketmod[
typed/racket typed/racket
(: sum (Number * -> Number)) (: sum (-> Number * Number))
(define (sum . xs) (define (sum . xs)
(if (null? xs) (if (null? xs)
0 0
@ -83,8 +83,7 @@ In Typed Racket, we can define @racket[fold-left] as follows:
typed/racket typed/racket
(: fold-left (: fold-left
(All (C A B ...) (All (C A B ...)
((C A B ... B -> C) C (Listof A) (Listof B) ... B (-> (-> C A B ... B C) C (Listof A) (Listof B) ... B
->
C))) C)))
(define (fold-left f i as . bss) (define (fold-left f i as . bss)
(if (or (null? as) (if (or (null? as)
@ -110,7 +109,6 @@ replaced with the corresponding type from the sequence.
So the type of @racket[(inst fold-left Integer Boolean String Number)] So the type of @racket[(inst fold-left Integer Boolean String Number)]
is is
@racket[((Integer Boolean String Number -> Integer) @racket[(-> (-> Integer Boolean String Number Integer)
Integer (Listof Boolean) (Listof String) (Listof Number) Integer (Listof Boolean) (Listof String) (Listof Number)
->
Integer)]. Integer)].