13 Types and Type Checking

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

Recall our running (untyped) example language:

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.