From 0a8b1acb6f8c5a10249421e1d0b6755c3e93a61b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 25 Jan 2010 15:36:56 +0000
Subject: [PATCH] work on new guide

svn: r17814

original commit: e65535c88037da8c21876c9c4a7fcd62efdbe9d4
---
 collects/typed-scheme/info.ss                 |   4 +-
 collects/typed-scheme/scribblings/begin.scrbl |  81 ++++++++++
 collects/typed-scheme/scribblings/more.scrbl  | 138 +++++++++++++++++
 collects/typed-scheme/scribblings/quick.scrbl |  48 ++++++
 .../{ => scribblings}/ts-guide.scrbl          | 144 +++---------------
 .../{ => scribblings}/ts-reference.scrbl      |  24 +--
 collects/typed-scheme/scribblings/utils.ss    |  23 +++
 .../typed-scheme/scribblings/varargs.scrbl    | 105 +++++++++++++
 8 files changed, 427 insertions(+), 140 deletions(-)
 create mode 100644 collects/typed-scheme/scribblings/begin.scrbl
 create mode 100644 collects/typed-scheme/scribblings/more.scrbl
 create mode 100644 collects/typed-scheme/scribblings/quick.scrbl
 rename collects/typed-scheme/{ => scribblings}/ts-guide.scrbl (65%)
 rename collects/typed-scheme/{ => scribblings}/ts-reference.scrbl (95%)
 create mode 100644 collects/typed-scheme/scribblings/utils.ss
 create mode 100644 collects/typed-scheme/scribblings/varargs.scrbl

diff --git a/collects/typed-scheme/info.ss b/collects/typed-scheme/info.ss
index e245bb52..c18cc35e 100644
--- a/collects/typed-scheme/info.ss
+++ b/collects/typed-scheme/info.ss
@@ -1,4 +1,4 @@
 #lang setup/infotab
 
-(define scribblings '(("ts-reference.scrbl" ())
-		      ("ts-guide.scrbl" ())))
+(define scribblings '(("scribblings/ts-reference.scrbl" ())
+		      ("scribblings/ts-guide.scrbl" (multi-page))))
diff --git a/collects/typed-scheme/scribblings/begin.scrbl b/collects/typed-scheme/scribblings/begin.scrbl
new file mode 100644
index 00000000..d20cd329
--- /dev/null
+++ b/collects/typed-scheme/scribblings/begin.scrbl
@@ -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"))
+]
+}
\ No newline at end of file
diff --git a/collects/typed-scheme/scribblings/more.scrbl b/collects/typed-scheme/scribblings/more.scrbl
new file mode 100644
index 00000000..154f9d32
--- /dev/null
+++ b/collects/typed-scheme/scribblings/more.scrbl
@@ -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}
diff --git a/collects/typed-scheme/scribblings/quick.scrbl b/collects/typed-scheme/scribblings/quick.scrbl
new file mode 100644
index 00000000..6486194b
--- /dev/null
+++ b/collects/typed-scheme/scribblings/quick.scrbl
@@ -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|
diff --git a/collects/typed-scheme/ts-guide.scrbl b/collects/typed-scheme/scribblings/ts-guide.scrbl
similarity index 65%
rename from collects/typed-scheme/ts-guide.scrbl
rename to collects/typed-scheme/scribblings/ts-guide.scrbl
index 75c0b713..dd604dde 100644
--- a/collects/typed-scheme/ts-guide.scrbl
+++ b/collects/typed-scheme/scribblings/ts-guide.scrbl
@@ -1,37 +1,29 @@
-#lang scribble/doc
+#lang scribble/manual
 
-@begin[(require scribble/manual)
-       (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")))
-]
+@begin[(require "utils.ss" (for-label typed/scheme))]
 
 @title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types}
 
 @author["Sam Tobin-Hochstadt"]
 
-@section-index["typechecking"]
+@section-index["typechecking" "typechecker" "typecheck"]
 
-Typed Scheme is a Scheme-like language, with a type system that
-supports common Scheme programming idioms.  Explicit type declarations
-are required --- that is, there is no type inference.  The language
-supports a number of features from previous work on type systems that
-make it easier to type Scheme programs, as well as a novel idea dubbed
-@italic{occurrence typing} for case discrimination.
+Typed Scheme is a family of languages, each of which enforce
+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 
+with PLT Scheme.  For an introduction to PLT Scheme, see the @(other-manual '(lib "scribblings/guide/guide.scrbl")).
 
-Typed Scheme is also designed to integrate with the rest of your PLT
-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.
+@local-table-of-contents[]
 
-Further information on Typed Scheme is available from
-@link["http://www.ccs.neu.edu/home/samth/typed-scheme"]{the homepage}.
+@include-section["quick.scrbl"]
+@include-section["begin.scrbl"]
+@include-section["more.scrbl"]
 
+@section{How the Type System Works}
+
+@section{Integrating with Untyped Code}
+
+@;{
 @section{Starting with Typed Scheme}
 
 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-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.
 
@@ -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
 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))].
+}
\ No newline at end of file
diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl
similarity index 95%
rename from collects/typed-scheme/ts-reference.scrbl
rename to collects/typed-scheme/scribblings/ts-reference.scrbl
index 3e7731dc..7b390e9a 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/scribblings/ts-reference.scrbl
@@ -1,29 +1,24 @@
-#lang scribble/doc
+#lang scribble/manual
 
-@begin[(require scribble/manual scribble/eval
+@begin[(require "utils.ss" scribble/eval
                 scheme/sandbox)
-       (require (for-label typed-scheme
+       (require (for-label typed/scheme
                            scheme/list srfi/14
                            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} 
 
 @author["Sam Tobin-Hochstadt"]
 
-@(defmodulelang typed-scheme)
+@(defmodulelang* (typed/scheme typed/scheme/base typed-scheme))
 
 @section[#:tag "type-ref"]{Type Reference}
 
 @subsubsub*section{Base Types}
 @deftogether[(
 @defidform[Number]
+@defidform[Real]
 @defidform[Integer]
 @defidform[Boolean]
 @defidform[String]
@@ -126,8 +121,13 @@ result of @scheme[_loop] (and thus the result of the entire
 				expression in @scheme[body]).}
 @deftogether[[
 @defform[(letrec: ([v : t e] ...) . body)]
-@defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of
-@scheme[letrec] and @scheme[let*].}
+@defform[(let*: ([v : t e] ...) . body)]
+@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[[
 @defform[(let/cc: v : t . body)]
diff --git a/collects/typed-scheme/scribblings/utils.ss b/collects/typed-scheme/scribblings/utils.ss
new file mode 100644
index 00000000..885f82c6
--- /dev/null
+++ b/collects/typed-scheme/scribblings/utils.ss
@@ -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["}"])))
diff --git a/collects/typed-scheme/scribblings/varargs.scrbl b/collects/typed-scheme/scribblings/varargs.scrbl
new file mode 100644
index 00000000..2e8022c6
--- /dev/null
+++ b/collects/typed-scheme/scribblings/varargs.scrbl
@@ -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))].