7.0.0.6

13 Types and Type Checking

Goals

What are types and type systems?

Different ways of specifying the rules of a type system.

Deriving a type checking algorithm for a type system.

Implementing a type checker.

Here is a link to the morning lecture slides (also available in PDF).

Recall our running (untyped) example language:

  Definition = (define-function (Variable Variable ...)  Expression)
     
  Expression = (function-application Variable Expression ...)
  | (if Expression Expression Expression)
  | (+ Expression Expression)
  | Variable
  | Number
  | Boolean
  | String

We convert it to a typed language by:

  1. Adjusting our language to accommodate the types:

      Definition = (define-function (Variable [Variable : Type] ...)  : Type Expression)
         
      Expression = (function-application Expression Expression ...)
      | (λ ([x : Type] ...) Expression)
      | (if Expression Expression Expression)
      | (+ Expression Expression)
      | Variable
      | Number
      | Boolean
      | String

    To simplify implementation of a type checker, we have added a λ expression in addition to define-function.

  2. Coming up with a language of types. For example:
      Type = (-> Type ...)
      | Number
      | Boolean
      | String

  3. Developing type rules for our type system.

  4. Implementing a type checker for our type rules.