Static type system
==================

Scheme48 supports a rudimentary static type system.  It is intended mainly to catch some classes of type and arity mismatch errors early, at compile-time.  By default, there is only extremely basic analysis, which is typically only good enough to catch arity errors and the really egregious type errors.  The full reconstructor, which is still not very sophisticated, is enabled by specifying an optimizer pass that invokes the code usage analyzer.  The only optimizer pass built-in to Scheme48, the automatic procedure integrator, named auto-integrate, does so.

The type reconstructor attempts to assign the most specific type it can to program terms, signalling warnings for terms that are certain to be invalid by Scheme's dynamic semantics.  Since the reconstructor is not very sophisticated, it frequently gives up and assigns very general types to many terms.  Note, however, that it is very lenient in that it only assigns more general types: it will never signal a warning because it could not reconstruct a very specific type.  For example, the following program will produce no warnings:

     (define (foo x y) (if x (+ y 1) (car y))) lisp

     Calls to foo that are clearly invalid, such as (foo #t
     'a), could cause the type analyzer to signal warnings, but it is not
     sophisticated enough to determine that foo's second argument
     must be either a number or a pair; it simply assigns a general value
     type (see below).

     There are some tricky cases that depend on the order by which arguments
     are evaluated in a combination, because that order is not specified in
     Scheme.  In these cases, the relevant types are narrowed to the most
     specific ones that could not possibly cause errors at run-time for any
     order.  For example,

          (lambda (x) (+ (begin (set! x '(3)) 5) (car x))) lisp

          will be assigned the type (proc (:pair) :number), because, if
          the arguments are evaluated right-to-left, and x is not a pair,
          there will be a run-time type error.

          The type reconstructor presumes that all code is potentially reachable,
          so it may signal warnings for code that the most trivial control flow
          analyzer could decide unreachable.  For example, it would signal a
          warning for (if #t 3 (car 7)).  Furthermore, it does not account
          for continuation throws; for example, though it is a perfectly valid
          Scheme program, the type analyzer might signal a warning for this code:

               (call-with-current-continuation
                 (lambda (k) (0 (k)))) lisp

               The type system is based on a type lattice.  There are several maximum
               or `top' elements, such as :values, :syntax, and
               :structure; and one minimum or `bottom' element, :error.
               This description of the type system makes use of the following
               notations: E : T means that the term E has the
               type, or some compatible subtype of, T; and TA
               subtype TB means that TA is a compatible
               subtype of TB --- that is, any term whose static type is
               TA is valid in any context that expects the type
               TB ---.

               Note that the previous text has used the word `term,' not `expression,'
               because static types are assigned to not only Scheme expressions.  For
               example, cond macro has the type :syntax.  Structures in
               the configuration language also have static types: their interfaces.
               (Actually, they really have the type :structure, but this is a
               deficiency in the current implementation's design.)  Types, in fact,
               have their own type: :type.  Here are some examples of values,
               first-class or otherwise, and their types:

                    cond : :syntax

                    (values 1 'foo '(x . y))
                      : (some-values :exact-integer :symbol :pair)

                    :syntax : :type

                    3 : :exact-integer

                    (define-structure foo (export a b) ...)
                    foo : (export a b) example

                    One notable deficiency of the type system is the absence of any sort of
                    parametric polymorphism.

                     -- type constructor: join type ...
                     -- type constructor: meet type ...
                         Join and meet construct the supremum and infimum elements
                         in the type lattice of the given types.  That is, for any two disjoint
                         types TA and TB, let TJ be
                         (join TA TB) and TM be
                         (meet TA TB):

                           * TJ subtype TA and TJ subtype TB

                           * TA subtype TM and TB subtype TM

                         For example, (join :pair :null) allows either pairs or nil,
                         ie lists, and (meet :integer :exact) accepts only integers
                         that are also exact.

                         (More complete definitions of supremum, infimum, and other elements of
                         lattice theory, may be found elsewhere.)

                     -- type: :error
                         This is the minimal, or `bottom,' element in the type lattice.  It is
                         the type of, for example, calls to error.

                     -- type: :values
                     -- type: :arguments
                         All Scheme expressions have the type :values.  They may
                         have more specific types as well, but all expressions' types are
                         compatible subtypes of :values.  :Values is a maximal
                         element of the type lattice.  :Arguments is synonymous with
                         :values.

                     -- type: :value
                         Scheme expressions that have a single result have the type
                         :value, or some compatible subtype thereof; it is itself a
                         compatible subtype of :values.

                     -- type constructor: some-values type ...
                         Some-values is used to denote the types of expressions that have
                         multiple results: if E1 ... EN have
                         the types T1 ... TN, then the Scheme
                         expression (values E1 ... EN) has
                         the type (some-values T1 ... TN).

                         Some-values-constructed types are compatible subtypes of
                         :values.

                         Some-values also accepts `optional' and `rest' types, similarly
                         to Common Lisp's `optional' and `rest' formal parameters.  The sequence
                         of types may contain a &opt token, followed by which is any
                         number of further types, which are considered to be optional.  For
                         example, make-vector's domain is (some-values
                         :exact-integer &opt :value).  There may also be a &rest token,
                         which must follow the &opt token if there is one.  Following the
                         &rest token is one more type, which the rest of the sequents in
                         a sequence after the required or optional sequents must satisfy.  For
                         example, map's domain is (some-values :procedure (join
                         :pair :null) &rest (join :pair :null)): it accepts one procedure and
                         at least one list (pair or null) argument.

                     -- type constructor: procedure domain codomain
                     -- type constructor: proc (arg-type ...) result-type
                         Procedure type constructors.  Procedure types are always compatible
                         subtypes of :value.  Procedure is a simple constructor
                         from a specific domain and codomain; DOMAIN and CODOMAIN
                         must be compatible subtypes of :values. Proc is a more
                         convenient constructor.  It is equivalent to (procedure
                         (some-values ARG-TYPE ...) RESULT-TYPE).

                     -- type: :boolean
                     -- type: :char
                     -- type: :null
                     -- type: :unspecific
                     -- type: :pair
                     -- type: :string
                     -- type: :symbol
                     -- type: :vector
                     -- type: :procedure
                     -- type: :input-port
                     -- type: :output-port
                         Types that represent standard Scheme data.  These are all compatible
                         subtypes of :value.  :Procedure is the general type for
                         all procedures; see proc and procedure for procedure
                         types with specific domains and codomains.

                     -- type: :number
                     -- type: :complex
                     -- type: :real
                     -- type: :rational
                     -- type: :integer
                         Types of the Scheme numeric tower.  :integer subtype :rational
                         subtype :real subtype :complex subtype :number

                     -- type: :exact
                     -- type: :inexact
                     -- type: :exact-integer
                     -- type: :inexact-real
                         :Exact and :inexact are the types of exact and inexact
                         numbers, respectively.  They are typically met with one of the types in
                         the numeric tower above; :exact-integer and :inexact-real
                         are two conveniences for the most common meets.

                     -- type: :other
                         :Other is for types that do not fall into any of the previous
                         value categories.  (:other subtype :value)  All new types
                         introduced, for example by Type annotations,loophole,
                         are compatible subtypes of :other.

                     -- type constructor: variable type
                         This is the type of all assignable variables, where TYPE
                         subtype :value.  Assignment to variables whose types are value
                         types, not assignable variable types, is invalid.

                     -- type: :syntax
                     -- type: :structure
                         :Syntax and :structure are two other maximal elements of
                         the type lattice, along with :values.  :Syntax is the
                         type of macros or syntax transformers.  :Structure is the
                         general type of all structures.

Types in the configuration language
-----------------------------------

Scheme48's configuration language has several places in which to write types.  However, due to the definitions of certain elements of the configuration language, notably the export syntax, the allowable type syntax is far more limited than the above.  Only the following are provided:

 -- type: :values
 -- type: :value
 -- type: :arguments
 -- type: :syntax
 -- type: :structure
     All of the built-in maximal elements of the type lattice are provided, as well as the simple compatible subtype :values, :value.

 -- type: :boolean
 -- type: :char
 -- type: :null
 -- type: :unspecific
 -- type: :pair
 -- type: :string
 -- type: :symbol
 -- type: :vector
 -- type: :procedure
 -- type: :input-port
 -- type: :output-port
 -- type: :number
 -- type: :complex
 -- type: :real
 -- type: :rational
 -- type: :integer
 -- type: :exact-integer
     These are the only value types provided in the configuration language. Note the conspicuous absence of :exact, :inexact, and :inexact-real.

 -- type constructor: procedure domain codomain
 -- type constructor: proc (arg-type ...) result-type
     These two are the only type constructors available.  Note here the conspicuous absence of some-values, so procedure types that are constructed by procedure can accept only one argument (or use the overly general :values type) & return only one result (or, again, use :values for the codomain), and procedure types that are constructed by proc are similar in the result type.