A Type Notation for Scheme

by Gary T. Leavens and Curtis Clifton

Department of Computer Science, Iowa State University,
226 Atanasoff Hall, Ames, Iowa, 50011-1040 USA

Copyright (c) Gary T. Leavens and Curtis Clifton, 2001.


1. Overview of the Type System

Our type checker for Scheme is invoked by loading the file `type-check-and-eval.scm' into Scheme [R5RS] from a library. This is usually done automatically by using a special command such as scm342typed or scm54typed, which loads the appropriate files.

When you run the type checker using a command like scm342typed or scm54typed, the automatically-loaded file `type-check-and-eval.scm' starts a new read-eval-print loop. This loop, reads a Scheme expression from the user's input, type checks it, and if it does type check, proceeds to evaluate it using the standard scheme evaluator. If the expression seems to contain a type error, execution is not attempted, and instead an error message is printed.

Scheme files loaded from the read-eval-print loop are also type checked, as are files that are loaded from other files being loaded, etc. Scheme files may themselves contain type declarations, but such declarations may also be present in a separate file. Such a file of type declarations is associated with the Scheme file by the use of a different suffix, `.def'. For example, if the Scheme file is named `displayln.scm', the associated `.def' file is named `displayln.def'. This `.def' file is read to supplement the type information in the Scheme file. This system permits the Scheme file to have no type annotations, if desired, which makes the Scheme file more easily portable to other systems that are not using our type checker.

A Scheme file with our type annotations can, however, be used in any Scheme system. To do this, one must first load the file `type-check-ignore-types-at-runtime.scm'. This file contains macros that ignore our type annotation syntax at run-time. This file is also loaded automatically by commands such as scm342untyped or scm54untyped. By loading this file, these commands tell Scheme enough about the type notation to ignore it. Otherwise they act just like standard Scheme.

The following sections describe the notation for type expressions used in the checker, our additions to Scheme for declaring various kinds of type information, some hints on what type errors may mean, and various configuration parameters and commands recognized by the type checker. See section A. Grammar Summary for a summary of the type checker's additions to Scheme's syntax.

2. Notation for Type Expressions

In this section we discuss the notations used in type expressions and their meaning.

A type can be thought of as a set of values with certain associated procedures. For example we use number as the name of the type of all numbers (both exact and inexact, real and integer) in Scheme. The procedures that work on numbers include + and *.

Types can also be thought of as abstractions of the type predicates found in Scheme. For example, the type number is an abstraction of the built-in Scheme predicate number? in the sense that if (number? x) is true, then x has type number. The following table gives an overview of this abstraction, by relating types to type predicates, and by giving some examples of expressions that satisfy the given predicates. (If this is confusing at this point, you may want to come back to it after you have read about the notation below.)

       Correspondence between types, predicates, and expressions

   Type                Type                  Example expressions that:
   expression          predicate             have type, satisfy predicate
   ------------------------------------------------------------------
   boolean             boolean?              #t, #f
   char                char?                 #\a, #\Z, #\newline
   number              number?               0, 342.54, -3
   input-port          input-port?           (current-input-port)
   output-port         output-port?          (current-output-port)
   string              string?               "a string", ""
   symbol              symbol?               'a-symbol, (quote this)
   datum               datum?                #t, #\a, 0, "a str", sym
   poof                poof?                 (error "bad index")
   void                void?                 (newline)
   (list-of number)    (list-of number?)     (list 3 4), '(2 2 7), '()
   (list-of datum)     (list-of datum?)      (list 3 #t 3 #\a), '()
   (list-of char)      (list-of char?)       (list #\a #\b), '()
   (vector-of number)  (vector-of number?)   (vector 3 4), '#(2 2 7), '#()
   (vector-of char)    (vector-of char?)     (vector #\a #\b), '#()
   (pair-of char char) (pair-of char? char?) (cons #\a #\b), '(#\a . #\b)
   (-> () char)        (-> () char?)         (lambda () #\a)
   (-> () void)        (-> () void?)         newline

   (-> (char)          (-> (char?)           (lambda (c)
       boolean)            boolean?)             (eqv? #\a c))

   (-> (number ...)    (-> (number? ...)     +, *
       number)             number?)          

The non-standard type predicates that are used above are all defined in the file `type-predicates.scm'. This file should be included with the type checker.

To begin explaining all of this, we start with the grammar for type expressions.

type-exp ::= monomorphic-type
          | polymorphic-type
monomorphic-type ::= basic-type
          | applied-type
          | procedure-type
          | intersection-type
          | variant-record-type
          | type-predicate-type

Type expressions are pieces of syntax that denote various types. The rest of this section explains each of these pieces of the syntax. See section 2.4 Polymorphic Types for the syntax of polymorphic-type.

2.1 Basic Types

The syntax of a basic-type is as follows.

basic-type ::= identifier
identifier ::= an <identifier> in the Scheme syntax [R5RS].

A basic type is either a built-in type, such as number, a type variable (see section 2.4 Polymorphic Types), or a user-defined type (see section 3.2.2 Define-Datatype Definitions).

Some of the built-in types are the types used for atomic data items in Scheme. These are displayed in the following table.

          Built-in Basic Types For Atomic Scheme Data

   Name        Example expressions that have that type
   ----------------------------------------------------
   boolean      #t, #f
   char         #\a, #\Z
   number       0, 342.54, -3
   string       "a string", ""
   symbol       'a-symbol, (quote this)
   input-port   (current-input-port)
   output-port  (current-output-port)

