You may not have ever thought about why some programming languages seem to have types and others don't. In fact, you may think types are a nuisance or worse.
No matter what programming language you use, you have to worry about types. The only question is whether or not the language will help you. For example, this semester we've been using Scheme, which is untyped. Even so, you still can't execute (car 4). The programmer must worry about types even if the language doesn't. Using a type in a way that's not supported is a type error.
Untyped universes of computational objects decompose naturally into subsets with uniform behavior. Sets of objects with uniform behavior may be named and are referred to as types.
Throughout this course, we've consistently used the terms static and dynamic. Static properties are unchanging and can be determined from the code without actually running it. Dynamic properties depend on what happens when you run the code.
Static type checking is done at ``compile time'' (before you begin running the code). Static type checking has many desirable properties, most notably that any type errors that are flagged are flagged before you ever start running the code. Notice that this doesn't mean types are always used correctly! It only means that what checking is done is performed before you run the code.
Dynamic type checking is done at runtime. For certain situations, the type of an expression can't be determined just by looking at the code--you have to actually run it to see which logical paths are followed. This is especially true when you have variables that sometimes hold one type and sometimes hold another. In order to make dynamic type checking work, the interpreter has to tag every piece of data with a label that identifies its type. (Static type checking can avoid this--you determine the types at compile time and then forget about them when it comes time to run the code.)
Done well, type systems can avoid embarrassing questions about representations and forbid situations in which these questions may come up. A type system is strong if it only admits correctly typed expressions.
Strong typing is not synonymous with
Declaring types ahead of time or checking at compile time doesn't guarantee that type errors won't occur. They help, but they don't by themselves provide strong typing.
In fact, declaring variables types isn't even required at all. That's right--a language can be strongly typed without having to declare all of the types ahead of time. Some languages don't require you to declare types explicitly but instead infer types from how the variable is used. (Example: ML.) We'll talk more about type inference more in Lecture 30.
Strong typing significantly helps program development, but it doesn't guarantee that other errors aren't present. One way to think about types is as a necessary, although not sufficient, specification of correctness. That is, for the program to run correctly, the types must be correct, but that's not enough to ensure correctness. This concept of types presupposes a good typing system, of course, but that's how we'd like types to work.
There are two general strategies for enforcing types statically:
The type checking approach requires that you declare the types of basic components (variables, functions, etc.) ahead of time. From these basic elements, the system then determines the types of subexpressions built from these components. Think of this as labeling the leaves of the parse tree, then calculating the types of interior nodes (expressions built out of other expressions) using properties of the language and the types of the subtrees (subexpressions).
Type inference, as previously defined, doesn't require you to declare types. Instead, the system infers the types of things from how they are used. Unlike type checking, the AST must typically be traversed multiple times, working from the bottom up and from the top down propogating type information as it can be determined. This process is known as unification.
You're probably used to thinking of variables as just ints, floats, strings, aggregates of other types, etc., but you've probably never thought about functions as having types.
The C++ function
int f(int x, int y)can be thought of as having the following type:
(int * int -> int)
That is, it is a mapping from two integers (an element of the Cartesian product int * int) to an integer.
Using this function in any other way is a type error.
In the next lecture, we'll start talking about how to implement type checking in ELL.
Here are the slides from the in-class lecture.
Last updated at 9:54 am on Friday, August 27, 2004.