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

work on new guide

Browse Source 
svn: r17814
This commit is contained in:
Sam Tobin-Hochstadt 2010-01-25 15:36:56 +00:00
parent e071050f7f
commit e65535c880
8 changed files with 427 additions and 140 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/info.ss
View File

@ -1,4 +1,4 @@
#lang setup/infotab #lang setup/infotab
(define scribblings '(("ts-reference.scrbl" ()) (define scribblings '(("scribblings/ts-reference.scrbl" ())
("ts-guide.scrbl" ()))) ("scribblings/ts-guide.scrbl" (multi-page))))

81
collects/typed-scheme/scribblings/begin.scrbl Normal file
View File

@ -0,0 +1,81 @@
#lang scribble/manual
@begin[(require (for-label typed/scheme) scribble/eval
"utils.ss" (only-in "quick.scrbl" typed-mod))]
@(define the-eval (make-base-eval))
@(the-eval '(require typed/scheme))
@title[#:tag "beginning"]{Beginning Typed Scheme}
Recall the typed module from @secref["quick"]:
@|typed-mod|
Let us consider each element of this program in turn.
@schememod[typed/scheme]
This specifies that the module is written in the
@schememodname[typed/scheme] language, which is a typed version of the
@schememodname[scheme] language. Typed versions of other languages
are provided as well; for example, the
@schememodname[typed/scheme/base] language corresponds to
@schememodname[scheme/base].
@schemeblock[(define-struct: pt ([x : Real] [y : Real]))]
@margin-note{Many forms in Typed Scheme have the same name as the
untyped forms, with a @scheme[:] suffix.}
This defines a new structure, name @scheme[pt], with two fields,
@scheme[x] and @scheme[y]. Both fields are specified to have the type
@scheme[Real], which corresponds to the @rtech{real numbers}.
The
@scheme[define-struct:] form corresponds to the @scheme[define-struct]
form from @schememodname[scheme]---when porting a program from
@schememodname[scheme] to @schememodname[typed/scheme], uses of
@scheme[define-struct] should be changed to @scheme[define-struct:].
@schemeblock[(: mag (pt -> Real))]
This declares that @scheme[mag] has the type @scheme[(pt -> Real)].
@;{@scheme[mag] must be defined at the top-level of the module containing
the declaration.}
The type @scheme[(pt -> Real)] is a function type, that is, the type
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]
structure. The @scheme[->] both indicates that this is a function
type and separates the domain from the range, or output type, in this
case @scheme[Real].
@schemeblock[
(define (mag p)
(sqrt (sqr (pt-x p)) (sqr (pt-y p))))
]
This definition is unchanged from the untyped version of the code.
The goal of Typed Scheme is to allow almost all definitions to be
typechecked without change. The typechecker verifies that the body of
the function has the type @scheme[Real], under the assumption that
@scheme[p] has the type @scheme[pt], taking these types from the
earlier type declaration. Since the body does have this type, the
program is accepted.
@section{Type Errors}
When Typed Scheme detects a type error in the module, it raises an
error before running the program.
@examples[#:eval the-eval
(add1 "not a number")
]
@;{
Typed Scheme also attempts to detect more than one error in the module.
@examples[#:eval the-eval
(string-append "a string" (add1 "not a number"))
]
}

138
collects/typed-scheme/scribblings/more.scrbl Normal file
View File

@ -0,0 +1,138 @@
#lang scribble/manual
@begin[(require "utils.ss"
scribble/core scribble/eval
(for-label typed/scheme mzlib/etc))]
@title[#:tag "more"]{More Features}
@(define the-eval (make-base-eval))
@(the-eval '(require typed/scheme))
The previous section introduced the basics of the Typed Scheme type
system. In this section, we will see several new features of the
language and the type system. The next
subsequent section will explain these features in more detail.
@section{Type Annotation and Binding Forms}
In general, variables in Typed Scheme must be annotated with their
type.
@subsection{Annotating Definitions}
We have already seen the @scheme[:] type annotation form. This is
useful for definitions, at both the top level of a module
@schemeblock[
(: x Number)
(define x 7)]
and in an internal definition
@schemeblock[
(let ()
(: x Number)
(define x 7)
(add1 x))
]
In addition to the @scheme[:] form, almost all binding forms from
@schememodname[scheme] have counterparts which allow the specification
of types. The @scheme[define:] form allows the definition of variables
in both top-level and internal contexts.
@schemeblock[
(define: x : Number 7)
(define: (id [z : Number]) z)]
Here, @scheme[x] has the type @scheme[Number], and @scheme[id] has the
type @scheme[(Number -> Number)]. In the body of @scheme[id],
@scheme[z] has the type @scheme[Number].
@subsection{Annotating Local Binding}
@schemeblock[
(let: ([x : Number 7])
(add1 x))
]
The @scheme[let:] form is exactly like @scheme[let], but type
annotations are provided for each variable bound. Here, @scheme[x] is
given the type @scheme[Number]. The @scheme[let*:] and
@scheme[letrec:] are similar.
@schemeblock[
(let-values: ([([x : Number] [y : String]) (values 7 "hello")])
(+ x (string-length y)))
]
The @scheme[let*-values:] and @scheme[letrec-values:] forms are similar.
@subsection{Annotating Functions}
Function expressions also bind variables, which can be annotated with
types. This function expects two arguments, a @scheme[Number] and a
@scheme[String]:
@schemeblock[(lambda: ([x : Number] [y : String]) (+ x 5))]
This function accepts at least one @scheme[String], followed by
arbitrarily many @scheme[Number]s. In the body, @scheme[y] is a list
of @scheme[Number]s.
@schemeblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))]
This function has the type @scheme[(String Number #,** -> Number)].
Functions defined by cases may also be annotated:
@schemeblock[(case-lambda: [() 0]
[([x : Number]) x])]
This function has the type
@scheme[(case-lambda (-> Number) (Number -> Number))].
@subsection{Annotating Single Variables}
When a single variable binding needs annotation, the annotation can be
applied to a single variable using a reader extension:
@schemeblock[
(let ([#,(annvar x Number) 7]) (add1 x))]
This is equivalent to the earlier use of @scheme[let:]. This is
especially useful for binding forms which do not have counterparts
provided by Typed Scheme, such as @scheme[let+]:
@schemeblock[
(let+ ([val #,(annvar x Number) (+ 6 1)])
(* x x))]
@subsection{Annotating Expressions}
It is also possible to provide an expected type for a particular
expression.
@schemeblock[(ann (+ 7 1) Number)]
This ensures that the expression, here @scheme[(+ 7 1)], has the
desired type, here @scheme[Number]. Otherwise, the type checker
signals an error. For example:
@interaction[#:eval the-eval
(ann "not a number" Number)]
@section{Type Inference}
@section{Subtyping}
@section{Occurrence Typing}
@section{Recursive Types}
@section{Polymorphism}
@include-section["varargs.scrbl"]
@section{Refinement Types}

48
collects/typed-scheme/scribblings/quick.scrbl Normal file
View File

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

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

@ -1,37 +1,29 @@
#lang scribble/doc #lang scribble/manual
@begin[(require scribble/manual) @begin[(require "utils.ss" (for-label typed/scheme))]
(require (for-label typed-scheme))]
@begin[
(define (item* header . args) (apply item @bold[header]{: } args))
(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
(define (gtech . x) (apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
(define (rtech . x) (apply tech x #:doc '(lib "scribblings/reference/reference.scrbl")))
]
@title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types} @title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types}
@author["Sam Tobin-Hochstadt"] @author["Sam Tobin-Hochstadt"]
@section-index["typechecking"] @section-index["typechecking" "typechecker" "typecheck"]
Typed Scheme is a Scheme-like language, with a type system that Typed Scheme is a family of languages, each of which enforce
supports common Scheme programming idioms. Explicit type declarations that programs written in the language obey a type system that ensures
are required --- that is, there is no type inference. The language the absence of many common errors. This guide is intended for programmers familiar
supports a number of features from previous work on type systems that with PLT Scheme. For an introduction to PLT Scheme, see the @(other-manual '(lib "scribblings/guide/guide.scrbl")).
make it easier to type Scheme programs, as well as a novel idea dubbed
@italic{occurrence typing} for case discrimination.
Typed Scheme is also designed to integrate with the rest of your PLT @local-table-of-contents[]
Scheme system. It is possible to convert a single module to Typed
Scheme, while leaving the rest of the program unchanged. The typed
module is protected from the untyped code base via
automatically-synthesized contracts.
Further information on Typed Scheme is available from @include-section["quick.scrbl"]
@link["http://www.ccs.neu.edu/home/samth/typed-scheme"]{the homepage}. @include-section["begin.scrbl"]
@include-section["more.scrbl"]
@section{How the Type System Works}
@section{Integrating with Untyped Code}
@;{
@section{Starting with Typed Scheme} @section{Starting with Typed Scheme}
If you already know PLT Scheme, or even some other Scheme, it should be If you already know PLT Scheme, or even some other Scheme, it should be
@ -191,7 +183,7 @@ process of elimination we can determine that @scheme[t] must be a
@scheme[node]. Therefore, we can use accessors such as @scheme[node]. Therefore, we can use accessors such as
@scheme[node-left] and @scheme[node-right] with @scheme[t] as input. @scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
@section{Polymorphism} @section[#:tag "poly"]{Polymorphism}
Typed Scheme offers abstraction over types as well as values. Typed Scheme offers abstraction over types as well as values.
@ -303,104 +295,4 @@ The new type constructor @scheme[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 @scheme[All] form.
@section{Variable-Arity Functions: Programming with Rest Arguments} }
Typed Scheme can handle some uses of rest arguments.
@subsection{Uniform Variable-Arity Functions}
In Scheme, one can write a function that takes an arbitrary
number of arguments as follows:
@schememod[
scheme
(define (sum . xs)
(if (null? xs)
0
(+ (car xs) (apply sum (cdr xs)))))
(sum)
(sum 1 2 3 4)
(sum 1 3)]
The arguments to the function that are in excess to the
non-rest arguments are converted to a list which is assigned
to the rest parameter. So the examples above evaluate to
@schemeresult[0], @schemeresult[10], and @schemeresult[4].
We can define such functions in Typed Scheme as well:
@schememod[
typed-scheme
(: sum (Number * -> Number))
(define (sum . xs)
(if (null? xs)
0
(+ (car xs) (apply sum (cdr xs)))))]
This type can be assigned to the function when each element
of the rest parameter is used at the same type.
@subsection{Non-Uniform Variable-Arity Functions}
However, the rest argument may be used as a heterogeneous list.
Take this (simplified) definition of the Scheme function @scheme[map]:
@schememod[
scheme
(define (map f as . bss)
(if (or (null? as)
(ormap null? bss))
null
(cons (apply f (car as) (map car bss))
(apply map f (cdr as) (map cdr bss)))))
(map add1 (list 1 2 3 4))
(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))]
Here the different lists that make up the rest argument @scheme[bss]
can be of different types, but the type of each list in @scheme[bss]
corresponds to the type of the corresponding argument of @scheme[f].
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
@scheme[as] corresponds to the first argument of @scheme[f]).
The example uses of @scheme[map] evaluate to @schemeresult[(list 2 3 4 5)],
@schemeresult[(list (list 1 4) (list 2 5) (list 3 6))], and
@schemeresult[(list 10 14 18)].
In Typed Scheme, we can define @scheme[map] as follows:
@schememod[
typed-scheme
(: map
(All (C A B ...)
((A B ... B -> C) (Listof A) (Listof B) ... B
->
(Listof C))))
(define (map f as . bss)
(if (or (null? as)
(ormap null? bss))
null
(cons (apply f (car as) (map car bss))
(apply map f (cdr as) (map cdr bss)))))]
Note that the type variable @scheme[B] is followed by an
ellipsis. This denotes that B is a dotted type variable
which corresponds to a list of types, much as a rest
argument corresponds to a list of values. When the type
of @scheme[map] is instantiated at a list of types, then
each type @scheme[t] which is bound by @scheme[B] (notated by
the dotted pre-type @scheme[t ... B]) is expanded to a number
of copies of @scheme[t] equal to the length of the sequence
assigned to @scheme[B]. Then @scheme[B] in each copy is
replaced with the corresponding type from the sequence.
So the type of @scheme[(inst map Integer Boolean String Number)]
is
@scheme[((Boolean String Number -> Integer)
(Listof Boolean) (Listof String) (Listof Number)
->
(Listof Integer))].

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

@ -1,29 +1,24 @@
#lang scribble/doc #lang scribble/manual
@begin[(require scribble/manual scribble/eval @begin[(require "utils.ss" scribble/eval
scheme/sandbox) scheme/sandbox)
(require (for-label typed-scheme (require (for-label typed/scheme
scheme/list srfi/14 scheme/list srfi/14
version/check))] version/check))]
@begin[
(define (item* header . args) (apply item @bold[header]{: } args))
(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
(define (gtech . x) (apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
(define (rtech . x) (apply tech x #:doc '(lib "scribblings/reference/reference.scrbl")))
]
@title[#:tag "top"]{The Typed Scheme Reference} @title[#:tag "top"]{The Typed Scheme Reference}
@author["Sam Tobin-Hochstadt"] @author["Sam Tobin-Hochstadt"]
@(defmodulelang typed-scheme) @(defmodulelang* (typed/scheme typed/scheme/base typed-scheme))
@section[#:tag "type-ref"]{Type Reference} @section[#:tag "type-ref"]{Type Reference}
@subsubsub*section{Base Types} @subsubsub*section{Base Types}
@deftogether[( @deftogether[(
@defidform[Number] @defidform[Number]
@defidform[Real]
@defidform[Integer] @defidform[Integer]
@defidform[Boolean] @defidform[Boolean]
@defidform[String] @defidform[String]
@ -126,8 +121,13 @@ result of @scheme[_loop] (and thus the result of the entire
expression in @scheme[body]).} expression in @scheme[body]).}
@deftogether[[ @deftogether[[
@defform[(letrec: ([v : t e] ...) . body)] @defform[(letrec: ([v : t e] ...) . body)]
@defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of @defform[(let*: ([v : t e] ...) . body)]
@scheme[letrec] and @scheme[let*].} @defform[(let-values: ([([v : t] ...) e] ...) . body)]
@defform[(letrec-values: ([([v : t] ...) e] ...) . body)]
@defform[(let*-values: ([([v : t] ...) e] ...) . body)]]]{
Type-annotated versions of
@scheme[letrec], @scheme[let*], @scheme[let-values],
@scheme[letrec-values], and @scheme[let*-values].}
@deftogether[[ @deftogether[[
@defform[(let/cc: v : t . body)] @defform[(let/cc: v : t . body)]

23
collects/typed-scheme/scribblings/utils.ss Normal file
View File

@ -0,0 +1,23 @@
#lang at-exp scheme
(require scribble/manual scribble/core)
(provide (all-defined-out))
(define (item* header . args) (apply item @bold[header]{: } args))
(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
(define (gtech . x)
(apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
(define (rtech . x)
(apply tech x #:doc '(lib "scribblings/reference/reference.scrbl")))
(define ** (let ([* #f]) @scheme[*]))
(define-syntax-rule (annvar x t)
(make-element #f (list @schemeparenfont["#{"]
@scheme[x : t]
@schemeparenfont["}"])))
(define-syntax-rule (annexpr x t)
(make-element #f (list @schemeparenfont["#{"]
@scheme[x :: t]
@schemeparenfont["}"])))

105
collects/typed-scheme/scribblings/varargs.scrbl Normal file
View File

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