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

rackety TS docs

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-09 12:35:59 -04:00
parent 820040abc1
commit 9ccd44e8fd
8 changed files with 340 additions and 614 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/scribblings/guide/dialects.scrbl
View File

@ -97,7 +97,7 @@ including the following:
@itemize[ @itemize[
@item{@racketmodname[typed/scheme] --- like @item{@racketmodname[typed/racket] --- like
@racketmodname[racket], but statically typed; see @racketmodname[racket], but statically typed; see
@other-manual['(lib "typed-scheme/scribblings/ts-guide.scrbl")]} @other-manual['(lib "typed-scheme/scribblings/ts-guide.scrbl")]}

104
collects/typed-scheme/scribblings/begin.scrbl
View File

@ -1,12 +1,12 @@
#lang scribble/manual #lang scribble/manual
@begin[(require (for-label (only-meta-in 0 typed/scheme)) scribble/eval @begin[(require (for-label (only-meta-in 0 typed/racket)) scribble/eval
"utils.ss" (only-in "quick.scrbl" typed-mod))] "utils.ss" (only-in "quick.scrbl" typed-mod))]
@(define the-eval (make-base-eval)) @(define the-eval (make-base-eval))
@(the-eval '(require typed/scheme)) @(the-eval '(require typed/racket))
@title[#:tag "beginning"]{Beginning Typed Scheme} @title[#:tag "beginning"]{Beginning Typed Racket}
Recall the typed module from @secref["quick"]: Recall the typed module from @secref["quick"]:
@ -14,62 +14,62 @@ Recall the typed module from @secref["quick"]:
Let us consider each element of this program in turn. Let us consider each element of this program in turn.
@schememod[typed/scheme] @racketmod[typed/racket]
This specifies that the module is written in the This specifies that the module is written in the
@schememodname[typed/scheme] language, which is a typed version of the @racketmodname[typed/racket] language, which is a typed version of the
@schememodname[scheme] language. Typed versions of other languages @racketmodname[racket] language. Typed versions of other languages
are provided as well; for example, the are provided as well; for example, the
@schememodname[typed/scheme/base] language corresponds to @racketmodname[typed/racket/base] language corresponds to
@schememodname[scheme/base]. @racketmodname[racket/base].
@schemeblock[(define-struct: pt ([x : Real] [y : Real]))] @racketblock[(define-struct: pt ([x : Real] [y : Real]))]
@margin-note{Many forms in Typed Scheme have the same name as the @margin-note{Many forms in Typed Racket have the same name as the
untyped forms, with a @scheme[:] suffix.} untyped forms, with a @racket[:] suffix.}
This defines a new structure, name @scheme[pt], with two fields, This defines a new structure, name @racket[pt], with two fields,
@scheme[x] and @scheme[y]. Both fields are specified to have the type @racket[x] and @racket[y]. Both fields are specified to have the type
@scheme[Real], which corresponds to the @rtech{real numbers}. @racket[Real], which corresponds to the @rtech{real numbers}.
The The
@scheme[define-struct:] form corresponds to the @scheme[define-struct] @racket[define-struct:] form corresponds to the @racket[define-struct]
form from @schememodname[scheme]---when porting a program from form from @racketmodname[racket]---when porting a program from
@schememodname[scheme] to @schememodname[typed/scheme], uses of @racketmodname[racket] to @racketmodname[typed/racket], uses of
@scheme[define-struct] should be changed to @scheme[define-struct:]. @racket[define-struct] should be changed to @racket[define-struct:].
@schemeblock[(: mag (pt -> Number))] @racketblock[(: mag (pt -> Number))]
This declares that @scheme[mag] has the type @scheme[(pt -> Number)]. This declares that @racket[mag] has the type @racket[(pt -> Number)].
@;{@scheme[mag] must be defined at the top-level of the module containing @;{@racket[mag] must be defined at the top-level of the module containing
the declaration.} the declaration.}
The type @scheme[(pt -> Number)] is a function type, that is, the type The type @racket[(pt -> Number)] is a function type, that is, the type
of a procedure. The input type, or domain, is a single argument of of a procedure. The input type, or domain, is a single argument of
type @scheme[pt], which refers to an instance of the @scheme[pt] type @racket[pt], which refers to an instance of the @racket[pt]
structure. The @scheme[->] both indicates that this is a function structure. The @racket[->] both indicates that this is a function
type and separates the domain from the range, or output type, in this type and separates the domain from the range, or output type, in this
case @scheme[Number]. case @racket[Number].
@schemeblock[ @racketblock[
(define (mag p) (define (mag p)
(sqrt (+ (sqr (pt-x p)) (sqr (pt-y p))))) (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
] ]
This definition is unchanged from the untyped version of the code. This definition is unchanged from the untyped version of the code.
The goal of Typed Scheme is to allow almost all definitions to be The goal of Typed Racket is to allow almost all definitions to be
typechecked without change. The typechecker verifies that the body of typechecked without change. The typechecker verifies that the body of
the function has the type @scheme[Real], under the assumption that the function has the type @racket[Real], under the assumption that
@scheme[p] has the type @scheme[pt], taking these types from the @racket[p] has the type @racket[pt], taking these types from the
earlier type declaration. Since the body does have this type, the earlier type declaration. Since the body does have this type, the
program is accepted. program is accepted.
@section{Datatypes and Unions} @section{Datatypes and Unions}
Many data structures involve multiple variants. In Typed Scheme, we Many data structures involve multiple variants. In Typed Racket, we
represent these using @italic{union types}, written @scheme[(U t1 t2 ...)]. represent these using @italic{union types}, written @racket[(U t1 t2 ...)].
@schememod[ @racketmod[
typed/scheme typed/racket
(define-type Tree (U leaf node)) (define-type Tree (U leaf node))
(define-struct: leaf ([val : Number])) (define-struct: leaf ([val : Number]))
(define-struct: node ([left : Tree] [right : Tree])) (define-struct: node ([left : Tree] [right : Tree]))
@ -87,36 +87,36 @@ typed/scheme
(tree-sum (node-right t)))])) (tree-sum (node-right t)))]))
] ]
In this module, we have defined two new datatypes: @scheme[leaf] and In this module, we have defined two new datatypes: @racket[leaf] and
@scheme[node]. We've also defined the type name @scheme[Tree] to be @racket[node]. We've also defined the type name @racket[Tree] to be
@scheme[(U node leaf)], which represents a binary tree of numbers. In @racket[(U node leaf)], which represents a binary tree of numbers. In
essence, we are saying that the @scheme[tree-height] function accepts essence, we are saying that the @racket[tree-height] function accepts
a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf], a @racket[Tree], which is either a @racket[node] or a @racket[leaf],
and produces a number. and produces a number.
In order to calculate interesting facts about trees, we have to take In order to calculate interesting facts about trees, we have to take
them apart and get at their contents. But since accessors such as them apart and get at their contents. But since accessors such as
@scheme[node-left] require a @scheme[node] as input, not a @racket[node-left] require a @racket[node] as input, not a
@scheme[Tree], we have to determine which kind of input we @racket[Tree], we have to determine which kind of input we
were passed. were passed.
For this purpose, we use the predicates that come with each defined For this purpose, we use the predicates that come with each defined
structure. For example, the @scheme[leaf?] predicate distinguishes structure. For example, the @racket[leaf?] predicate distinguishes
@scheme[leaf]s from all other Typed Scheme values. Therefore, in the @racket[leaf]s from all other Typed Racket values. Therefore, in the
first branch of the @scheme[cond] clause in @scheme[tree-sum], we know first branch of the @racket[cond] clause in @racket[tree-sum], we know
that @scheme[t] is a @scheme[leaf], and therefore we can get its value that @racket[t] is a @racket[leaf], and therefore we can get its value
with the @scheme[leaf-val] function. with the @racket[leaf-val] function.
In the else clauses of both functions, we know that @scheme[t] is not In the else clauses of both functions, we know that @racket[t] is not
a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by a @racket[leaf], and since the type of @racket[t] was @racket[Tree] by
process of elimination we can determine that @scheme[t] must be a process of elimination we can determine that @racket[t] must be a
@scheme[node]. Therefore, we can use accessors such as @racket[node]. Therefore, we can use accessors such as
@scheme[node-left] and @scheme[node-right] with @scheme[t] as input. @racket[node-left] and @racket[node-right] with @racket[t] as input.
@section{Type Errors} @section{Type Errors}
When Typed Scheme detects a type error in the module, it raises an When Typed Racket detects a type error in the module, it raises an
error before running the program. error before running the program.
@examples[#:eval the-eval @examples[#:eval the-eval
@ -124,7 +124,7 @@ error before running the program.
] ]
@;{ @;{
Typed Scheme also attempts to detect more than one error in the module. Typed Racket also attempts to detect more than one error in the module.
@examples[#:eval the-eval @examples[#:eval the-eval
(string-append "a string" (add1 "not a number")) (string-append "a string" (add1 "not a number"))

106
collects/typed-scheme/scribblings/more.scrbl
View File

@ -2,109 +2,109 @@
@begin[(require "utils.ss" @begin[(require "utils.ss"
scribble/core scribble/eval scribble/core scribble/eval
(for-label (only-meta-in 0 typed/scheme) mzlib/etc))] (for-label (only-meta-in 0 typed/racket) mzlib/etc))]
@title[#:tag "more"]{Specifying Types} @title[#:tag "more"]{Specifying Types}
@(define the-eval (make-base-eval)) @(define the-eval (make-base-eval))
@(the-eval '(require typed/scheme)) @(the-eval '(require typed/racket))
The previous section introduced the basics of the Typed Scheme type The previous section introduced the basics of the Typed Racket type
system. In this section, we will see several new features of the system. In this section, we will see several new features of the
language, allowing types to be specified and used. language, allowing types to be specified and used.
@section{Type Annotation and Binding Forms} @section{Type Annotation and Binding Forms}
In general, variables in Typed Scheme must be annotated with their In general, variables in Typed Racket must be annotated with their
type. type.
@subsection{Annotating Definitions} @subsection{Annotating Definitions}
We have already seen the @scheme[:] type annotation form. This is We have already seen the @racket[:] type annotation form. This is
useful for definitions, at both the top level of a module useful for definitions, at both the top level of a module
@schemeblock[ @racketblock[
(: x Number) (: x Number)
(define x 7)] (define x 7)]
and in an internal definition and in an internal definition
@schemeblock[ @racketblock[
(let () (let ()
(: x Number) (: x Number)
(define x 7) (define x 7)
(add1 x)) (add1 x))
] ]
In addition to the @scheme[:] form, almost all binding forms from In addition to the @racket[:] form, almost all binding forms from
@schememodname[scheme] have counterparts which allow the specification @racketmodname[racket] have counterparts which allow the specification
of types. The @scheme[define:] form allows the definition of variables of types. The @racket[define:] form allows the definition of variables
in both top-level and internal contexts. in both top-level and internal contexts.
@schemeblock[ @racketblock[
(define: x : Number 7) (define: x : Number 7)
(define: (id [z : Number]) z)] (define: (id [z : Number]) z)]
Here, @scheme[x] has the type @scheme[Number], and @scheme[id] has the Here, @racket[x] has the type @racket[Number], and @racket[id] has the
type @scheme[(Number -> Number)]. In the body of @scheme[id], type @racket[(Number -> Number)]. In the body of @racket[id],
@scheme[z] has the type @scheme[Number]. @racket[z] has the type @racket[Number].
@subsection{Annotating Local Binding} @subsection{Annotating Local Binding}
@schemeblock[ @racketblock[
(let: ([x : Number 7]) (let: ([x : Number 7])
(add1 x)) (add1 x))
] ]
The @scheme[let:] form is exactly like @scheme[let], but type The @racket[let:] form is exactly like @racket[let], but type
annotations are provided for each variable bound. Here, @scheme[x] is annotations are provided for each variable bound. Here, @racket[x] is
given the type @scheme[Number]. The @scheme[let*:] and given the type @racket[Number]. The @racket[let*:] and
@scheme[letrec:] are similar. @racket[letrec:] are similar.
@schemeblock[ @racketblock[
(let-values: ([([x : Number] [y : String]) (values 7 "hello")]) (let-values: ([([x : Number] [y : String]) (values 7 "hello")])
(+ x (string-length y))) (+ x (string-length y)))
] ]
The @scheme[let*-values:] and @scheme[letrec-values:] forms are similar. The @racket[let*-values:] and @racket[letrec-values:] forms are similar.
@subsection{Annotating Functions} @subsection{Annotating Functions}
Function expressions also bind variables, which can be annotated with Function expressions also bind variables, which can be annotated with
types. This function expects two arguments, a @scheme[Number] and a types. This function expects two arguments, a @racket[Number] and a
@scheme[String]: @racket[String]:
@schemeblock[(lambda: ([x : Number] [y : String]) (+ x 5))] @racketblock[(lambda: ([x : Number] [y : String]) (+ x 5))]
This function accepts at least one @scheme[String], followed by This function accepts at least one @racket[String], followed by
arbitrarily many @scheme[Number]s. In the body, @scheme[y] is a list arbitrarily many @racket[Number]s. In the body, @racket[y] is a list
of @scheme[Number]s. of @racket[Number]s.
@schemeblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))] @racketblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))]
This function has the type @scheme[(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:
@schemeblock[(case-lambda: [() 0] @racketblock[(case-lambda: [() 0]
[([x : Number]) x])] [([x : Number]) x])]
This function has the type This function has the type
@scheme[(case-lambda (-> Number) (Number -> Number))]. @racket[(case-lambda (-> Number) (Number -> Number))].
@subsection{Annotating Single Variables} @subsection{Annotating Single Variables}
When a single variable binding needs annotation, the annotation can be When a single variable binding needs annotation, the annotation can be
applied to a single variable using a reader extension: applied to a single variable using a reader extension:
@schemeblock[ @racketblock[
(let ([#,(annvar x Number) 7]) (add1 x))] (let ([#,(annvar x Number) 7]) (add1 x))]
This is equivalent to the earlier use of @scheme[let:]. This is This is equivalent to the earlier use of @racket[let:]. This is
especially useful for binding forms which do not have counterparts especially useful for binding forms which do not have counterparts
provided by Typed Scheme, such as @scheme[let+]: provided by Typed Racket, such as @racket[let+]:
@schemeblock[ @racketblock[
(let+ ([val #,(annvar x Number) (+ 6 1)]) (let+ ([val #,(annvar x Number) (+ 6 1)])
(* x x))] (* x x))]
@ -113,10 +113,10 @@ provided by Typed Scheme, such as @scheme[let+]:
It is also possible to provide an expected type for a particular It is also possible to provide an expected type for a particular
expression. expression.
@schemeblock[(ann (+ 7 1) Number)] @racketblock[(ann (+ 7 1) Number)]
This ensures that the expression, here @scheme[(+ 7 1)], has the This ensures that the expression, here @racket[(+ 7 1)], has the
desired type, here @scheme[Number]. Otherwise, the type checker desired type, here @racket[Number]. Otherwise, the type checker
signals an error. For example: signals an error. For example:
@interaction[#:eval the-eval @interaction[#:eval the-eval
@ -124,37 +124,37 @@ signals an error. For example:
@section{Type Inference} @section{Type Inference}
In many cases, type annotations can be avoided where Typed Scheme can In many cases, type annotations can be avoided where Typed Racket can
infer them. For example, the types of all local bindings using infer them. For example, the types of all local bindings using
@scheme[let] and @scheme[let*] can be inferred. @racket[let] and @racket[let*] can be inferred.
@schemeblock[(let ([x 7]) (add1 x))] @racketblock[(let ([x 7]) (add1 x))]
In this example, @scheme[x] has the type In this example, @racket[x] has the type
@scheme[Exact-Positive-Integer]. @racket[Exact-Positive-Integer].
Similarly, top-level constant definitions do not require annotation: Similarly, top-level constant definitions do not require annotation:
@schemeblock[(define y "foo")] @racketblock[(define y "foo")]
In this examples, @scheme[y] has the type @scheme[String]. In this examples, @racket[y] has the type @racket[String].
Finally, the parameter types for loops are inferred from their initial Finally, the parameter types for loops are inferred from their initial
values. values.
@schemeblock[ @racketblock[
(let loop ([x 0] [y (list 1 2 3)]) (let loop ([x 0] [y (list 1 2 3)])
(if (null? y) x (loop (+ x (car y)) (cdr y))))] (if (null? y) x (loop (+ x (car y)) (cdr y))))]
Here @scheme[x] has the inferred type @scheme[Integer], and @scheme[y] Here @racket[x] has the inferred type @racket[Integer], and @racket[y]
has the inferred type @scheme[(Listof Integer)]. The @scheme[loop] has the inferred type @racket[(Listof Integer)]. The @racket[loop]
variable has type @scheme[(Integer (Listof Integer) -> Integer)]. variable has type @racket[(Integer (Listof Integer) -> Integer)].
@section{New Type Names} @section{New Type Names}
Any type can be given a name with @scheme[define-type]. Any type can be given a name with @racket[define-type].
@schemeblock[(define-type NN (Number -> Number))] @racketblock[(define-type NN (Number -> Number))]
Anywhere the name @scheme[NN] is used, it is expanded to Anywhere the name @racket[NN] is used, it is expanded to
@scheme[(Number -> Number)]. Type names may not be recursive. @racket[(Number -> Number)]. Type names may not be recursive.

24
collects/typed-scheme/scribblings/quick.scrbl
View File

@ -1,18 +1,18 @@
#lang scribble/manual #lang scribble/manual
@(require "utils.ss" (for-label (only-meta-in 0 typed/scheme))) @(require "utils.ss" (for-label (only-meta-in 0 typed/racket)))
@(provide typed-mod) @(provide typed-mod)
@title[#:tag "quick"]{Quick Start} @title[#:tag "quick"]{Quick Start}
Given a module written in the @schememodname[scheme] language, using Given a module written in the @racketmodname[racket] language, using
Typed Scheme requires the following steps: Typed Racket requires the following steps:
@itemize[#:style @itemize[#:style
'ordered 'ordered
@item{Change the language to @schememodname[typed/scheme].} @item{Change the language to @racketmodname[typed/racket].}
@item{Change the uses of @scheme[(require mod)] to @item{Change the uses of @racket[(require mod)] to
@scheme[(require typed/mod)].} @racket[(require typed/mod)].}
@item{Annotate structure definitions and top-level @item{Annotate structure definitions and top-level
definitions with their types.} ] definitions with their types.} ]
@ -20,12 +20,12 @@ Then, when the program is run, it will automatically be typechecked
before any execution, and any type errors will be reported. If there before any execution, and any type errors will be reported. If there
are any type errors, the program will not run. are any type errors, the program will not run.
Here is an example program, written in the @schememodname[scheme] Here is an example program, written in the @racketmodname[racket]
language: language:
@(define typed-mod @(define typed-mod
@schememod[ @racketmod[
typed/scheme typed/racket
(define-struct: pt ([x : Real] [y : Real])) (define-struct: pt ([x : Real] [y : Real]))
(: mag (pt -> Number)) (: mag (pt -> Number))
@ -34,8 +34,8 @@ typed/scheme
] ]
) )
@schememod[ @racketmod[
scheme racket
(define-struct pt (x y)) (define-struct pt (x y))
(code:contract mag : pt -> number) (code:contract mag : pt -> number)
@ -43,6 +43,6 @@ scheme
(sqrt (+ (sqr (pt-x p)) (sqr (pt-y p))))) (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
] ]
Here is the same program, in @schememodname[typed/scheme]: Here is the same program, in @racketmodname[typed/racket]:
@|typed-mod| @|typed-mod|

282
collects/typed-scheme/scribblings/ts-guide.scrbl
View File

@ -1,17 +1,17 @@
#lang scribble/manual #lang scribble/manual
@begin[(require "utils.ss" (for-label (only-meta-in 0 typed/scheme)))] @begin[(require "utils.ss" (for-label (only-meta-in 0 typed/racket)))]
@title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types} @title[#:tag "top"]{@bold{Typed Racket}: Racket with Static Types}
@author["Sam Tobin-Hochstadt"] @author["Sam Tobin-Hochstadt"]
@section-index["typechecking" "typechecker" "typecheck"] @section-index["typechecking" "typechecker" "typecheck"]
Typed Scheme is a family of languages, each of which enforce Typed Racket is a family of languages, each of which enforce
that programs written in the language obey a type system that ensures that programs written in the language obey a type system that ensures
the absence of many common errors. This guide is intended for programmers familiar the absence of many common errors. This guide is intended for programmers familiar
with PLT Scheme. For an introduction to PLT Scheme, see the @(other-manual '(lib "scribblings/guide/guide.scrbl")). with Racket. For an introduction to Racket, see the @(other-manual '(lib "scribblings/guide/guide.scrbl")).
@local-table-of-contents[] @local-table-of-contents[]
@ -23,277 +23,3 @@ with PLT Scheme. For an introduction to PLT Scheme, see the @(other-manual '(li
@;@section{How the Type System Works} @;@section{How the Type System Works}
@;@section{Integrating with Untyped Code} @;@section{Integrating with Untyped Code}
@;{
@section{Starting with Typed Scheme}
If you already know PLT Scheme, or even some other Scheme, it should be
easy to start using Typed Scheme.
@subsection{A First Function}
The following program defines the Fibonacci function in PLT Scheme:
@schememod[
scheme
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
This program defines the same program using Typed Scheme.
@schememod[
typed-scheme
(: fib (Number -> Number))
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
There are two differences between these programs:
@itemize[
@item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
@item*[@elem{The Type Annotation}]{We have added a type annotation
for the @scheme[fib] function, using the @scheme[:] form.} ]
In general, these are most of the changes that have to be made to a
PLT Scheme program to transform it into a Typed Scheme program.
@margin-note{Changes to uses of @scheme[require] may also be necessary
- these are described later.}
@subsection[#:tag "complex"]{Adding more complexity}
Other typed binding forms are also available. For example, we could have
rewritten our fibonacci program as follows:
@schememod[
typed-scheme
(: fib (Number -> Number))
(define (fib n)
(let ([base? (or (= 0 n) (= 1 n))])
(if base?
1
(+ (fib (- n 1)) (fib (- n 2))))))
]
This program uses the @scheme[let] binding form, but no new type
annotations are required. Typed Scheme infers the type of
@scheme[base?].
We can also define mutually-recursive functions:
@schememod[
typed-scheme
(: my-odd? (Number -> Boolean))
(define (my-odd? n)
(if (= 0 n) #f
(my-even? (- n 1))))
(: my-even? (Number -> Boolean))
(define (my-even? n)
(if (= 0 n) #t
(my-odd? (- n 1))))
(my-even? 12)
]
As expected, this program prints @schemeresult[#t].
@subsection{Defining New Datatypes}
If our program requires anything more than atomic data, we must define
new datatypes. In Typed Scheme, structures can be defined, similarly
to PLT Scheme structures. The following program defines a date
structure and a function that formats a date as a string, using PLT
Scheme's built-in @scheme[format] function.
@schememod[
typed-scheme
(define-struct: Date ([day : Number] [month : String] [year : Number]))
(: format-date (Date -> String))
(define (format-date d)
(format "Today is day ~a of ~a in the year ~a"
(Date-day d) (Date-month d) (Date-year d)))
(format-date (make-Date 28 "November" 2006))
]
Here we see the built-in type @scheme[String] as well as a definition
of the new user-defined type @scheme[Date]. To define
@scheme[Date], we provide all the information usually found in a
@scheme[define-struct], but added type annotations to the fields using
the @scheme[define-struct:] form.
Then we can use the functions that this declaration creates, just as
we would have with @scheme[define-struct].
@subsection{Recursive Datatypes and Unions}
Many data structures involve multiple variants. In Typed Scheme, we
represent these using @italic{union types}, written @scheme[(U t1 t2 ...)].
@schememod[
typed-scheme
(define-type Tree (U leaf node))
(define-struct: leaf ([val : Number]))
(define-struct: node ([left : Tree] [right : Tree]))
(: tree-height (Tree -> Number))
(define (tree-height t)
(cond [(leaf? t) 1]
[else (max (+ 1 (tree-height (node-left t)))
(+ 1 (tree-height (node-right t))))]))
(: tree-sum (Tree -> Number))
(define (tree-sum t)
(cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t))
(tree-sum (node-right t)))]))
]
In this module, we have defined two new datatypes: @scheme[leaf] and
@scheme[node]. We've also defined the type name @scheme[Tree] to be
@scheme[(U node leaf)], which represents a binary tree of numbers. In
essence, we are saying that the @scheme[tree-height] function accepts
a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf],
and produces a number.
In order to calculate interesting facts about trees, we have to take
them apart and get at their contents. But since accessors such as
@scheme[node-left] require a @scheme[node] as input, not a
@scheme[Tree], we have to determine which kind of input we
were passed.
For this purpose, we use the predicates that come with each defined
structure. For example, the @scheme[leaf?] predicate distinguishes
@scheme[leaf]s from all other Typed Scheme values. Therefore, in the
first branch of the @scheme[cond] clause in @scheme[tree-sum], we know
that @scheme[t] is a @scheme[leaf], and therefore we can get its value
with the @scheme[leaf-val] function.
In the else clauses of both functions, we know that @scheme[t] is not
a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by
process of elimination we can determine that @scheme[t] must be a
@scheme[node]. Therefore, we can use accessors such as
@scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
@section[#:tag "poly"]{Polymorphism}
Typed Scheme offers abstraction over types as well as values.
@subsection{Polymorphic Data Structures}
Virtually every Scheme program uses lists and sexpressions. Fortunately, Typed
Scheme can handle these as well. A simple list processing program can be
written like this:
@schememod[
typed-scheme
(: sum-list ((Listof Number) -> Number))
(define (sum-list l)
(cond [(null? l) 0]
[else (+ (car l) (sum-list (cdr l)))]))
]
This looks similar to our earlier programs --- except for the type
of @scheme[l], which looks like a function application. In fact, it's
a use of the @italic{type constructor} @scheme[Listof], which takes
another type as its input, here @scheme[Number]. We can use
@scheme[Listof] to construct the type of any kind of list we might
want.
We can define our own type constructors as well. For example, here is
an analog of the @tt{Maybe} type constructor from Haskell:
@schememod[
typed-scheme
(define-struct: Nothing ())
(define-struct: (a) Just ([v : a]))
(define-type (Maybe a) (U Nothing (Just a)))
(: find (Number (Listof Number) -> (Maybe Number)))
(define (find v l)
(cond [(null? l) (make-Nothing)]
[(= v (car l)) (make-Just v)]
[else (find v (cdr l))]))
]
The first @scheme[define-struct:] defines @scheme[Nothing] to be
a structure with no contents.
The second definition
@schemeblock[
(define-struct: (a) Just ([v : a]))
]
creates a parameterized type, @scheme[Just], which is a structure with
one element, whose type is that of the type argument to
@scheme[Just]. Here the type parameters (only one, @scheme[a], in
this case) are written before the type name, and can be referred to in
the types of the fields.
The type definiton
@schemeblock[
(define-type (Maybe a) (U Nothing (Just a)))
]
creates a parameterized type --- @scheme[Maybe] is a potential
container for whatever type is supplied.
The @scheme[find] function takes a number @scheme[v] and list, and
produces @scheme[(make-Just v)] when the number is found in the list,
and @scheme[(make-Nothing)] otherwise. Therefore, it produces a
@scheme[(Maybe Number)], just as the annotation specified.
@subsection{Polymorphic Functions}
Sometimes functions over polymorphic data structures only concern
themselves with the form of the structure. For example, one might
write a function that takes the length of a list of numbers:
@schememod[
typed-scheme
(: list-number-length ((Listof Number) -> Integer))
(define (list-number-length l)
(if (null? l)
0
(add1 (list-number-length (cdr l)))))]
and also a function that takes the length of a list of strings:
@schememod[
typed-scheme
(: list-string-length ((Listof String) -> Integer))
(define (list-string-length l)
(if (null? l)
0
(add1 (list-string-length (cdr l)))))]
Notice that both of these functions have almost exactly the same
definition; the only difference is the name of the function. This
is because neither function uses the type of the elements in the
definition.
We can abstract over the type of the element as follows:
@schememod[
typed-scheme
(: list-length (All (A) ((Listof A) -> Integer)))
(define (list-length l)
(if (null? l)
0
(add1 (list-length (cdr l)))))]
The new type constructor @scheme[All] takes a list of type
variables and a body type. The type variables are allowed to
appear free in the body of the @scheme[All] form.
}

258
collects/typed-scheme/scribblings/ts-reference.scrbl
View File

@ -1,19 +1,19 @@
#lang scribble/manual #lang scribble/manual
@begin[(require "utils.ss" scribble/eval @begin[(require "utils.ss" scribble/eval
scheme/sandbox) racket/sandbox)
(require (for-label (only-meta-in 0 typed/scheme) (require (for-label (only-meta-in 0 typed/racket)
scheme/list srfi/14 racket/list srfi/14
version/check))] version/check))]
@(define the-eval (make-base-eval)) @(define the-eval (make-base-eval))
@(the-eval '(require (except-in typed/scheme #%top-interaction #%module-begin))) @(the-eval '(require (except-in typed/racket #%top-interaction #%module-begin)))
@title[#:tag "top"]{The Typed Scheme Reference} @title[#:tag "top"]{The Typed Racket Reference}
@author["Sam Tobin-Hochstadt"] @author["Sam Tobin-Hochstadt"]
@(defmodulelang* (typed/scheme/base typed/scheme) @(defmodulelang* (typed/racket/base typed/racket)
#:use-sources (typed-scheme/typed-scheme typed-scheme/private/prims)) #:use-sources (typed-scheme/typed-scheme typed-scheme/private/prims))
@section[#:tag "type-ref"]{Type Reference} @section[#:tag "type-ref"]{Type Reference}
@ -45,9 +45,9 @@
@defidform[EOF] @defidform[EOF]
@defidform[Continuation-Mark-Set] @defidform[Continuation-Mark-Set]
@defidform[Char])]{ @defidform[Char])]{
These types represent primitive Scheme data. Note that @scheme[Integer] represents exact integers.} These types represent primitive Racket data. Note that @racket[Integer] represents exact integers.}
@defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].} @defidform[Any]{Any Racket value. All other types are subtypes of @racket[Any].}
@defidform[Nothing]{The empty type. No values inhabit this type, and @defidform[Nothing]{The empty type. No values inhabit this type, and
any expression of this type will not evaluate to a value.} any expression of this type will not evaluate to a value.}
@ -55,18 +55,18 @@ any expression of this type will not evaluate to a value.}
The following base types are parameteric in their type arguments. The following base types are parameteric in their type arguments.
@defform[(Listof t)]{Homogenous @rtech{lists} of @scheme[t]} @defform[(Listof t)]{Homogenous @rtech{lists} of @racket[t]}
@defform[(Boxof t)]{A @rtech{box} of @scheme[t]} @defform[(Boxof t)]{A @rtech{box} of @racket[t]}
@defform[(Syntaxof t)]{A @rtech{syntax object} containing a @scheme[t]} @defform[(Syntaxof t)]{A @rtech{syntax object} containing a @racket[t]}
@defform[(Vectorof t)]{Homogenous @rtech{vectors} of @scheme[t]} @defform[(Vectorof t)]{Homogenous @rtech{vectors} of @racket[t]}
@defform[(Option t)]{Either @scheme[t] of @scheme[#f]} @defform[(Option t)]{Either @racket[t] of @racket[#f]}
@defform*[[(Parameter t) @defform*[[(Parameter t)
(Parameter s t)]]{A @rtech{parameter} of @scheme[t]. If two type arguments are supplied, (Parameter s t)]]{A @rtech{parameter} of @racket[t]. If two type arguments are supplied,
the first is the type the parameter accepts, and the second is the type returned.} the first is the type the parameter accepts, and the second is the type returned.}
@defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car] @defform[(Pair s t)]{is the pair containing @racket[s] as the @racket[car]
and @scheme[t] as the @scheme[cdr]} and @racket[t] as the @racket[cdr]}
@defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type @defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type
@scheme[k] and value type @scheme[v].} @racket[k] and value type @racket[v].}
@subsubsub*section{Type Constructors} @subsubsub*section{Type Constructors}
@ -75,62 +75,62 @@ The following base types are parameteric in their type arguments.
(dom ... rest * -> rng) (dom ... rest * -> rng)
(dom ... rest ... bound -> rng) (dom ... rest ... bound -> rng)
(dom -> rng : pred)]]{is the type of functions from the (possibly-empty) (dom -> rng : pred)]]{is the type of functions from the (possibly-empty)
sequence @scheme[dom ...] to the @scheme[rng] type. The second form sequence @racket[dom ...] to the @racket[rng] type. The second form
specifies a uniform rest argument of type @scheme[rest], and the specifies a uniform rest argument of type @racket[rest], and the
third form specifies a non-uniform rest argument of type third form specifies a non-uniform rest argument of type
@scheme[rest] with bound @scheme[bound]. In the third form, the @racket[rest] with bound @racket[bound]. In the third form, the
second occurrence of @scheme[...] is literal, and @scheme[bound] second occurrence of @racket[...] is literal, and @racket[bound]
must be an identifier denoting a type variable. In the fourth form, must be an identifier denoting a type variable. In the fourth form,
there must be only one @scheme[dom] and @scheme[pred] is the type there must be only one @racket[dom] and @racket[pred] is the type
checked by the predicate.} checked by the predicate.}
@defform[(U t ...)]{is the union of the types @scheme[t ...]} @defform[(U t ...)]{is the union of the types @racket[t ...]}
@defform[(case-lambda fun-ty ...)]{is a function that behaves like all of @defform[(case-lambda fun-ty ...)]{is a function that behaves like all of
the @scheme[fun-ty]s. The @scheme[fun-ty]s must all be function the @racket[fun-ty]s. The @racket[fun-ty]s must all be function
types constructed with @scheme[->].} types constructed with @racket[->].}
@defform/none[(t t1 t2 ...)]{is the instantiation of the parametric type @defform/none[(t t1 t2 ...)]{is the instantiation of the parametric type
@scheme[t] at types @scheme[t1 t2 ...]} @racket[t] at types @racket[t1 t2 ...]}
@defform[(All (v ...) t)]{is a parameterization of type @scheme[t], with @defform[(All (v ...) t)]{is a parameterization of type @racket[t], with
type variables @scheme[v ...]} type variables @racket[v ...]}
@defform[(List t ...)]{is the type of the list with one element, in order, @defform[(List t ...)]{is the type of the list with one element, in order,
for each type provided to the @scheme[List] type constructor.} for each type provided to the @racket[List] type constructor.}
@defform[(values t ...)]{is the type of a sequence of multiple values, with @defform[(values t ...)]{is the type of a sequence of multiple values, with
types @scheme[t ...]. This can only appear as the return type of a types @racket[t ...]. This can only appear as the return type of a
function.} function.}
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value} @defform/none[v]{where @racket[v] is a number, boolean or string, is the singleton type containing only that value}
@defform/none[(quote val)]{where @scheme[val] is a Scheme value, is the singleton type containing only that value} @defform/none[(quote val)]{where @racket[val] is a Racket value, is the singleton type containing only that value}
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type @defform/none[i]{where @racket[i] is an identifier can be a reference to a type
name or a type variable} name or a type variable}
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the @defform[(Rec n t)]{is a recursive type where @racket[n] is bound to the
recursive type in the body @scheme[t]} recursive type in the body @racket[t]}
Other types cannot be written by the programmer, but are used Other types cannot be written by the programmer, but are used
internally and may appear in error messages. internally and may appear in error messages.
@defform/none[(struct:n (t ...))]{is the type of structures named @defform/none[(struct:n (t ...))]{is the type of structures named
@scheme[n] with field types @scheme[t]. There may be multiple such @racket[n] with field types @racket[t]. There may be multiple such
types with the same printed representation.} types with the same printed representation.}
@defform/none[<n>]{is the printed representation of a reference to the @defform/none[<n>]{is the printed representation of a reference to the
type variable @scheme[n]} type variable @racket[n]}
@section[#:tag "special-forms"]{Special Form Reference} @section[#:tag "special-forms"]{Special Form Reference}
Typed Scheme provides a variety of special forms above and beyond Typed Racket provides a variety of special forms above and beyond
those in PLT Scheme. They are used for annotating variables with types, those in Racket. They are used for annotating variables with types,
creating new types, and annotating expressions. creating new types, and annotating expressions.
@subsection{Binding Forms} @subsection{Binding Forms}
@scheme[_loop], @scheme[_f], @scheme[_a], and @scheme[_v] are names, @scheme[_t] is a type. @racket[_loop], @racket[_f], @racket[_a], and @racket[_v] are names, @racket[_t] is a type.
@scheme[_e] is an expression and @scheme[_body] is a block. @racket[_e] is an expression and @racket[_body] is a block.
@defform*[[ @defform*[[
(let: ([v : t e] ...) . body) (let: ([v : t e] ...) . body)
(let: loop : t0 ([v : t e] ...) . body)]]{ (let: loop : t0 ([v : t e] ...) . body)]]{
Local bindings, like @scheme[let], each with Local bindings, like @racket[let], each with
associated types. In the second form, @scheme[_t0] is the type of the associated types. In the second form, @racket[_t0] is the type of the
result of @scheme[_loop] (and thus the result of the entire result of @racket[_loop] (and thus the result of the entire
expression as well as the final expression as well as the final
expression in @scheme[body]).} expression in @racket[body]).}
@deftogether[[ @deftogether[[
@defform[(letrec: ([v : t e] ...) . body)] @defform[(letrec: ([v : t e] ...) . body)]
@defform[(let*: ([v : t e] ...) . body)] @defform[(let*: ([v : t e] ...) . body)]
@ -138,30 +138,30 @@ result of @scheme[_loop] (and thus the result of the entire
@defform[(letrec-values: ([([v : t] ...) e] ...) . body)] @defform[(letrec-values: ([([v : t] ...) e] ...) . body)]
@defform[(let*-values: ([([v : t] ...) e] ...) . body)]]]{ @defform[(let*-values: ([([v : t] ...) e] ...) . body)]]]{
Type-annotated versions of Type-annotated versions of
@scheme[letrec], @scheme[let*], @scheme[let-values], @racket[letrec], @racket[let*], @racket[let-values],
@scheme[letrec-values], and @scheme[let*-values].} @racket[letrec-values], and @racket[let*-values].}
@deftogether[[ @deftogether[[
@defform[(let/cc: v : t . body)] @defform[(let/cc: v : t . body)]
@defform[(let/ec: v : t . body)]]]{Type-annotated versions of @defform[(let/ec: v : t . body)]]]{Type-annotated versions of
@scheme[let/cc] and @scheme[let/ec].} @racket[let/cc] and @racket[let/ec].}
@subsection{Anonymous Functions} @subsection{Anonymous Functions}
@defform/subs[(lambda: formals . body) @defform/subs[(lambda: formals . body)
([formals ([v : t] ...) ([formals ([v : t] ...)
([v : t] ... . [v : t])])]{ ([v : t] ... . [v : t])])]{
A function of the formal arguments @scheme[v], where each formal A function of the formal arguments @racket[v], where each formal
argument has the associated type. If a rest argument is present, then argument has the associated type. If a rest argument is present, then
it has type @scheme[(Listof t)].} it has type @racket[(Listof t)].}
@defform[(λ: formals . body)]{ @defform[(λ: formals . body)]{
An alias for the same form using @scheme[lambda:].} An alias for the same form using @racket[lambda:].}
@defform[(plambda: (a ...) formals . body)]{ @defform[(plambda: (a ...) formals . body)]{
A polymorphic function, abstracted over the type variables A polymorphic function, abstracted over the type variables
@scheme[a]. The type variables @scheme[a] are bound in both the types @racket[a]. The type variables @racket[a] are bound in both the types
of the formal, and in any type expressions in the @scheme[body].} of the formal, and in any type expressions in the @racket[body].}
@defform[(case-lambda: [formals body] ...)]{ @defform[(case-lambda: [formals body] ...)]{
A function of multiple arities. Note that each @scheme[formals] must have a A function of multiple arities. Note that each @racket[formals] must have a
different arity.} different arity.}
@defform[(pcase-lambda: (a ...) [formals body] ...)]{ @defform[(pcase-lambda: (a ...) [formals body] ...)]{
A polymorphic function of multiple arities.} A polymorphic function of multiple arities.}
@ -173,8 +173,8 @@ A polymorphic function of multiple arities.}
expr ...+) expr ...+)
([step-expr-maybe code:blank ([step-expr-maybe code:blank
step-expr])]{ step-expr])]{
Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and Like @racket[do], but each @racket[id] having the associated type @racket[t], and
the final body @scheme[expr] having the type @scheme[u]. the final body @racket[expr] having the type @racket[u].
} }
@ -184,9 +184,9 @@ the final body @scheme[expr] having the type @scheme[u].
(define: (f . formals) : t . body) (define: (f . formals) : t . body)
(define: (a ...) (f . formals) : t . body)]]{ (define: (a ...) (f . formals) : t . body)]]{
These forms define variables, with annotated types. The first form These forms define variables, with annotated types. The first form
defines @scheme[v] with type @scheme[t] and value @scheme[e]. The defines @racket[v] with type @racket[t] and value @racket[e]. The
second and third forms defines a function @scheme[f] with appropriate second and third forms defines a function @racket[f] with appropriate
types. In most cases, use of @scheme[:] is preferred to use of @scheme[define:].} types. In most cases, use of @racket[:] is preferred to use of @racket[define:].}
@ -195,63 +195,63 @@ types. In most cases, use of @scheme[:] is preferred to use of @scheme[define:]
(define-struct: maybe-type-vars name-spec ([f : t] ...)) (define-struct: maybe-type-vars name-spec ([f : t] ...))
([maybe-type-vars code:blank (v ...)] ([maybe-type-vars code:blank (v ...)]
[name-spec name (name parent)])]{ [name-spec name (name parent)])]{
Defines a @rtech{structure} with the name @scheme[name], where the Defines a @rtech{structure} with the name @racket[name], where the
fields @scheme[f] have types @scheme[t]. When @scheme[parent], the fields @racket[f] have types @racket[t]. When @racket[parent], the
structure is a substructure of @scheme[parent]. When structure is a substructure of @racket[parent]. When
@scheme[maybe-type-vars] is present, the structure is polymorphic in the type @racket[maybe-type-vars] is present, the structure is polymorphic in the type
variables @scheme[v].} variables @racket[v].}
@defform/subs[ @defform/subs[
(define-struct/exec: name-spec ([f : t] ...) [e : proc-t]) (define-struct/exec: name-spec ([f : t] ...) [e : proc-t])
([name-spec name (name parent)])]{ ([name-spec name (name parent)])]{
Like @scheme[define-struct:], but defines an procedural structure. Like @racket[define-struct:], but defines an procedural structure.
The procdure @scheme[e] is used as the value for @scheme[prop:procedure], and must have type @scheme[proc-t].} The procdure @racket[e] is used as the value for @racket[prop:procedure], and must have type @racket[proc-t].}
@subsection{Names for Types} @subsection{Names for Types}
@defform*[[(define-type name t) @defform*[[(define-type name t)
(define-type (name v ...) t)]]{ (define-type (name v ...) t)]]{
The first form defines @scheme[name] as type, with the same meaning as The first form defines @racket[name] as type, with the same meaning as
@scheme[t]. The second form is equivalent to @racket[t]. The second form is equivalent to
@scheme[(define-type name (All (v ...) t))]. Type names may @racket[(define-type name (All (v ...) t))]. Type names may
refer to other types defined in the same module, but refer to other types defined in the same module, but
cycles among them are prohibited.} cycles among them are prohibited.}
@subsection{Generating Predicates Automatically} @subsection{Generating Predicates Automatically}
@defform[(define-predicate name t)]{ @defform[(define-predicate name t)]{
Defines @scheme[name] as a predicate for the type @scheme[t]. Defines @racket[name] as a predicate for the type @racket[t].
@scheme[name] has the type @scheme[(Any -> Boolean : t)]. @racket[name] has the type @racket[(Any -> Boolean : t)].
@scheme[t] may not contain function types.} @racket[t] may not contain function types.}
@subsection{Type Annotation and Instantiation} @subsection{Type Annotation and Instantiation}
@defform[(: v t)]{This declares that @scheme[v] has type @scheme[t]. @defform[(: v t)]{This declares that @racket[v] has type @racket[t].
The definition of @scheme[v] must appear after this declaration. This The definition of @racket[v] must appear after this declaration. This
can be used anywhere a definition form may be used.} can be used anywhere a definition form may be used.}
@defform[(provide: [v t] ...)]{This declares that the @scheme[v]s have @defform[(provide: [v t] ...)]{This declares that the @racket[v]s have
the types @scheme[t], and also provides all of the @scheme[v]s.} the types @racket[t], and also provides all of the @racket[v]s.}
@litchar{#{v : t}} This declares that the variable @scheme[v] has type @litchar{#{v : t}} This declares that the variable @racket[v] has type
@scheme[t]. This is legal only for binding occurences of @scheme[_v]. @racket[t]. This is legal only for binding occurences of @racket[_v].
@defform[(ann e t)]{Ensure that @scheme[e] has type @scheme[t], or @defform[(ann e t)]{Ensure that @racket[e] has type @racket[t], or
some subtype. The entire expression has type @scheme[t]. some subtype. The entire expression has type @racket[t].
This is legal only in expression contexts.} This is legal only in expression contexts.}
@litchar{#{e :: t}} This is identical to @scheme[(ann e t)]. @litchar{#{e :: t}} This is identical to @racket[(ann e t)].
@defform[(inst e t ...)]{Instantiate the type of @scheme[e] with types @defform[(inst e t ...)]{Instantiate the type of @racket[e] with types
@scheme[t ...]. @scheme[e] must have a polymorphic type with the @racket[t ...]. @racket[e] must have a polymorphic type with the
appropriate number of type variables. This is legal only in expression appropriate number of type variables. This is legal only in expression
contexts.} contexts.}
@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)]. @litchar|{#{e @ t ...}}| This is identical to @racket[(inst e t ...)].
@subsection{Require} @subsection{Require}
Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier Here, @racket[_m] is a module spec, @racket[_pred] is an identifier
naming a predicate, and @scheme[_r] is an optionally-renamed identifier. naming a predicate, and @racket[_r] is an optionally-renamed identifier.
@defform/subs[#:literals (struct opaque) @defform/subs[#:literals (struct opaque)
(require/typed m rt-clause ...) (require/typed m rt-clause ...)
@ -259,54 +259,54 @@ naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
[struct name ([f : t] ...)] [struct name ([f : t] ...)]
[struct (name parent) ([f : t] ...)] [struct (name parent) ([f : t] ...)]
[opaque t pred]]) [opaque t pred]])
]{This form requires identifiers from the module @scheme[m], giving ]{This form requires identifiers from the module @racket[m], giving
them the specified types. them the specified types.
The first form requires @scheme[r], giving it type @scheme[t]. The first form requires @racket[r], giving it type @racket[t].
@index["struct"]{The second and third forms} require the struct with name @scheme[name] @index["struct"]{The second and third forms} require the struct with name @racket[name]
with fields @scheme[f ...], where each field has type @scheme[t]. The with fields @racket[f ...], where each field has type @racket[t]. The
third form allows a @scheme[parent] structure type to be specified. third form allows a @racket[parent] structure type to be specified.
The parent type must already be a structure type known to Typed The parent type must already be a structure type known to Typed
Scheme, either built-in or via @scheme[require/typed]. The Racket, either built-in or via @racket[require/typed]. The
structure predicate has the appropriate Typed Scheme filter type so structure predicate has the appropriate Typed Racket filter type so
that it may be used as a predicate in @scheme[if] expressions in Typed that it may be used as a predicate in @racket[if] expressions in Typed
Scheme. Racket.
@index["opaque"]{The fourth case} defines a new type @scheme[t]. @scheme[pred], imported from @index["opaque"]{The fourth case} defines a new type @racket[t]. @racket[pred], imported from
module @scheme[m], is a predicate for this type. The type is defined module @racket[m], is a predicate for this type. The type is defined
as precisely those values to which @scheme[pred] produces as precisely those values to which @racket[pred] produces
@scheme[#t]. @scheme[pred] must have type @scheme[(Any -> Boolean)]. @racket[#t]. @racket[pred] must have type @racket[(Any -> Boolean)].
Opaque types must be required lexically before they are used. Opaque types must be required lexically before they are used.
In all cases, the identifiers are protected with @rtech{contracts} which In all cases, the identifiers are protected with @rtech{contracts} which
enforce the specified types. If this contract fails, the module enforce the specified types. If this contract fails, the module
@scheme[m] is blamed. @racket[m] is blamed.
Some types, notably polymorphic types constructed with @scheme[All], Some types, notably polymorphic types constructed with @racket[All],
cannot be converted to contracts and raise a static error when used in cannot be converted to contracts and raise a static error when used in
a @scheme[require/typed] form.} a @racket[require/typed] form.}
@section{Libraries Provided With Typed Scheme} @section{Libraries Provided With Typed Racket}
The @schememodname[typed/scheme] language corresponds to the The @racketmodname[typed/racket] language corresponds to the
@schememodname[scheme] language---that is, any identifier provided @racketmodname[racket] language---that is, any identifier provided
by @schememodname[scheme], such as @scheme[modulo] is available by default in by @racketmodname[racket], such as @racket[modulo] is available by default in
@schememodname[typed/scheme]. @racketmodname[typed/racket].
@schememod[typed/scheme @racketmod[typed/racket
(modulo 12 2) (modulo 12 2)
] ]
The @schememodname[typed/scheme/base] language corresponds to the The @racketmodname[typed/racket/base] language corresponds to the
@schememodname[scheme/base] language. @racketmodname[racket/base] language.
Some libraries have counterparts in the @schemeidfont{typed} Some libraries have counterparts in the @racketidfont{typed}
collection, which provide the same exports as the untyped versions. collection, which provide the same exports as the untyped versions.
Such libraries include @schememodname[srfi/14], Such libraries include @racketmodname[srfi/14],
@schememodname[net/url], and many others. @racketmodname[net/url], and many others.
@schememod[typed/scheme @racketmod[typed/racket
(require typed/srfi/14) (require typed/srfi/14)
(char-set= (string->char-set "hello") (char-set= (string->char-set "hello")
(string->char-set "olleh")) (string->char-set "olleh"))
@ -316,33 +316,33 @@ To participate in making more libraries available, please visit
@link["http://www.ccs.neu.edu/home/samth/adapt/"]{here}. @link["http://www.ccs.neu.edu/home/samth/adapt/"]{here}.
Other libraries can be used with Typed Scheme via Other libraries can be used with Typed Racket via
@scheme[require/typed]. @racket[require/typed].
@schememod[typed/scheme @racketmod[typed/racket
(require/typed version/check (require/typed version/check
[check-version (-> (U Symbol (Listof Any)))]) [check-version (-> (U Symbol (Listof Any)))])
(check-version) (check-version)
] ]
@section{Typed Scheme Syntax Without Type Checking} @section{Typed Racket Syntax Without Type Checking}
@defmodulelang[typed-scheme/no-check] @defmodulelang[typed-scheme/no-check]
On occasions where the Typed Scheme syntax is useful, but actual On occasions where the Typed Racket syntax is useful, but actual
typechecking is not desired, the @schememodname[typed-scheme/no-check] typechecking is not desired, the @racketmodname[typed-scheme/no-check]
language is useful. It provides the same bindings and syntax as Typed language is useful. It provides the same bindings and syntax as Typed
Scheme, but does no type checking. Racket, but does no type checking.
Examples: Examples:
@schememod[typed-scheme/no-check @racketmod[typed-scheme/no-check
(: x Number) (: x Number)
(define x "not-a-number")] (define x "not-a-number")]
@section{Typed Regions} @section{Typed Regions}
The @scheme[with-type] for allows for localized Typed Scheme regions in otherwise untyped code. The @racket[with-type] for allows for localized Typed Racket regions in otherwise untyped code.
@defform*/subs[[(with-type result-spec fv-clause body ...+) @defform*/subs[[(with-type result-spec fv-clause body ...+)
(with-type export-spec fv-clause body ...+)] (with-type export-spec fv-clause body ...+)]
@ -350,16 +350,16 @@ The @scheme[with-type] for allows for localized Typed Scheme regions in otherwis
(code:line #:freevars ([id fv-type] ...))] (code:line #:freevars ([id fv-type] ...))]
[result-spec (code:line #:result type)] [result-spec (code:line #:result type)]
[export-spec ([export-id export-type] ...)])]{ [export-spec ([export-id export-type] ...)])]{
The first form, an expression, checks that @scheme[body ...+] has the type @scheme[type]. The first form, an expression, checks that @racket[body ...+] has the type @racket[type].
If the last expression in @scheme[body ...+] returns multiple values, @scheme[type] must If the last expression in @racket[body ...+] returns multiple values, @racket[type] must
be a type of the form @scheme[(values t ...)]. be a type of the form @racket[(values t ...)].
Uses of the result values are appropriately checked by contracts generated from Uses of the result values are appropriately checked by contracts generated from
@scheme[type]. @racket[type].
The second form, which can be used as a definition, checks that each of the @scheme[export-id]s The second form, which can be used as a definition, checks that each of the @racket[export-id]s
has the specified type. These types are also enforced in the surrounding code with contracts. has the specified type. These types are also enforced in the surrounding code with contracts.
The @scheme[id]s are assumed to The @racket[id]s are assumed to
have the types ascribed to them; these types are converted to contracts and checked dynamically. have the types ascribed to them; these types are converted to contracts and checked dynamically.
@examples[#:eval the-eval @examples[#:eval the-eval

114
collects/typed-scheme/scribblings/types.scrbl
View File

@ -2,21 +2,21 @@
@begin[(require "utils.ss" @begin[(require "utils.ss"
scribble/core scribble/eval scribble/core scribble/eval
(for-label (only-meta-in 0 typed/scheme) mzlib/etc))] (for-label (only-meta-in 0 typed/racket) mzlib/etc))]
@(define the-eval (make-base-eval)) @(define the-eval (make-base-eval))
@(the-eval '(require typed/scheme)) @(the-eval '(require typed/racket))
@title[#:tag "types"]{Types in Typed Scheme} @title[#:tag "types"]{Types in Typed Racket}
Typed Scheme provides a rich variety of types to describe data. This Typed Racket provides a rich variety of types to describe data. This
section introduces them. section introduces them.
@section{Basic Types} @section{Basic Types}
The most basic types in Typed Scheme are those for primitive data, The most basic types in Typed Racket are those for primitive data,
such as @scheme[True] and @scheme[False] for booleans, @scheme[String] such as @racket[True] and @racket[False] for booleans, @racket[String]
for strings, and @scheme[Char] for characters. for strings, and @racket[Char] for characters.
@interaction[#:eval the-eval @interaction[#:eval the-eval
'"hello, world" '"hello, world"
@ -25,13 +25,13 @@ for strings, and @scheme[Char] for characters.
#f] #f]
Each symbol is given a unique type containing only that symbol. The Each symbol is given a unique type containing only that symbol. The
@scheme[Symbol] type includes all symbols. @racket[Symbol] type includes all symbols.
@interaction[#:eval the-eval @interaction[#:eval the-eval
'foo 'foo
'bar] 'bar]
Typed Scheme also provides a rich hierarchy for describing particular Typed Racket also provides a rich hierarchy for describing particular
kinds of numbers. kinds of numbers.
@interaction[#:eval the-eval @interaction[#:eval the-eval
@ -49,20 +49,20 @@ 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 @scheme[->], with the argument types before the are constructed using @racket[->], with the argument types before the
arrow and the result type after. Here are some example function arrow and the result type after. Here are some example function
types: types:
@schemeblock[ @racketblock[
(Number -> Number) (Number -> Number)
(String String -> Boolean) (String String -> Boolean)
(Char -> (values String Natural)) (Char -> (values String Natural))
] ]
The first type requires a @scheme[Number] as input, and produces a The first type requires a @racket[Number] as input, and produces a
@scheme[Number]. The second requires two arguments. The third takes @racket[Number]. The second requires two arguments. The third takes
one argument, and produces @rtech{multiple values}, of types one argument, and produces @rtech{multiple values}, of types
@scheme[String] and @scheme[Natural]. Here are example functions for @racket[String] and @racket[Natural]. Here are example functions for
each of these types. each of these types.
@interaction[#:eval the-eval @interaction[#:eval the-eval
@ -74,7 +74,7 @@ each of these types.
@section{Union Types} @section{Union Types}
Sometimes a value can be one of several types. To specify this, we Sometimes a value can be one of several types. To specify this, we
can use a union type, written with the type constructor @scheme[U]. can use a union type, written with the type constructor @racket[U].
@interaction[#:eval the-eval @interaction[#:eval the-eval
(let ([a-number 37]) (let ([a-number 37])
@ -85,7 +85,7 @@ can use a union type, written with the type constructor @scheme[U].
Any number of types can be combined together in a union, and nested Any number of types can be combined together in a union, and nested
unions are flattened. unions are flattened.
@schemeblock[(U Number String Boolean Char)] @racketblock[(U Number String Boolean Char)]
@section{Recursive Types} @section{Recursive Types}
@ -93,34 +93,34 @@ unions are flattened.
to describe an infinite family of data. For example, this is the type to describe an infinite family of data. For example, this is the type
of binary trees of numbers. of binary trees of numbers.
@schemeblock[ @racketblock[
(Rec BT (U Number (Pair BT BT)))] (Rec BT (U Number (Pair BT BT)))]
The @scheme[Rec] type constructor specifies that the type @scheme[BT] The @racket[Rec] type constructor specifies that the type @racket[BT]
refers to the whole binary tree type within the body of the refers to the whole binary tree type within the body of the
@scheme[Rec] form. @racket[Rec] form.
@section{Structure Types} @section{Structure Types}
Using @scheme[define-struct:] introduces new types, distinct from any Using @racket[define-struct:] introduces new types, distinct from any
previous type. previous type.
@schemeblock[(define-struct: point ([x : Real] [y : Real]))] @racketblock[(define-struct: point ([x : Real] [y : Real]))]
Instances of this structure, such as @scheme[(make-point 7 12)], have type @scheme[point]. Instances of this structure, such as @racket[(make-point 7 12)], have type @racket[point].
@section{Subtyping} @section{Subtyping}
In Typed Scheme, all types are placed in a hierarchy, based on what In Typed Racket, all types are placed in a hierarchy, based on what
values are included in the type. When an element of a larger type is values are included in the type. When an element of a larger type is
expected, an element of a smaller type may be provided. The smaller expected, an element of a smaller type may be provided. The smaller
type is called a @deftech{subtype} of the larger type. The larger type is called a @deftech{subtype} of the larger type. The larger
type is called a @deftech{supertype}. For example, type is called a @deftech{supertype}. For example,
@scheme[Integer] is a subtype of @scheme[Real], since every integer is @racket[Integer] is a subtype of @racket[Real], since every integer is
a real number. Therefore, the following code is acceptable to the a real number. Therefore, the following code is acceptable to the
type checker: type checker:
@schemeblock[ @racketblock[
(: f (Real -> Real)) (: f (Real -> Real))
(define (f x) (* x 0.75)) (define (f x) (* x 0.75))
@ -130,30 +130,30 @@ type checker:
(f x) (f x)
] ]
All types are subtypes of the @scheme[Any] type. All types are subtypes of the @racket[Any] type.
The elements of a union type are individually subtypes of the whole The elements of a union type are individually subtypes of the whole
union, so @scheme[String] is a subtype of @scheme[(U String Number)]. 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, @scheme[(Any -> String)] is a subtype of @scheme[(Number For example, @racket[(Any -> String)] is a subtype of @racket[(Number
-> (U String #f))]. -> (U String #f))].
@;@section{Occurrence Typing} @;@section{Occurrence Typing}
@section{Polymorphism} @section{Polymorphism}
Typed Scheme offers abstraction over types as well as values. Typed Racket offers abstraction over types as well as values.
@subsection{Polymorphic Data Structures} @subsection{Polymorphic Data Structures}
Virtually every Scheme program uses lists and sexpressions. Fortunately, Typed Virtually every Racket program uses lists and sexpressions. Fortunately, Typed
Scheme can handle these as well. A simple list processing program can be Racket can handle these as well. A simple list processing program can be
written like this: written like this:
@schememod[ @racketmod[
typed/scheme 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]
@ -161,17 +161,17 @@ typed/scheme
] ]
This looks similar to our earlier programs --- except for the type This looks similar to our earlier programs --- except for the type
of @scheme[l], which looks like a function application. In fact, it's of @racket[l], which looks like a function application. In fact, it's
a use of the @italic{type constructor} @scheme[Listof], which takes a use of the @italic{type constructor} @racket[Listof], which takes
another type as its input, here @scheme[Number]. We can use another type as its input, here @racket[Number]. We can use
@scheme[Listof] to construct the type of any kind of list we might @racket[Listof] to construct the type of any kind of list we might
want. want.
We can define our own type constructors as well. For example, here is We can define our own type constructors as well. For example, here is
an analog of the @tt{Maybe} type constructor from Haskell: an analog of the @tt{Maybe} type constructor from Haskell:
@schememod[ @racketmod[
typed/scheme typed/racket
(define-struct: None ()) (define-struct: None ())
(define-struct: (a) Some ([v : a])) (define-struct: (a) Some ([v : a]))
@ -184,32 +184,32 @@ typed/scheme
[else (find v (cdr l))])) [else (find v (cdr l))]))
] ]
The first @scheme[define-struct:] defines @scheme[None] to be The first @racket[define-struct:] defines @racket[None] to be
a structure with no contents. a structure with no contents.
The second definition The second definition
@schemeblock[ @racketblock[
(define-struct: (a) Some ([v : a])) (define-struct: (a) Some ([v : a]))
] ]
creates a parameterized type, @scheme[Just], which is a structure with creates a parameterized type, @racket[Just], which is a structure with
one element, whose type is that of the type argument to one element, whose type is that of the type argument to
@scheme[Just]. Here the type parameters (only one, @scheme[a], in @racket[Just]. Here the type parameters (only one, @racket[a], in
this case) are written before the type name, and can be referred to in this case) are written before the type name, and can be referred to in
the types of the fields. the types of the fields.
The type definiton The type definiton
@schemeblock[ @racketblock[
(define-type (Opt a) (U None (Some a))) (define-type (Opt a) (U None (Some a)))
] ]
creates a parameterized type --- @scheme[Opt] is a potential creates a parameterized type --- @racket[Opt] is a potential
container for whatever type is supplied. container for whatever type is supplied.
The @scheme[find] function takes a number @scheme[v] and list, and The @racket[find] function takes a number @racket[v] and list, and
produces @scheme[(make-Some v)] when the number is found in the list, produces @racket[(make-Some v)] when the number is found in the list,
and @scheme[(make-None)] otherwise. Therefore, it produces a and @racket[(make-None)] otherwise. Therefore, it produces a
@scheme[(Opt Number)], just as the annotation specified. @racket[(Opt Number)], just as the annotation specified.
@subsection{Polymorphic Functions} @subsection{Polymorphic Functions}
@ -217,8 +217,8 @@ Sometimes functions over polymorphic data structures only concern
themselves with the form of the structure. For example, one might themselves with the form of the structure. For example, one might
write a function that takes the length of a list of numbers: write a function that takes the length of a list of numbers:
@schememod[ @racketmod[
typed/scheme 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)
@ -227,8 +227,8 @@ typed/scheme
and also a function that takes the length of a list of strings: and also a function that takes the length of a list of strings:
@schememod[ @racketmod[
typed/scheme 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)
@ -242,17 +242,17 @@ definition.
We can abstract over the type of the element as follows: We can abstract over the type of the element as follows:
@schememod[ @racketmod[
typed/scheme 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
(add1 (list-length (cdr l)))))] (add1 (list-length (cdr l)))))]
The new type constructor @scheme[All] takes a list of type The new type constructor @racket[All] takes a list of type
variables and a body type. The type variables are allowed to variables and a body type. The type variables are allowed to
appear free in the body of the @scheme[All] form. appear free in the body of the @racket[All] form.
@include-section["varargs.scrbl"] @include-section["varargs.scrbl"]

62
collects/typed-scheme/scribblings/varargs.scrbl
View File

@ -1,18 +1,18 @@
#lang scribble/manual #lang scribble/manual
@begin[(require "utils.ss" (for-label typed/scheme/base))] @begin[(require "utils.ss" (for-label typed/racket/base))]
@title[#:tag "varargs"]{Variable-Arity Functions: Programming with Rest Arguments} @title[#:tag "varargs"]{Variable-Arity Functions: Programming with Rest Arguments}
Typed Scheme can handle some uses of rest arguments. Typed Racket can handle some uses of rest arguments.
@section{Uniform Variable-Arity Functions} @section{Uniform Variable-Arity Functions}
In Scheme, one can write a function that takes an arbitrary In Racket, one can write a function that takes an arbitrary
number of arguments as follows: number of arguments as follows:
@schememod[ @racketmod[
scheme racket
(define (sum . xs) (define (sum . xs)
(if (null? xs) (if (null? xs)
0 0
@ -25,12 +25,12 @@ scheme
The arguments to the function that are in excess to the The arguments to the function that are in excess to the
non-rest arguments are converted to a list which is assigned non-rest arguments are converted to a list which is assigned
to the rest parameter. So the examples above evaluate to to the rest parameter. So the examples above evaluate to
@schemeresult[0], @schemeresult[10], and @schemeresult[4]. @racketresult[0], @racketresult[10], and @racketresult[4].
We can define such functions in Typed Scheme as well: We can define such functions in Typed Racket as well:
@schememod[ @racketmod[
typed/scheme typed/racket
(: sum (Number * -> Number)) (: sum (Number * -> Number))
(define (sum . xs) (define (sum . xs)
(if (null? xs) (if (null? xs)
@ -43,10 +43,10 @@ of the rest parameter is used at the same type.
@section{Non-Uniform Variable-Arity Functions} @section{Non-Uniform Variable-Arity Functions}
However, the rest argument may be used as a heterogeneous list. However, the rest argument may be used as a heterogeneous list.
Take this (simplified) definition of the Scheme function @scheme[map]: Take this (simplified) definition of the Racket function @racket[map]:
@schememod[ @racketmod[
scheme racket
(define (map f as . bss) (define (map f as . bss)
(if (or (null? as) (if (or (null? as)
(ormap null? bss)) (ormap null? bss))
@ -58,21 +58,21 @@ scheme
(map cons (list 1 2 3) (list (list 4) (list 5) (list 6))) (map cons (list 1 2 3) (list (list 4) (list 5) (list 6)))
(map + (list 1 2 3) (list 2 3 4) (list 3 4 5) (list 4 5 6))] (map + (list 1 2 3) (list 2 3 4) (list 3 4 5) (list 4 5 6))]
Here the different lists that make up the rest argument @scheme[bss] Here the different lists that make up the rest argument @racket[bss]
can be of different types, but the type of each list in @scheme[bss] can be of different types, but the type of each list in @racket[bss]
corresponds to the type of the corresponding argument of @scheme[f]. corresponds to the type of the corresponding argument of @racket[f].
We also know that, in order to avoid arity errors, the length of We also know that, in order to avoid arity errors, the length of
@scheme[bss] must be one less than the arity of @scheme[f] (as @racket[bss] must be one less than the arity of @racket[f] (as
@scheme[as] corresponds to the first argument of @scheme[f]). @racket[as] corresponds to the first argument of @racket[f]).
The example uses of @scheme[map] evaluate to @schemeresult[(list 2 3 4 5)], The example uses of @racket[map] evaluate to @racketresult[(list 2 3 4 5)],
@schemeresult[(list (list 1 4) (list 2 5) (list 3 6))], and @racketresult[(list (list 1 4) (list 2 5) (list 3 6))], and
@schemeresult[(list 10 14 18)]. @racketresult[(list 10 14 18)].
In Typed Scheme, we can define @scheme[map] as follows: In Typed Racket, we can define @racket[map] as follows:
@schememod[ @racketmod[
typed/scheme typed/racket
(: map (: map
(All (C A B ...) (All (C A B ...)
((A B ... B -> C) (Listof A) (Listof B) ... B ((A B ... B -> C) (Listof A) (Listof B) ... B
@ -85,21 +85,21 @@ typed/scheme
(cons (apply f (car as) (map car bss)) (cons (apply f (car as) (map car bss))
(apply map f (cdr as) (map cdr bss)))))] (apply map f (cdr as) (map cdr bss)))))]
Note that the type variable @scheme[B] is followed by an Note that the type variable @racket[B] is followed by an
ellipsis. This denotes that B is a dotted type variable ellipsis. This denotes that B is a dotted type variable
which corresponds to a list of types, much as a rest which corresponds to a list of types, much as a rest
argument corresponds to a list of values. When the type argument corresponds to a list of values. When the type
of @scheme[map] is instantiated at a list of types, then of @racket[map] is instantiated at a list of types, then
each type @scheme[t] which is bound by @scheme[B] (notated by each type @racket[t] which is bound by @racket[B] (notated by
the dotted pre-type @scheme[t ... B]) is expanded to a number the dotted pre-type @racket[t ... B]) is expanded to a number
of copies of @scheme[t] equal to the length of the sequence of copies of @racket[t] equal to the length of the sequence
assigned to @scheme[B]. Then @scheme[B] in each copy is assigned to @racket[B]. Then @racket[B] in each copy is
replaced with the corresponding type from the sequence. replaced with the corresponding type from the sequence.
So the type of @scheme[(inst map Integer Boolean String Number)] So the type of @racket[(inst map Integer Boolean String Number)]
is is
@scheme[((Boolean String Number -> Integer) @racket[((Boolean String Number -> Integer)
(Listof Boolean) (Listof String) (Listof Number) (Listof Boolean) (Listof String) (Listof Number)
-> ->
(Listof Integer))]. (Listof Integer))].