CS217 Day 24 Monday, May 22, 2000

Types, Type Checking

A language is latently or dynamically typed if it is possible to determine the type of a value at runtime.
Scheme is latently typed -- every value has a tag which indicates its type, and there are predicates for recognizing each type (number?, symbol?, string?, vector?, null?, pair?, boolean?, procedure?).
A language is statically typed if it is possible to determine the type of each expression from the text of the program. Each variable and procedure is explicitly typed, or it is possible to infer their types.
In a a strongly statically typed language, a type checker can determine whether there is an attempt in a program to
- apply a non-procedure.
- apply a procedure to the wrong number of arguments,
- apply a procedure to an argument of the wrong type,
- use a non-boolean as the test in a conditional.
Java is strongly statically typed. Compilation errors are reported if there are any type errors.

Static type checking

We will associate a type expression with each expression.

The type of an integer is int.
The type of a boolean is bool.
The type of a procedure with parameter t1 and value of type t is
```
(t1 -> t)
```
The type of a procedure with parameters t1, t2,... and value of type t is
```
((t1 * t2 * ...) -> t)
```

Examples (in DL)

Type                       Expression
(int -> bool)                 zero?
(int -> int)                  add1
((int * int) -> int)          +
(int -> (int -> int)          proc (x) proc (y) +(x, y)
((int -> int) * int -> bool   proc (f, x) zero?((f add1(x)))

We introduce type expressions

[type-exp] ::= int
[type-exp] ::= bool
[type-exp] ::= ( -> [type-exp])
             | ([type-exp] {* [type-exp]}* -> [type-exp])

with abstract syntax

int-type-exp ()
bool-type-exp ()
proc-type-exp (argument-type-exps result-type-exp)

And we modify our grammar with concrete syntax (to obtain STDK?)

[expression] ::= proc () [expression]
               | proc ([type-exp] [id] {, [type-exp] [id]}*) [expression]

               | letrec
                   {[type-exp] [id] ({[type-id] [id]}*(,))
                      = [expression]}*
                 in [expression]

               | true
               | false

with abstract syntax

proc-exp (argument-type-exps ids body)

letrec-exp
  (result-type-exps proc-names
   argument-type-expss idss bodies
   letrec-body)

true-exp
false-exp

Example programs with this syntax:

proc (int x) add1(x)

letrec
  int fact (int x) = if zero(x) then 1 else *(x, (fact sub1(x)))
in fact

proc ((int -> bool) p, int x) (p x)

proc (int x) proc (int y) +(x, y)

proc ((int -> int) f, int x) zero?((f add1(x)))

We can type any expression in a type environment -- an environment in which each variable is bound to its type -- with the following rules. ([[exp]] denotes abstract syntax.)

Type rules for integer, boolean values:
```
(type-of-expression [[b]] tenv) = bool
(type-of-expression [[id]] tenv) = (apply-env tenv id)
```
If the equations above the line hold, then the equation below the line holds.

Type rule for applications:

(type-of-expression [[rator]] tenv) = (t1 * t2 * ... * tn) -> t
(type-of-expression [[rand1]] tenv) = t1
(type-of-expression [[rand2]] tenv) = t2
...
(type-of-expression [[randn]] tenv) = tn
----------------------------------------------------------------
(type-of-expression [[(rator rand1 rand2 ... randn)]] tenv) = t

Type rule for if:

(type-of-expression [[test-exp]] tenv) = bool
(type-of-expression [[true-exp]] tenv) = t
(type-of-expression [[false-exp]] tenv) = t
----------------------------------------------------------------
(type-of-expression 
  [[if test-exp then true-exp else false-exp]] tenv) = t

Type rule for procedures: (Recall notation for extended envs)

(type-of-expression [[exp]] [x1 = t1,..., xn = tn]tenv) = t
----------------------------------------------------------------
(type-of-expression [[proc (x1,..., xn) exp]] tenv)
   = (t1 * t2 * ... * tn) -> t

A type data type is introduced for analysis-time representation of types. There are two kinds of types, atomic and procedure.

Type expressions are converted to types by expand-type-expression.

(define-datatype type type?
  (atomic-type
    (name symbol?))
  (proc-type
    (arg-types (list-of type?))
    (result-type   type?)))

(define expand-type-expression
  (lambda (texp)
    (cases type-exp texp
      (int-type-exp () int-type)
      (bool-type-exp () bool-type)
      (proc-type-exp (arg-texps result-texp)
        (proc-type
          (expand-type-expressions arg-texps)
          (expand-type-expression  result-texp))))))

(define expand-type-expressions
  (lambda (texps)
    (map expand-type-expression texps)))

The primitive types:

(define int-type (atomic-type 'int))
(define bool-type (atomic-type 'bool))

(define type-of-primitive
  (lambda (prim)
    (cases primitive prim
      (add-prim  ()     (proc-type (list int-type int-type) int-type))
      (subtract-prim () (proc-type (list int-type int-type) int-type))
      (mult-prim  ()    (proc-type (list int-type int-type) int-type))
      (incr-prim  ()    (proc-type (list int-type) int-type))
      (decr-prim  ()    (proc-type (list int-type) int-type))
      (zero-test-prim () (proc-type (list int-type) bool-type)))))

Type environments.

(define-datatype type-environment type-environment?
  (empty-tenv-record)
  (extended-tenv-record
    (syms (list-of symbol?))
    (vals (list-of type?))
    (tenv type-environment?)))

(define empty-tenv empty-tenv-record)
(define extend-tenv extended-tenv-record)

(define apply-tenv 
  (lambda (tenv sym)
    (cases type-environment tenv
      (empty-tenv-record ()
        (eopl:error 'apply-tenv "unbound variable ~s" sym))
      (extended-tenv-record (syms vals env)
        (let ((position (list-find-position sym syms)))
          (if (number? position)
            (list-ref vals position)
            (apply-tenv env sym)))))))

type-of-expression has abstract syntax and type environmen parameters, and returns a type expression or signals an error. type-to-external-form converts a type expression to external form.

(define type-to-external-form
  (lambda (ty)
    (cases type ty
      (atomic-type (name) name)
      (proc-type (arg-types result-type)
        (append
          (arg-types-to-external-form arg-types)
          '(->)
          (list (type-to-external-form result-type)))))))

(define arg-types-to-external-form
  (lambda (types)
    (if (null? types)
      '()
      (if (null? (cdr types))
        (list (type-to-external-form (car types)))
        (cons
          (type-to-external-form (car types))
          (cons '*
                (arg-types-to-external-form (cdr types))))))))

Interface to the type checker in 7.2.scm.

(define type-check
  (lambda (string)
    (type-to-external-form
      (type-of-program
        (scan&parse string)))))

(define run
  (lambda (string)
    (eval-program (scan&parse string))))

(define run-all
  (lambda () 
    (run-list all-tests)))

(define check-all
  (lambda ()
    (check-list all-tests)))

The type checker (from 7.2.scm)

(define type-of-program
  (lambda (pgm)
    (cases program pgm
      (a-program (exp) (type-of-expression exp (empty-tenv))))))

(define type-of-expression
  (lambda (exp tenv)
    (cases expression exp
      (lit-exp (number) int-type)
      (true-exp () bool-type)
      (false-exp () bool-type)
      (var-exp (id) (apply-tenv tenv id))
      (if-exp (test-exp true-exp false-exp)
        (let ((test-type (type-of-expression test-exp tenv))
              (true-type (type-of-expression true-exp tenv))
              (false-type (type-of-expression false-exp tenv)))
          ;; these tests either succeed or raise an error
          (check-equal-type! test-type bool-type test-exp)
          (check-equal-type! true-type false-type exp)
          true-type))
      (proc-exp (texps ids body)
        (type-of-proc-exp texps ids body tenv))
      (primapp-exp (prim rands)
        (type-of-application
          (type-of-primitive prim)
          (types-of-expressions rands tenv)
          prim rands exp))
      (app-exp (rator rands) 
        (type-of-application
          (type-of-expression rator tenv)
          (types-of-expressions rands tenv)
          rator rands exp))
      (let-exp (ids rands body) (type-of-let-exp ids rands body tenv))
      (letrec-exp (result-texps proc-names texpss idss bodies
                    letrec-body)
        (type-of-letrec-exp
          result-texps proc-names texpss idss bodies
          letrec-body tenv))))) 

(define check-equal-type!
  (lambda (t1 t2 exp)
    (or (equal? t1 t2) 
      (eopl:error 'type-of-expression "types didn't match: ~s != ~s in~%~s"
        (type-to-external-form t1)
        (type-to-external-form t2)
        exp))))

(define type-of-proc-exp
  (lambda (texps ids body tenv)
    (let ((arg-types (expand-type-expressions texps)))
      (let ((result-type
              (type-of-expression body
                (extend-tenv ids arg-types tenv))))
        (proc-type arg-types result-type)))))

(define type-of-application
  (lambda (rator-type rand-types rator rands exp)
    (cases type rator-type
      (proc-type (arg-types result-type)
        (if (= (length arg-types) (length rand-types))
          (begin 
            (for-each
              (lambda (arg-type rator-type rand)
                (check-equal-type! rator-type arg-type rand))
              arg-types rand-types rands)
            result-type)
          (eopl:error 'type-of-expression
            "wrong number of arguments in expression ~s:~%expected ~s~%got ~s"
            exp
            (map type-to-external-form arg-types)
            (map type-to-external-form rand-types))))
      (else
        (eopl:error 'type-of-expression
          "rator not a proc type:~%~s~%had rator type ~s"   
          rator (type-to-external-form rator-type))))))

(define types-of-expressions
  (lambda (rands tenv)
    (map
      (lambda (exp) (type-of-expression exp tenv))
      rands)))

(define type-of-let-exp
  (lambda (ids rands body tenv)
    (let ((new-tenv
            (extend-tenv
              ids
              (types-of-expressions rands tenv)
              tenv)))
      (type-of-expression body new-tenv))))
          
(define type-of-letrec-exp
  (lambda (result-texps proc-names texpss idss bodies
            letrec-body tenv) 
    (let ((arg-typess
            (map
              (lambda (texps) (expand-type-expressions texps))
              texpss))
          (result-types (expand-type-expressions result-texps)))
      (let ((the-proc-types (map proc-type arg-typess result-types)))
        (let ((tenv-for-body            ; type env for all proc-bodies
                (extend-tenv proc-names the-proc-types tenv)))
          (for-each                     
            (lambda (ids arg-types body result-type)
              (check-equal-type!
                (type-of-expression 
                  body
                  (extend-tenv ids arg-types tenv-for-body))
                result-type
                body))
            idss arg-typess bodies result-types)
          (type-of-expression letrec-body tenv-for-body))))))

To use 7-2.scm, first load
Search for "add-test" to see the tests, with types and values.
(check-all) -- to check types
(run-all) -- to check values