Convert TR docs to use scribble/example

This commit is contained in:
Asumu Takikawa 2015-12-12 17:47:06 -05:00
parent b18d940f1a
commit f08f3d07d4
17 changed files with 130 additions and 116 deletions

View File

@ -10,7 +10,7 @@
"r6rs-lib"
"sandbox-lib"
"at-exp-lib"
"scribble-lib"
("scribble-lib" #:version "1.16")
"pict-lib"
("typed-racket-lib" #:version "1.3")
"typed-racket-compatibility"

View File

@ -1,6 +1,7 @@
#lang scribble/manual
@begin[(require (for-label (only-meta-in 0 typed/racket)) scribble/eval
@begin[(require (for-label (only-meta-in 0 typed/racket))
scribble/example
"../utils.rkt" (only-in "quick.scrbl" typed-mod))]
@(define the-eval (make-base-eval))
@ -23,7 +24,7 @@ are provided as well; for example, the
@racketmodname[typed/racket/base] language corresponds to
@racketmodname[racket/base].
@racketblock+eval[#:eval the-eval (struct pt ([x : Real] [y : Real]))]
@examples[#:no-result #:eval the-eval (struct pt ([x : Real] [y : Real]))]
@margin-note{Typed Racket provides modified versions of core Racket forms,
which permit type annotations. Previous versions of Typed Racket provided
@ -38,7 +39,7 @@ This defines a new structure, named @racket[pt], with two fields,
@racketmodname[racket] to @racketmodname[typed/racket], simply add
type annotations to existing field declarations.
@racketblock+eval[#:eval the-eval (: distance (-> pt pt Real))]
@examples[#:no-result #:eval the-eval (: distance (-> 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
@ -54,7 +55,7 @@ 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+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(define (distance p1 p2)
(sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
(sqr (- (pt-y p2) (pt-y p1))))))
@ -71,14 +72,14 @@ the program is accepted.
In the Typed Racket @gtech{REPL}, calling @racket[distance] will
show the result as usual and will also print the result's type:
@interaction[#:eval the-eval (distance (pt 0 0) (pt 3.1415 2.7172))]
@examples[#:label #f #:eval the-eval (distance (pt 0 0) (pt 3.1415 2.7172))]
Just evaluating the function name will print the function value and its type,
which can be useful for discovering the types that Typed Racket ascribes to
Racket functions. Alternatively, the @racket[:print-type] command will just
print the type:
@interaction[#:eval the-eval distance string-length (:print-type string-ref)]
@examples[#:label #f #:eval the-eval distance string-length (:print-type string-ref)]
@section{Datatypes and Unions}
@ -141,14 +142,14 @@ When Typed Racket detects a type error in the module, it raises an
error before running the program.
@examples[#:eval the-eval
(add1 "not a number")
(eval:error (add1 "not a number"))
]
@;{
Typed Racket also attempts to detect more than one error in the module.
@examples[#:eval the-eval
(string-append "a string" (add1 "not a number"))
(eval:error (string-append "a string" (add1 "not a number")))
]
}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@(require "../utils.rkt"
scribble/eval
scribble/example
(for-label (only-meta-in 0 typed/racket)))
@(define the-eval (make-base-eval))
@ -38,19 +38,19 @@ on higher-order arguments that are themselves polymorphic.
For example, the following program results in a type error
that demonstrates this limitation:
@interaction[#:eval the-eval
(map cons '(a b c d) '(1 2 3 4))
@examples[#:label #f #:eval the-eval
(eval:error (map cons '(a b c d) '(1 2 3 4)))
]
The issue is that the type of @racket[cons] is also polymorphic:
@interaction[#:eval the-eval cons]
@examples[#:label #f #:eval the-eval cons]
To make this expression type-check, the @racket[inst] form can
be used to instantiate the polymorphic argument (e.g., @racket[cons])
at a specific type:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(map (inst cons Symbol Integer) '(a b c d) '(1 2 3 4))
]
@ -69,10 +69,11 @@ fixed in a future release.
The following illustrates an example type that cannot be
converted to a contract:
@interaction[#:eval the-eval
(require/typed racket/base
[object-name (case-> (-> Struct-Type-Property Symbol)
(-> Regexp (U String Bytes)))])
@examples[#:label #f #:eval the-eval
(eval:error
(require/typed racket/base
[object-name (case-> (-> Struct-Type-Property Symbol)
(-> Regexp (U String Bytes)))]))
]
This function type by cases is a valid type, but a corresponding
@ -83,7 +84,7 @@ supported with dependent contracts.
A more approximate type will work for this case, but with a loss
of type precision at use sites:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(require/typed racket/base
[object-name (-> (U Struct-Type-Property Regexp)
(U String Bytes Symbol))])
@ -94,8 +95,8 @@ Use of @racket[define-predicate] also involves contract generation, and
so some types cannot have predicates generated for them. The following
illustrates a type for which a predicate can't be generated:
@interaction[#:eval the-eval
(define-predicate p? (All (A) (Listof A)))]
@examples[#:label #f #:eval the-eval
(eval:error (define-predicate p? (All (A) (Listof A))))]
@section{Unsupported features}
@ -109,7 +110,7 @@ To make programming with invariant type constructors (such as @racket[Boxof])
easier, Typed Racket generalizes types that are used as arguments to invariant
type constructors. For example:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
0
(define b (box 0))
b
@ -123,7 +124,7 @@ initialize it with @racket[0]. Type generalization does exactly that.
In some cases, however, type generalization can lead to unexpected results:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(box (ann 1 Fixnum))
]
@ -131,7 +132,7 @@ The intent of this code may be to create of box of @racket[Fixnum], but Typed
Racket will generalize it anyway. To create a box of @racket[Fixnum], the box
itself should have a type annotation:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(ann (box 1) (Boxof Fixnum))
((inst box Fixnum) 1)
]
@ -146,22 +147,24 @@ occur inside macros---are not checked.
Concretely, this means that expressions inside, for example, a
@racket[begin-for-syntax] block are not checked:
@interaction[#:eval the-eval
(begin-for-syntax (+ 1 "foo"))
@examples[#:label #f #:eval the-eval
(eval:error (begin-for-syntax (+ 1 "foo")))
]
Similarly, expressions inside of macros defined in Typed Racket are
not type-checked. On the other hand, the macro's expansion is always
type-checked:
@defs+int[#:eval the-eval
((define-syntax (example-1 stx)
@examples[#:label #f #:eval the-eval
(eval:no-prompt
(define-syntax (example-1 stx)
(+ 1 "foo")
#'1)
#'1))
(eval:no-prompt
(define-syntax (example-2 stx)
#'(+ 1 "foo")))
(example-1)
(example-2)
(eval:error (example-1))
(eval:error (example-2))
]
Note that functions defined in Typed Racket that are used at

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/eval
scribble/core scribble/example
(for-label (only-meta-in 0 typed/racket)
(prefix-in base: racket)))]
@ -127,8 +127,8 @@ This ensures that the expression, here @racket[(+ 7 1)], has the
desired type, here @racket[Number]. Otherwise, the type checker
signals an error. For example:
@interaction[#:eval the-eval
(ann "not a number" Number)]
@examples[#:label #f #:eval the-eval
(eval:error (ann "not a number" Number))]
@section{Type Inference}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/eval
scribble/core scribble/example
(for-label (only-meta-in 0 typed/racket)))]
@(define the-eval (make-base-eval))
@ -18,7 +18,7 @@ fails.
To illustrate, consider the following code:
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: flexible-length (-> (U String (Listof Any)) Integer))
(define (flexible-length str-or-lst)
(if (string? str-or-lst)
@ -64,7 +64,7 @@ information is gained when a predicate check succeeds or fails.
For example, consider the REPL's type printout for @racket[string?]:
@interaction[#:eval the-eval string?]
@examples[#:label #f #:eval the-eval string?]
The type @racket[(-> Any Boolean : String)] has three parts. The first
two are the same as any other function type and indicate that the
@ -93,7 +93,7 @@ control flow constructs that are present in Racket such as
For example, the @racket[_flexible-length] function from earlier can
be re-written to use @racket[cond] with no additional effort:
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: flexible-length/cond (-> (U String (Listof Any)) Integer))
(define (flexible-length/cond str-or-lst)
(cond [(string? str-or-lst) (string-length str-or-lst)]
@ -104,13 +104,13 @@ In some cases, the type system does not have enough information or is
too conservative to typecheck an expression. For example, consider
the following interaction:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(: a Positive-Integer)
(define a 15)
(: b Positive-Integer)
(define b 20)
(: c Positive-Integer)
(define c (- b a))
(eval:error (define c (- b a)))
]
In this case, the type system only knows that @racket[_a] and
@ -119,7 +119,7 @@ difference will always be positive in defining @racket[_c]. In cases
like this, occurrence typing can be used to make the code type-check
using an @emph{assertion}. For example,
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: d Positive-Integer)
(define d (assert (- b a) positive?))
]
@ -133,7 +133,7 @@ Note that @racket[assert] is a derived concept in Typed Racket and is
a natural consequence of occurrence typing. The assertion above is
essentially equivalent to the following:
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: e Positive-Integer)
(define e (let ([diff (- b a)])
(if (positive? diff)
@ -165,7 +165,7 @@ by let-expressions alias other values (e.g. when they alias non-mutated identifi
This allows programs which explicitly rely on occurrence typing and aliasing to
typecheck:
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: f (Any -> Number))
(define (f x)
(let ([y x])
@ -180,7 +180,7 @@ typecheck:
It also allows the typechecker to check programs which use macros
that heavily rely on let-bindings internally (such as @racket[match]):
@racketblock+eval[#:eval the-eval
@examples[#:no-result #:eval the-eval
(: g (Any -> Number))
(define (g x)
(match x

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@(require "../utils.rkt"
scribble/eval
scribble/example
(for-label (only-meta-in 0 typed/racket)))
@(define the-eval (make-base-eval))
@ -100,7 +100,7 @@ function:
@margin-note{For general information on Racket's contract system
, see @secref[#:doc '(lib "scribblings/guide/guide.scrbl")]{contracts}.}
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(module increment racket
(provide increment)
@ -110,7 +110,7 @@ function:
and a typed module that uses it:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(module client typed/racket
(require/typed 'increment [increment (-> Integer Integer)])
@ -127,7 +127,7 @@ strings.
On the other hand, when the program is run:
@interaction[#:eval the-eval (require 'client)]
@examples[#:label #f #:eval the-eval (eval:error (require 'client))]
we find that the contract system checks the assumption made by the typed
module and correctly finds that the assumption failed because of the

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/eval
scribble/core scribble/example
(for-label (only-meta-in 0 typed/racket)))]
@(define the-eval (make-base-eval))
@ -18,7 +18,7 @@ The most basic types in Typed Racket are those for primitive data,
such as @racket[True] and @racket[False] for booleans, @racket[String]
for strings, and @racket[Char] for characters.
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
'"hello, world"
#\f
#t
@ -27,14 +27,14 @@ for strings, and @racket[Char] for characters.
Each symbol is given a unique type containing only that symbol. The
@racket[Symbol] type includes all symbols.
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
'foo
'bar]
Typed Racket also provides a rich hierarchy for describing particular
kinds of numbers.
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
0
-7
14
@ -43,7 +43,7 @@ kinds of numbers.
Finally, any value is itself a type:
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(ann 23 23)]
@section{Function Types}
@ -65,7 +65,7 @@ one argument, and produces @rtech{multiple values}, of types
@racket[String] and @racket[Natural]. Here are example functions for
each of these types.
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(lambda ([x : Number]) x)
(lambda ([a : String] [b : String]) (equal? a b))
(lambda ([c : Char]) (values (string c) (char->integer c)))]
@ -106,7 +106,7 @@ The result is two values of type @racket[Number].
Sometimes a value can be one of several types. To specify this, we
can use a union type, written with the type constructor @racket[U].
@interaction[#:eval the-eval
@examples[#:label #f #:eval the-eval
(let ([a-number 37])
(if (even? a-number)
'yes
@ -141,9 +141,9 @@ type defintion could also be written like this.
Of course, types which directly refer to themselves are not
permitted. For example, both of these definitions are illegal.
@interaction[#:eval the-eval
(define-type BinaryTree BinaryTree)
(define-type BinaryTree (U Number BinaryTree))]
@examples[#:label #f #:eval the-eval
(eval:error (define-type BinaryTree BinaryTree))
(eval:error (define-type BinaryTree (U Number BinaryTree)))]
@section{Structure Types}

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval)
@begin[(require "../utils.rkt" scribble/example)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-top-eval (make-base-eval #:lang 'typed/racket))

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt")
(require scribble/eval)
(require scribble/example)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-top-eval (make-base-eval))

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt")
(require scribble/eval
(require scribble/example
(for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket])
(only-in racket/base)))]
@ -417,7 +417,7 @@ structure type cannot extend a prefab structure type.
@ex[
(struct a-prefab ([x : String]) #:prefab)
(:type a-prefab)
(struct not-allowed a-prefab ())
(eval:error (struct not-allowed a-prefab ()))
]
}
@ -468,8 +468,8 @@ back to itself.
However, the recursive reference may not occur immediately inside
the type:
@ex[(define-type Foo Foo)
(define-type Bar (U Bar False))]
@ex[(eval:error (define-type Foo Foo))
(eval:error (define-type Bar (U Bar False)))]
}
@section{Generating Predicates Automatically}
@ -526,7 +526,7 @@ returned by @racket[e], protected by a contract ensuring that it has type
@racket[t]. This is legal only in expression contexts.
@ex[(cast 3 Integer)
(cast 3 String)
(eval:error (cast 3 String))
(cast (lambda: ([x : Any]) x) (String -> String))
]
}

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))
@ -127,9 +127,10 @@ additional provides all other bindings from @racketmodname[racket/class].
class form's clauses) are restricted.
@ex[
(class object%
(code:comment "Note the missing `super-new`")
(init-field [x : Real 0] [y : Real 0]))
(eval:error
(class object%
(code:comment "Note the missing `super-new`")
(init-field [x : Real 0] [y : Real 0])))
]
If any identifier with an optional type annotation is left without an

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))
@ -35,19 +35,21 @@ have the types ascribed to them; these types are converted to contracts and chec
@examples[#:eval the-eval
(with-type #:result Number 3)
((with-type #:result (Number -> Number)
(lambda: ([x : Number]) (add1 x)))
#f)
(eval:error
((with-type #:result (Number -> Number)
(lambda: ([x : Number]) (add1 x)))
#f))
(let ([x "hello"])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world")))
(let ([x 'hello])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world")))
(eval:error
(let ([x 'hello])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world"))))
(with-type ([fun (Number -> Number)]
[val Number])

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for]))
(for-label (only-in racket/unit tag unit/c)))]
@ -290,11 +290,12 @@ not present in the signature environment.
(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:error
(module TYPED-2 typed/racket
(require/typed 'UNTYPED-2
[#:signature a-sub^
([a1 : Integer]
[a2 : String])])))]
Requiring a signature from an untyped module that contains variable definitions is an error
@ -305,11 +306,12 @@ in Typed 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:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^
([bad : (Pairof Integer Integer)]
[bad-ref : Integer])])))]
@ -331,9 +333,10 @@ signature that contains definitions in a typed module will result in an error.
@ex[(module UNTYPED racket
(provide bad^)
(define-signature bad^ ((define-values (bad) 13))))
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^ ([bad : Integer])]))]
(eval:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^ ([bad : Integer])])))]
@subsection{Contracts and Unit Static Information}
Unit values that flow between typed and untyped contexts are wrapped in
@ -347,10 +350,11 @@ 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:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[u@ (Unit (import) (export) String)])
(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
@ -361,9 +365,10 @@ typed unit is disallowed in untyped contexts.
(module TYPED typed/racket
(provide u@)
(define-unit u@ (import) (export) "Hello!"))
(module UNTYPED racket
(require 'TYPED)
u@)]
(eval:error
(module UNTYPED racket
(require 'TYPED)
u@))]
@subsection{Signatures and Internal Definition Contexts}
Typed Racket's @racket[define-signature] form is allowed in both top-level and
@ -371,13 +376,14 @@ internal definition contexts. As the following example shows, defining
signatures in internal definiition contexts can be problematic.
@ex[
(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:error
(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^))))]
Even though the unit imports a signature named @racket[a^], the @racket[a^]
provided for the import refers to the top-level @racket[a^] signature and the

View File

@ -2,7 +2,7 @@
@begin[(require "../utils.rkt"
"numeric-tower-pict.rkt"
scribble/eval
scribble/example
racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])
racket/async-channel))]
@ -722,7 +722,7 @@ functions and continuation mark functions.
@ex[
(: my-list Procedure)
(define my-list list)
(my-list "zwiebelkuchen" "socca")
(eval:error (my-list "zwiebelkuchen" "socca"))
]
}

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@(require scribble/eval
@(require scribble/example
(for-label (only-meta-in 0 [except-in typed/racket for])))
@(define eval (make-base-eval))
@ -55,7 +55,7 @@ behavior and may even crash Typed Racket.
(code:comment "bad call that's unchecked")
(f "foo"))
(require 'u)
(eval:error (require 'u))
]
@history[#:added "1.3"]

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])
typed/untyped-utils))]
@ -30,7 +30,7 @@ x
(define: y : (U String Symbol) "hello")
y
(assert y string?)
(assert y boolean?)]
(eval:error (assert y boolean?))]
@defform*/subs[[(with-asserts ([id maybe-pred] ...) body ...+)]
([maybe-pred code:blank
@ -64,10 +64,11 @@ the error message.
#`(cond clause ... [else (typecheck-fail #,stx "incomplete coverage"
#:covered-id x)])]))
(define: (f [x : (U String Integer)]) : Boolean
(cond* x
[(string? x) #t]
[(exact-nonnegative-integer? x) #f]))
(eval:error
(define: (f [x : (U String Integer)]) : Boolean
(cond* x
[(string? x) #t]
[(exact-nonnegative-integer? x) #f])))
]
}