suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add docs for TR's filter syntax

Browse Source 
original commit: f638247b26c35efb7cbc3f501a32781a905128f8
This commit is contained in:
Asumu Takikawa 2014-04-28 17:17:23 -04:00
parent 9d7f92fbb7
commit 129f632e04
1 changed files with 53 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
View File

@ -526,22 +526,40 @@ functions and continuation mark functions.
@section{Other Type Constructors}
@defform*/subs[#:id -> #:literals (* ...)
[(-> dom ... rng)
@defform*/subs[#:id -> #:literals (|@| * ... ! and or implies car cdr)
[(-> dom ... rng optional-filter)
(-> dom ... rest * rng)
(-> dom ... rest ooo bound rng)
(-> dom rng : pred)
(dom ... -> rng)
(dom ... -> rng optional-filter)
(dom ... rest * -> rng)
(dom ... rest ooo bound -> rng)
(dom -> rng : pred)]
(dom ... rest ooo bound -> rng)]
([ooo #,(racket ...)]
[dom type
mandatory-kw
optional-kw]
[mandatory-kw (code:line keyword type)]
[optional-kw [keyword type]])]{
[optional-kw [keyword type]]
[optional-filter (code:line)
(code:line : type)
(code:line : pos-filter neg-filter object)]
[pos-filter (code:line)
(code:line #:+ proposition ...)]
[neg-filter (code:line)
(code:line #:- proposition ...)]
[object (code:line)
(code:line #:object index)]
[proposition type
(! type)
(type |@| path-elem ... index)
(! type |@| path-elem ... index)
(and proposition ...)
(or proposition ...)
(implies proposition ...)]
[path-elem car cdr]
[index positive-integer
(positive-integer positive-integer)
identifier])]{
The type of functions from the (possibly-empty)
sequence @racket[dom ....] to the @racket[rng] type.
@ -559,13 +577,6 @@ functions and continuation mark functions.
In the third form, the @racket[...] introduced by @racket[ooo] is literal,
and @racket[bound] must be an identifier denoting a type variable.
In the fourth form, there must be only one @racket[dom] and @racket[pred] is the type
checked by the predicate. The type @racket[pred] is known as a @emph{filter} for
the function type (for an introduction to filters, see
@tr-guide-secref["filters-and-predicates"]).
@ex[string?]
The @racket[dom]s can include both mandatory and optional keyword arguments.
Mandatory keyword arguments are a pair of keyword and type, while optional
arguments are surrounded by a pair of parentheses.
@ -577,9 +588,35 @@ functions and continuation mark functions.
(is-zero? 2 #:equality =)
(is-zero? 2 #:equality eq? #:zero 2.0)]
When @racket[optional-filter] is provided, it specifies the @emph{filter} for the
function type (for an introduction to filters, see @tr-guide-secref["filters-and-predicates"]).
For almost all use cases, only the simplest form of filters, with a single type after a
@racket[:], are necessary:
@ex[string?]
The filter specifies that when @racket[(string? x)] evaluates to a true value, the
variable @racket[x] can be assumed to have type @racket[String]. Likewise, if the
expression evaluates to @racket[#f], the variable has type @racket[String].
In some cases, asymmetric type information is useful in filters. For example, the
@racket[filter] function's first argument is specified with only a positive filter:
@ex[filter]
The use of @racket[#:+] indicates that when the function applied to a variable
evaluates to a true value, the given type can be assumed for the variable. However,
the type-checker gains no information in branches in which the result is @racket[#f].
Conversely, @racket[#:-] specifies that a function provides information for the
false branch of a conditional.
The other filter proposition cases are rarely needed, but the grammar documents them
for completeness. They correspond to logical operations on the propositions.
The type of functions can also be specified with an @emph{infix} @racket[->]
which comes immediately before the @racket[rng] type. The fifth through
eighth forms match the first four cases, but with the infix style of arrow.
which comes immediately before the @racket[rng] type. The fourth through
sixth forms match the first three cases, but with the infix style of arrow.
@ex[(: add2 (Number -> Number))
(define (add2 n) (+ n 2))]