The type checker also knows about several other special basic types: datum, poof, and void. These are described below.

2.1.1 Datum

The built-in basic type datum is the type of all the values in Scheme. Every Scheme object has this type; that is, datum is the supertype of all types. (In the literature on type checking, such a type is sometimes called "top".)

One use of datum is in type checking heterogeneous lists. In Scheme the elements of a list do not all have to be of the same type; such a list is heterogeneous. A list whose elements are all of the same type is homogeneous. The type checker uses types of the form (list-of T) for lists whose elements all have some type T. (See section 2.2 Applied Types for the meaning of list-of.) For example, a list of booleans such as (#t #f) has the type (list-of boolean), and a list of numbers such as (3 4 2) has the type (list-of number). For a list such as (#t 3 #f), the type checker uses the type (list-of datum).

Although datum is the supertype of all types, the type checker does not infer that an expression has type datum unless forced to do so [Jenkins-Leavens96]. One reason for this is to give better error messages, since otherwise every expression would have a type datum.

2.1.2 Void

The built-in basic type void, as in C, C++, or Java, is used to represent the return type of a procedure that returns but doesn't return a useful result. For example, Scheme's procedure display has the following type.

   (-> (datum) void)

This means that a call such as (display 'Scheme) has no value, and should only be used for its side effects.

See section 2.3 Procedure Types for an explanation of the -> syntax.

2.1.3 Poof

The built-in basic type poof is used for the return types of procedures that do not return to their caller. An example is the built-in Scheme procedure error, whose type is the following.

   (-> (datum ...) poof)

This means that a call such as (error 'wrong!) does not return to its caller.

The type checker considers poof to be a subtype of all types [Jenkins-Leavens96]. The reason for this is to allow code such as the following to type check.

   (if (not (zero? denom))
       (/ num denom)                 ; has type: number
       (error "zero denominator!"))  ; has type: poof

It is sensible that the above expression has type number, because when it has a value at all, that value is of type number.

2.2 Applied Types

The syntax of an applied-type is as follows. The notation { type-exp }+ means one or more repetitions of the nonterminal type-exp.

applied-type ::= ( identifier { type-exp }+ )

Applied types denote the result of applying some type constructor, such as list-of or vector-of to one or more type parameters. For example, we write (list-of number) for the type of lists of numbers. The lists (1 2 3) and (3.14 2.73) both have this type. In the type (list-of number), list-of is the type constructor, and number is the only type parameter. The application of a type constructor to one or more type parameters produces an instance of that type constructor.

Some of the built-in type constructors are used for the types of non-atomic data in Scheme. These are displayed in the following table.

          Example Instances of Built-in Type Constructors

   Instance                Example expressions that have that type
   -----------------------------------------------------------
   (list-of number)        (list 3 4 2)
   (list-of boolean)       (cons #t (cons #f '()))
   (vector-of number)      (vector 5 4)
   (pair-of number number) (cons 3 4)

Type constructors are symbols, and cannot be type variables (see section 2.4 Polymorphic Types).

2.3 Procedure Types

The syntax of procedure types is given below.

procedure-type ::= ( -> ( { type-exp }* ) type-exp )
          | ( -> ( { type-exp }* type-exp ... ) type-exp )

In the above, the notation { type-exp }* means zero or more repetitions of the nonterminal type-exp. The symbol ... used in the second alternative is a terminal symbol in the grammar; it is used in the types of variable argument procedures.

We explain the two different kinds of procedure types below.

2.3.1 Procedure Types with Fixed Numbers of Arguments

A procedure type denotes the type of a Scheme procedure. In the notation, the types of the arguments are enclosed in parentheses, and these are followed by the type that the procedure returns. For example, the Scheme procedure substring has the following type.

   (-> (string number number) string)

This means that substring is a procedure with 3 arguments, the first of type string, the second of type number, and the third of type number, which returns a string.

You can derive such a type from a lambda expression systematically. Take the lambda expression, replace lambda by ->, replace each formal parameter name by its type, and replace the body by its type. For example, the type of the lambda expression

   (lambda (n m) (+ 2 (+ n m)))

is the following.

      (-> (number number) number)

As another example, the type of sum in the following definition

   (define sum
      (lambda (ls)
        (if (null? ls)
            0
           (+ (car ls) (sum (cdr ls))))))

is the following.

   (-> ((list-of number)) number)

2.3.2 Variable Argument Procedure Types

A variable argument procedure type denotes the type of a procedure constructed with Scheme's "unrestricted lambda". The notation is just like that of a normal procedure type (see section 2.3.1 Procedure Types with Fixed Numbers of Arguments), except that the last thing in the list of argument types is a type expression followed by .... This means that the procedure may take 0 or more actual arguments of the type immediately preceding .... For example, consider the type

   (-> (number ...) number)

This is the type of a procedure that takes 0 or more arguments of type number. This is the type of sum* in the following.

   (define sum*
     (lambda args
       (sum args)))

It follows that all of the following calls to sum* have type number.

   (sum* )
   (sum* 1)
   (sum* 2 1)
   (sum* 3 2 1)
   (sum* 4 3 2 1)

As another example, the lambda expression

   (lambda (num1 . nums) (sum (cons num1 nums)))

has the following type.

   (-> (number number ...) number)

Note that, unlike the type of sum*, the above type only permits calls with one or more numbers as arguments, and does not permit calls with no arguments.

2.4 Polymorphic Types

A polymorphic type denotes a family of types, all of which have a similar shape. The shape of the instances in this family are described by the type-exp in the following syntax.

polymorphic-type ::= ( forall type-formals monomorphic-type )
type-formals ::= ( { type-variable }* )
type-variable ::= identifier

Because of the type inference algorithm [Milner78] used in the type checker [Jenkins-Leavens96], the type checker cannot deal with nested polymorphic types. This is why the syntax for polymorphic-type only permits a monomorphic-type inside the forall. See section 2. Notation for Type Expressions for the syntax of monomorphic-type.

Indeed, as a predicate transformer, the run-time version of forall is the same as lambda (see section 3.1.5 Forall Expressions). In type checking, the notion that corresponds to calling this lambda is called instantiation.

To explain what instantiation of a polymorphic type means, consider the following example.

   (forall (T) (list-of T))

If we instantiate this type, by supplying a type, such as number, for the type variable T, we obtain an instance of the above type, in this case (list-of number). The following are all instances of the type (forall (T) (list-of T)).

   (list-of number)
   (list-of boolean)
   (list-of char)
   (list-of (vector-of number))
   (list-of (vector-of boolean))
   (list-of (-> (number) number))
   (list-of (-> ((list-of number)) number))
   (list-of (list-of number))
   (list-of (list-of (list-of boolean)))

Each polymorphic type has an infinite number of instances.

Armed with the notion of instantiation, and of the instances of a polymorphic type, we can describe the meaning of a polymorphic type. Using the analogy between types and sets, a polymorphic type denotes an infinite intersection of the sets that its instances denote. Thus, for example, the type (forall (T) (list-of T)) denotes the infinite intersection of all of its instances, including those listed above. It turns out that the only Scheme value with this type is the empty list, (). Another way of saying this is to say that () has the type (list-of T) for all types T.

Using the analogy between types and predicates, a polymorphic type denotes a predicate transformer. This predicate transformer, when given predicates corresponding to each of the formals, returns a predicate. The returned predicate is the denotation of the corresponding instance of the polymorphic type. For example, the type (forall (T) (list-of T)) denotes a predicate transformer we write as (forall (T?) (list-of T?)), which is equivalent to (lambda (T?) (list-of T?)). When applied to a type predicate, such as number?, this predicate transformer returns the predicate (list-of number?). Since the predicate number? corresponds to the type number, this means that the predicate (list-of number?) should correspond to the instance (list-of number), which it does. This can be illustrated as follows.

   (forall (T) (list-of T))  -- denotes -->  (forall (T?) (list-of T?))
              !
              !                                          ||
              !
              !                              (lambda (T?) (list-of T?))
              !                                          !
          applied to                                 applied to
           number                                     number?
           yields                                     yields
              !                                          !
              !                                          !
              v                                          v
        (list-of number)    -- denotes -->        (list-of number?)

Another way to illustrate this analogy is through the following table.

    Types generators, predicate transformers, and expressions

   Type                Type                  Example expressions that:
   expression          predicate             have type, satisfy predicate
                       transformer           for all values of formals
   ------------------------------------------------------------------
   (forall (T)         (forall (T?)           
     (list-of T))        (list-of T?))       '()

   (forall (T)         (forall (T?)            
     (-> (T)             (-> (T?)            (lambda (x) 
         char))              char?))            #\a)

   (forall (S T)       (forall (S? T?)         
    (-> (S T)           (-> (S? T?)          (lambda (x y)
        T))                 T?))                y)

   (forall (T)         (forall (T?)           
    (-> (T T ...)       (-> (T? T? ...)       (lambda args
        T))                  T?))                (car args))

   (forall (S T U)     (forall (S? T? U?)     
    (all-of             (all-of               cons
     (-> (T              (-> (T?              
          (list-of T))        (list-of T?))   
         (list-of T))        (list-of T?))    
     (-> (S (list-of U)) (-> (S? (list-of U?))
         (list-of            (list-of         
          datum))))           datum?))))      

As illustrated above, polymorphic types are especially useful for describing the types of higher-order functions. For such functions, one often needs to describe procedure types that are not as specific as the ones used in the previous subsection, but which are also not so general as datum.

In making instances, it is important to replace type variables consistently throughout. For example, Scheme's built in procedure map has the following type.

   (forall (S T)
     (-> ((-> (S) T) (list-of S)) (list-of T)))

This means that when map is used, the type checker must find two types S and T such that the first argument to map has type (-> (S) T), and the second has type (list-of S); once the specific types for S and T are chosen, consistent replacement dictates that the result of a call will have type (list-of T). For example, consider type checking the following call.

   (map odd? (list 3 4 2 3))

Since the type of odd? is (-> (number) boolean), the type checker is forced to choose number for S and boolean for T; these are the only choices that match the type of odd? correctly against the type of map's first argument. Once the type checker has made this choice, however, it is no longer free to use different types for S and T in checking the rest of the application. So it must check that the second argument in the call has type (list-of number), because it must consistently replace S with number. Similarly it must give the type of the result as (list-of boolean), because it must consistently replace T with boolean.

Another way to view this process is that the type checker chooses an instance of map's type, and uses that in type checking the call. The instance it uses is the following.

   (-> ((-> (number) boolean) (list-of number)) (list-of boolean))

What instance would be used in checking the types of the following application?

   (map (lambda (n) (+ n 1)) '(3 -2 1))

Since datum is a type expression, it can be used in an instance to replace type variables in a polymorphic type expression. For example, one type for Scheme's cons procedure is as follows.

   (forall (T) (-> (T (list-of T)) (list-of T)))

This has the type (-> (datum (list-of datum)) (list-of datum)) as an instance.

2.5 Intersection Types

The syntax of an intersection-type is as follows.

intersection-type ::= ( all-of { type-exp }+ )

Here the notation { type-exp }+ means one or more repetitions of the nonterminal type-exp.

If one thinks of types as sets of values, then an intersection type can be thought of as the intersection of several such sets. If one thinks of types as predicates, then an intersection type corresponds to the application of all of the predicates and a conjunction of the results. Therefore, if x has type (all-of S T), then x has both type S and type T. For example, since '() has both types (list-of number) and (list-of boolean), the empty list also has the following type.

   (all-of (list-of number) (list-of boolean))

One use of such intersection types is for procedures that can be used in several ways. For example, Scheme's cons procedure can make homogeneous lists, heterogeneous lists, and pairs. Thus a better type for cons than the one given above is the following.

   (forall (S T U V W)
     (all-of (-> (T (list-of T)) (list-of T))
             (-> (S (list-of U)) (list-of datum))
             (-> (V W) (pair-of V W))))

The type checker considers the order of types listed in an intersection type when doing type inference [Jenkins-Leavens96]. It will first try to use the first type listed, then the second, and so on. For example, in the expression (cons 2 '(3)), the arguments to cons are of type number and (list-of number), so the type checker uses an instance of the first type in the above intersection type for cons, (-> (T (list-of T)) (list-of T)), and so the type of the expression is inferred to be (list-of number). However, the type of the expression (cons 2 '(#t)) is inferred to be (list-of datum) since there is no instance of the first type in the intersection type that matches the argument types. (This is because T cannot be consistently replaced by both number and boolean. See section 2.4 Polymorphic Types for more about consistent replacement.) Finally, the type of the expression (cons 2 3) is inferred to be (pair-of number number), since no instance of either of the first two types for cons matches the second argument's type.

The type checker never infers that an expression has an intersection type unless it is forced to do so. However, one can use deftype (see section 3.2.1 Deftype) to declare such a type. The types of built-in procedures such as cons make heavy use of carefully constructed intersection types.

2.6 Variant Record Types

The syntax of an variant-record-type is as follows.

variant-record-type ::= ( variant-record { variant }+ )
variant ::= ( identifier { field-type-binding }* )
field-type-binding ::= ( identifier type-exp )

Again, the notation { variant }+ means one or more repetitions of the nonterminal variant, and the notation { field-type-binding }* means zero or more repetitions of the nonterminal field-type-binding,

A variant record type is the type of a name defined with define-datatype (see section 3.2.2 Define-Datatype Definitions) [Friedman-Wand-Haynes01]. It lists the complete set of variants and their field-type bindings. Each field-type binding associates a field name with the name of that field's type. The order among the field-type bindings in a variant is significant, but the order among the variants themselves is not.

For example, given the following define-datatype declaration

   (define-datatype pi-calc-expr pi-calc-expr?
     (parallel-composition (list-of pi-calc-expr?))
     (restriction (name symbol?) (body pi-calc-expr?))
     (input (name symbol?) (formals (list-of symbol?))
            (body pi-calc-expr?))
     (output (name symbol?) (actuals (list-of symbol?)))
     (replication (body pi-calc-expr?))
     (null ))

then the name pi-calc-expr has the following type:

   (variant-record
     (parallel-composition (list-of pi-calc-expr))
     (restriction (name symbol) (body pi-calc-expr))
     (input (name symbol) (formals (list-of symbol))
            (body pi-calc-expr))
     (output (name symbol) (actuals (list-of symbol)))
     (replication (body pi-calc-expr))
     (null ))

A variant record S is a subtype of another variant record type T if for each variant of S there is a corresponding variant in T with the same identifier, the same number of fields, and such that the nth field in the variant of S, the field type is a subtype of the field type of T's nth field.

2.7 Type Predicate Types

The syntax of an type-predicate-type is as follows.

type-predicate-type ::= ( type-predicate-for type-exp )

A type predicate is a procedure that can be applied to any Scheme object, and yields a boolean value; hence a type predicate type such as (type-predicate-for number) is a subtype of (-> (datum) boolean), meaning that a type predicate can be used anywhere a procedure of type (-> (datum) boolean) is required. However, type predicate types are used by the type checker to infer the type tested for by the Scheme expressions used in define-datatype declarations (see section 3.2.2 Define-Datatype Definitions).

The following are some examples of type predicate types and expressions that have those types.

   Type                                  Expressions that:
   expression                            have that type
   ------------------------------------------------------------------
   (type-predicate-for boolean)          boolean?
   (type-predicate-for char)             char?
   (type-predicate-for number)           number?
   (type-predicate-for string)           string?
   (type-predicate-for symbol)           symbol?
   (type-predicate-for datum)            datum?
   (type-predicate-for (list-of number)) (list-of number?)
   (type-predicate-for (list-of char))   (list-of char?)
   (type-predicate-for (vector-of char)) (vector-of char?)

3. Additions to Scheme

This section describes additions that the type checker makes to Scheme's expressions, definitions, top-level forms, and programs.

3.1 Expressions Added To Scheme

The type checker adds the following syntax to Scheme expressions. See the formal syntax in the Revised(5) Report on Scheme [R5RS] for the syntax of Scheme's standard expression, i.e., for other alternative productions for expression.

expression ::= cases-exp
          | has-type-exp
          | has-type-trusted-exp
          | arrow-exp
          | forall-exp
          | a standard Scheme <expression> from [R5RS]

The details of this syntax are explained in the following subsections.

3.1.1 Cases Expressions

The cases-exp is part of the define-datatype mechanism found in the second edition of Essentials of Programming Languages [Friedman-Wand-Haynes01]. The syntax for a cases-exp, adapted from [Friedman-Wand-Haynes01] (p. 47), is given below. The notation { field-name }* means zero or more repetitions of the nonterminal field-name.

cases-exp ::= ( cases type-name expression
                    { cases-clause }+ )
       | ( cases type-name expression
           { cases-clause }*
           ( else sequence ) )
type-name ::= identifier
cases-clause ::= ( variant-name ( { field-name }* ) sequence )
variant-name ::= identifier
field-name ::= identifier
sequence ::= 0 or more <command>s followed by an expression [R5RS]

For example, suppose we have the following definition (see section 3.2.2 Define-Datatype Definitions).

   (define-datatype course course?
       (regular (professor string?) (subject string?) (catnum number?))
       (seminar (leader string?) (subject string?)))

Then the following procedures, which uses a cases-exp, can extract the subject of a course.

   (define course->subject
      (lambda (c)
        (cases course c
          (regular (professor subject catnum) subject)
          (seminar (leader subject) subject))))

3.1.2 Has-Type Expressions

The syntax of a has-type-exp is as follows.

has-type-exp ::= ( has-type type-exp expression )

A has-type-exp is used to write a type into an expression. The type checker checks that the expression in the body of has-type has the type given, and the run-time value of the whole expression is the value of the body. For example, (has-type number 3) type checks because 3 has type number; the value of (has-type number 3) is 3.

A has-type-exp is especially useful with Scheme's let and letrec expressions, because it allows one to declare the type of a procedure in places where a deftype (see section 3.2.1 Deftype) is not permitted. An example is the following.

   (define fact
     (lambda (n)
       (letrec
          ((fact-iter
             (has-type (-> (number number) number)
                       (lambda (n acc)
                          (if (zero? n)
                               acc
                               (fact-iter (- n 1) (* n acc)))))))
          (fact-iter n 1))))

Another use of a has-type-exp is to force the type checker to use datum (see section 2.1.1 Datum) in a type. For example, one might write:

   (cons (has-type datum 1) '())

which will force the type checker to infer the type (list-of datum) for this expression, instead of (list-of number).

3.1.3 Trusted Has-Type Expressions

The syntax of a has-type-trusted-exp is as follows.

has-type-trusted-exp ::= ( has-type-trusted type-exp expression )

The meaning of a has-type-trusted-exp is just like a has-type expression (see section 3.1.2 Has-Type Expressions), but it is type checked differently. The type checker does not perform type checking on the expression, but simply accepts the given type. This allows one to suppress error reports when the code is correct but the type checker cannot prove it. For example, the current type checker does not take the flow of control into account; thus when a dynamic test is made to determine the type of a value using a type predicate, the type checker does not use this information. The type checker complains that the following code is not correct,

   (let ((input (read)))
     (if (number? input)
         (* 3 input)
         (error "please enter a number)))

because input, it says, is not a number. However, this error message can be avoided by use of has-type-trusted as follows.

   (let ((input (read)))
     (if (number? input)
         (* 3 (has-type-trusted number input))
         (error "please enter a number)))

However, has-type-trusted should be used sparingly, because one can suppress real errors with it. For example, the use of has-type-trusted in the following suppresses a real, but subtle type error, which will now occur at run-time when the procedure is called.

   (define add-to-list
      (lambda (num ls)
         (if (null? ls)
             '()
             (cons (+ num (car ls))
                   (has-type-trusted
                     (list-of number)
                     (add-to-list (cdr ls))))))) ; wrong!

(In the example above, the recursive call on the last line doesn't pass the right number of arguments, since it leaves out the argument num.)

3.1.4 Arrow Expressions

The syntax of an arrow-exp is as follows.

arrow-exp ::= ( -> ( { expression }* ) expression )
          | ( -> ( { expression }* expression ... ) expression )

An arrow-exp is used to construct a type predicate that corresponds to a procedure type (see section 2.3 Procedure Types). The meaning of an <arrow-exp> is the type predicate procedure?, except that the type checker can use the type predicates to construct more specific procedure types. For example, the following expression

   (-> (boolean? number?) boolean?)

has type

   (type-predicate-for (-> (boolean number) boolean))

That is, the expression corresponds to the type (-> (boolean number) boolean) (see section 2.7 Type Predicate Types). This is more specific than the type (-> (datum ...) datum) which the type checker thinks corresponds to the type predicate procedure?. (Note that the type of procedure? itself is not the issue, the issue is what type corresponds to an object that satisfies the predicate procedure?. See section 2. Notation for Type Expressions for a table of such correspondences.)

Since an arrow-exp is a type predicate, such an expression can be used as one of the subexpressions of an arrow-exp. For example, the following expression

   (-> ((-> (number? number?) number?) (list-of number?)) number?)

corresponds to the following type.

   (-> ((-> (number number) number) (list-of number)) number)

3.1.5 Forall Expressions

The syntax of a forall-exp is as follows.

forall-exp ::= ( forall formals expression )
formals ::= <formals> in the Scheme syntax [R5RS]

A forall-exp is used instead of a lambda to write type predicates transformers that correspond to polymorphic types (see section 2.4 Polymorphic Types). A type predicate transformer is a procedure that takes type predicates as arguments and returns a type predicate as its result.

Each standard formal T in the list of formals has type (type-predicate-for T). The expression that forms the body of the forall expression must have a type that matches (type-predicate-for S), for some type S. (Usually, S will depend on T.)

For example, we could write the type predicate transformer double-list-of as follows.

   (define double-list-of
     (forall (T?)
       (list-of (list-of T?))))

From this, the type checker will deduce that the type of list-of is the following.

   (forall (T) (-> ((type-predicate-for T))
                   (type-predicate-for (list-of (list-of T)))))

The forall that appears in the type also causes the overall type to be polymorphic, using a forall in the type (see section 2.4 Polymorphic Types). This explains the name of the expression.

In execution, a forall-exp of the form (forall formals exp) is equivalent to (lambda formals exp). The reason to not use the equivalent lambda is to tell the the type checker that one is defining a type predicate transformer for a polymorphic type, as described above.

Note, however, that a type predicate transformer is not itself a type predicate; it is a procedure that returns a type predicate when given type predicates as arguments. Hence, one cannot, for example, use a forall-exp as a type predicate in a define-datatype declaration (see section 3.2.2 Define-Datatype Definitions). For example, the following will cause a run-time error when used:

   (define-datatype poly-set poly-set?
      (empty)
      (comprehension
        (predicate (forall (T?) (-> (T?) boolean?)))))  ; wrong!

The problem will surface when trying to build an object of this type using the comprehension constructor. For example, the following will cause a run-time error.

   (cases poly-set (comprehension null?)
     (empty #f)
     (comprehension (predicate) (predicate '())))

One way to make this example work is to use the following instead.

   (define-datatype poly-set poly-set?
      (empty)
      (comprehension
        (predicate (-> (datum?) boolean?))))

3.2 Definitions Added To Scheme

The type checker adds the following kinds of definitions to Scheme. These are explained in the subsections below.

definition ::= deftype
          | define-datatype
          | a standard Scheme <definition> from [R5RS]

These are explained below.

3.2.1 Deftype

The syntax of a deftype is given below. See section 2. Notation for Type Expressions for the syntax of type-exp.

deftype ::= ( deftype name type-exp )
name ::= identifier

A deftype is used to define the type of a name. It can be used anywhere a Scheme definition can be used. The type checker will issue an error message if the type inferred for the name does not match the type given.

For example, one might write the following to define the type of the procedure remove-first.

   (deftype remove-first (forall (T) (-> (T (list-of T)) (list-of T))))

One can also use a deftype to define the type of a variable that is not a procedure. For example, the following declares that e has type number.

   (deftype e number)

3.2.2 Define-Datatype Definitions

The define-datatype definition form is found in the second edition of Essentials of Programming Languages [Friedman-Wand-Haynes01]. The syntax for a define-datatype, adapted from page 44 is given below. The notation { X }* means zero or more repetitions of X, and { X }+ means one or more repetitions of X. Recall that a type-name, variant-name, and field-name are each Scheme symbols (see section 3.1.1 Cases Expressions).

define-datatype ::= ( define-datatype type-name type-predicate-name
                          { ( variant-name { field-pred-binding }* ) }+ )
field-pred-binding ::= ( field-name predicate-exp )
type-predicate-name ::= identifier
predicate-exp ::= expression

The type checker can only deal with predicate-exps that have a type of the form (type-predicate-for S) for some type S. See section 2.7 Type Predicate Types for an explanation of these types. All of the standard type predicates, such as number?, symbol?, and several that we supply with the type checker, such as datum?, have such types. Another way to produce such a type is to apply a type predicate transformer, such as list-of, vector-of, pair-of, or -> to known type predicates. Thus the following are all predicate-exps that can be understood by the type checker; they are listed with their corresponding types.

          Built-in type predicates and corresponding types

   Type predicate                    Corresponding type expression
   -------------------------------------------------------------
   boolean?                          boolean
   number?                           number
   datum?                            datum
   (list-of string?)                 (list-of string)
   (list-of (list-of string?))       (list-of (list-of string))
   (vector-of number?)               (vector-of number)
   (pair-of char? char?)             (pair-of char char)
   (-> (char?) char?)                (-> (char) char)
   (-> (char? ...) char?)            (-> (char ...) char)

However, an expression such as (if #t number? boolean?) does not have such a type. The type checker rejects such predicate expressions, because it does not know how to extract the corresponding type information from them. When this happens, one can fall back to using a type predicate such as datum?.

A define-datatype declaration declares a variant record type, a new known type predicate, and the types of the procedures for constructing the variants. It also provides information needed to type check a cases-exp (see section 3.1.1 Cases Expressions) that is used with that type.

For example, the following definition

   (define-datatype person person?
      (student (name string?) (major string?))
      (professor (name string?) (office number?)))

has the effect of the following deftype definitions.

   (deftype person? (type-predicate-for person))
   (deftype student (-> (string string) person))
   (deftype professor (-> (string number) person))
   (deftype person
      (variant-record
        (student (name string) (major string))
        (professor (name string) (office number))))

For example, the following expressions are both of type person

  (student "Alyssa P. Hacker" "Computing")
  (professor "Daniel P. Friedman" 3021)

In addition, the following expressions will both return #t.

   (person? (student "Mitchell Wand" "Computer Science"))
   (person? (professor "Christopher T. Haynes" 3033))

Furthermore, the following expression will return "Hal Abelson" (see section 3.1.1 Cases Expressions).

   (let ((mit-prof (professor "Hal Abelson" 507)))
     (cases person mit-prof
        (professor (name salary) name))
        (student (name major) name))

Finally, in this example person becomes a known type, and person? a known type predicate, which can thus be used in making other simple type predicates.

3.3 Top-level Forms Added To Scheme

The type checker adds the following top-level forms to Scheme. These are explained in the subsections below.

command or definition ::= defrep
          | public
          | a standard Scheme <command or definition> from [R5RS]

3.3.1 Defrep

The syntax of a defrep is as follows.

defrep ::= ( defrep abstract-type-exp representation-type-exp )
abstract-type-exp ::= type-exp
representation-type-exp ::= type-exp

A defrep form is used to declare the correspondence between an abstract data type (ADT) and its concrete representation type [Liskov-Guttag86] [Jenkins-Leavens96]. Because a defrep form is syntactically a command or definition, i.e., a top-level form, it can only appear in certain places inside a program. These are the top-level of a Scheme program and within a top-level begin form (see the formal syntax appendix of [R5RS]).

The abstract type in a defrep form should be a basic type or an applied type. If a basic type is used, it cannot be a type variable.

For example, the defrep form in the following example, which would be found in a file `ratl.scm', says that the ADT ratl is represented by the type (list-of number). The deftype declarations present the client's view of the ADT's operations.

   ;;; file ratl.scm

   (defrep ratl (list-of number))

   (deftype make-ratl (-> (number number) ratl))
   (deftype numr (-> (ratl) number))
   (deftype denr (-> (ratl) number))

   ;;; the following is from p. 91 of [Springer-Friedman89]

   (define make-ratl
     (lambda (int1 int2)
       (if (zero? int2)
           (error "make-ratl: The denominator cannot be zero.")
           (list int1 int2))))

   (define numr
     (lambda (rtl)
       (car rtl)))

   (define denr
     (lambda (rtl)
       (cadr rtl)))

Without the defrep form, the type checker would infer that the type of the procedure make-ratl is as follows,

   (-> (number number) (list-of number))

which would not match the type declared with the deftype in the above example.

   (-> (number number) ratl)

However, with the defrep form, the type checker matches the inferred type of the procedure against a concrete version of the declared type. This concrete version is formed by substituting the representation type for each occurrence of the abstract type. Thus the concrete version of the declared type (-> (number number) ratl) is (-> (number number) (list-of number)), and so the inferred type and this concrete version of the declared type match.

When using the defrep form, one must also provide suitable deftype declarations (see section 3.2.1 Deftype) for the operations of the ADT, or the defrep form will have no effect.

In summary, the type checker uses a defrep form to check the concrete types of an ADT implementation against the client-visible types declared using deftype.

3.3.2 Public

public ::= ( public { identifier }* )

A public form allows one to declare which names declared in a file are visible (exported) to clients. Because a public form is syntactically a command or definition, i.e., a top-level form, it can only appear at the top-level of a Scheme program and within a top-level begin form (see the formal syntax appendix of [R5RS]).

If a Scheme file (and its associated `.def' file) contains no public forms, then all names defined in that file are exported to clients, and thus none are hidden. For example, in the file `ratl.scm' above (see section 3.3.1 Defrep), there is no public form, so all the names defined there are exported to clients. For that example, it would be equivalent to write the following.

   (public make-ratl numr denr)

If a Scheme file (and its associated `.def' file) have some public forms, then only the names listed are exported to clients, and all other definitions in the file are hidden. This would be used, for example, to hide helping procedures that clients should not need to know about.

3.4 Trusted Scheme Programs

A Scheme program file may optionally start with trustme!. (See the syntax appendix of the Revised(5) Report on Scheme [R5RS] for the syntax of command or definition.)

program ::= [ trustme! ] { command or definition }*

The trustme! directive can only be used at the top-level of a Scheme file or in a `.def' file (see section 1. Overview of the Type System). That is, it cannot be typed directly into the interpreter. Furthermore, if it appears at all in the file, it must be the first thing in the file that is not a Scheme comment.

The appearance of trustme! as the first thing in a file turns off all type checking for that file. Any deftype and grouped deftype declarations (see section 3.2 Definitions Added To Scheme) are accepted without comparing them to the types of their implementations. This is used to get around limitations of the type checker, and to make the type checker run faster. It should not be used by casual users.

Unless the speed advantages of trustme! are desired, a file with only a few problems for type checking should instead use the has-type-trusted expression described above (see section 3.1.3 Trusted Has-Type Expressions). This has the advantage of retaining some type checking by limiting the sections of the program where type checking is turned off.

4. Understanding Type Error Messages

(Not written yet.)

5. Type Checker Commands and Options

The following commands are helpful to regular users of the type checker.

  command                       effect
  ------------------------------------------------------------------
  (type-check-exit)             leave the typed interpreter loop
  (type-check-and-eval-loop)    starts (another) typed Scheme interpreter loop
  (type-check-reset-env!)       forget all names defined so far
  (type-help)                   displays helpful information (like this)

If you have exited the type checker's read-eval-print loop, you can use

  (type-check-and-eval-loop)

to restart it from Scheme.

The following commands are mainly useful for developing the type checker itself.

  command                       effect
  ------------------------------------------------------------------
  (type-tracing-set! N)         set tracing detail level to N
  (type-tracing-off!)           set tracing detail level to 0
  (type-tracing-level)          returns the numeric level of tracing detail

6. Future Work and Conclusions

The define-datatype facility doesn't support polymorphic variant record types. It seems necessary to have a separate declaration that would allow one to declare polymorphic variant record types, which produces a type predicate transformer instead of a type predicate.

One can also imagine trying to use more sophisticated type inference algorithms that can deal with some uses of nested polymorphic types.

6.1 Acknowledgments

Thanks to Steven Jenkins for work on an earlier version of the type checker and for discussions about these ideas. A more extensive (but dated) discussion of the type checker is found in [Jenkins-Leavens96].

The work of Leavens was supported in part by by the US NSF under grants CCR-9803843, CCR-0097907, and CCR-0113181. Some of the work on this document was done while Leavens was a visiting professor at the University of Iowa. Thanks to the students at the University of Iowa in 22C:54, section 2, during Fall 2000. Thanks to the students at Iowa State University in Com S 342 in several semesters, most recently Fall 2000.

A. Grammar Summary

The following is a summary of the context-free grammar for the type checker. In the grammar, the notation { X }* means zero or more repetitions of the nonterminal X. The notation { X }+ means one or more repetitions of the nonterminal X.

A.1 Notation for Type Expressions


type-exp ::= monomorphic-type
          | polymorphic-type
monomorphic-type ::= basic-type
          | applied-type
          | procedure-type
          | intersection-type
          | variant-record-type
          | type-predicate-type
basic-type ::= identifier
identifier ::= an <identifier> in the Scheme syntax [R5RS].
applied-type ::= ( identifier { type-exp }+ )
procedure-type ::= ( -> ( { type-exp }* ) type-exp )
          | ( -> ( { type-exp }* type-exp ... ) type-exp )
polymorphic-type ::= ( forall type-formals monomorphic-type )
type-formals ::= ( { type-variable }* )
type-variable ::= identifier
intersection-type ::= ( all-of { type-exp }+ )
variant-record-type ::= ( variant-record { variant }+ )
variant ::= ( identifier { field-type-binding }* )
field-type-binding ::= ( identifier type-exp )
type-predicate-type ::= ( type-predicate-for type-exp )

A.2 Additions to Scheme


expression ::= cases-exp
          | has-type-exp
          | has-type-trusted-exp
          | arrow-exp
          | forall-exp
          | a standard Scheme <expression> from [R5RS]
cases-exp ::= ( cases type-name expression
                    { cases-clause }+ )
       | ( cases type-name expression
type-name ::= identifier
cases-clause ::= ( variant-name ( { field-name }* ) sequence )
variant-name ::= identifier
field-name ::= identifier
sequence ::= 0 or more <command>s followed by an expression [R5RS]
has-type-exp ::= ( has-type type-exp expression )
has-type-trusted-exp ::= ( has-type-trusted type-exp expression )
arrow-exp ::= ( -> ( { expression }* ) expression )
          | ( -> ( { expression }* expression ... ) expression )
forall-exp ::= ( forall formals expression )
formals ::= <formals> in the Scheme syntax [R5RS]
definition ::= deftype
          | define-datatype
          | a standard Scheme <definition> from [R5RS]
deftype ::= ( deftype name type-exp )
name ::= identifier
define-datatype ::= ( define-datatype type-name type-predicate-name
                          { ( variant-name { field-pred-binding }* ) }+ )
field-pred-binding ::= ( field-name predicate-exp )
type-predicate-name ::= identifier
predicate-exp ::= expression
command or definition ::= defrep
          | public
          | a standard Scheme <command or definition> from [R5RS]
defrep ::= ( defrep abstract-type-exp representation-type-exp )
abstract-type-exp ::= type-exp
representation-type-exp ::= type-exp
public ::= ( public { identifier }* )
program ::= [ trustme! ] { command or definition }*

Bibliography

[Friedman-Wand-Haynes01]
Daniel P. Friedman and Mitchell Wand and Christopher T. Haynes. Essentials of Programming Languages, Second Edition, McGraw-Hill, 2001.
[Jenkins-Leavens96]
Steven Jenkins and Gary T. Leavens. Polymorphic Type-Checking in Scheme. Computer Languages, 22(4):215-223, 1996. Also available from
`ftp://ftp.cs.iastate.edu/pub/techreports/TR95-21/TR.ps.Z'.
[Liskov-Guttag86]
Barbara Liskov and John Guttag. Abstraction and Specification in Program Development, McGraw-Hill, 1986.
[Milner78]
Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3):348-375, December 1978.
[R5RS]
Richard Kelsey, William Clinger, and Jonathan Rees (editors). Revised(5) Report on the Algorithmic Language Scheme. February 1998. Available from
`http://www.schemers.org/Documents/Standards/'.
[Springer-Friedman89]
George Springer and Daniel P. Friedman. Scheme and the Art of Programming, McGraw-Hill, N.Y., 1989.


This document was generated on 9 October 2001 using texi2html 1.56k.