Class 20: Introduction to Type Checking

Held Monday, October 14, 2002

Summary

Today we begin our consideration of a key semantic step: type checking. That is, we consider where and how one might verify types in a program.

Notes

• Are there questions on phase 2 of the project?
• For some reason, my notes on this topic have disappeared, so my outline is less robust than normal. Sorry.

Overview

• The problem of type checking
  • How it's used
  • Two issues: determining types and using types
• Examples from Pascal

An Introduction to Type Checking

• The problem of type checking is one of the first important semantic aspects of compilation. (What we've been doing so far is more syntactic.)
• Essentially, type checking
  • allows the programmer to limit what types may be used in certain circumstances;
  • assigns types to values ;
  • determines whether those values are used in an appropriate way.
• There are many variants of type checking. For example, if the type of an object is incorrect, you may coerce it to a different type.
• The definition of types is subtle; it's often worth asking when two values should be considered as having the same type.

When Should You Type Check?

• In many modern languages, type checking is done at compile time.
• In some, it's done at run time.
• What are some advantages for type checking at compile time?
  • Catches many common errors.
  • Can result in faster code.
  • ...
• What are some advantages for type checking at run time?
  • Frees the programmer.
  • Can result in more robust code.
  • Can result in clearer code.
  • ...
• Pascal type checking is traditionally done at compile time.

Common Types

• Built-in types (integers, floating-point numbers, strings, ...)
• Compound types (arrays, lists, records, classes)
• User-defined enumerated types.
• ...

Computing Types

• In Pascal, the types of variables are declared in advance.
• However, we still need to type other things (such as ...)
• We'll consider as a class what kinds of things should be typed and where we use types.