CSC362 2004S, Class 25: Type Checking (1)

Admin:
* No train today?
* Cool convo tomorrow
* Talk by Mr. Walker today at 4:15 (extra credit)
* New written assignment 
* From today's Science Teaching and Learning Group (not from Sam): "I'd never *call out* a student in class, e.g., for missing the previous class."

Overview:
* An introduction to type checking
  * What is a type?
  * What is type checking?
  * Why type check?
  * Where should we type check?
* Compile-time vs. Run-time type checking
* Common types
  * What kinds of things have types?
  * What are types
  * Computing types

What is a type?
* Method-focused: A way of categorizing data (e.g., with interfaces in Java)
* Implementation-focused: A way of interpreting bits
* Data-focused: A set of values

E.g., what are integers?
* Numbers with only whole parts
* ints are a subset of integers from MININT to MAXINT
* ... -2, -1, 0, 1, 2, ...

Why do we type?
* We categorize data because categorization tells us how we can manipulate them (polymorphism in action)
* Typing allows us to catch programming errors (e.g., trying to use a real as an index for an array)
* Some kinds of type describe the underlying representation and the size of that representation (short vs. int vs. long)
* machines often have different instructions for different "basic" types

How do we define types?
* Listing the elements
* Implicitly: By defining legal operations
* By writing rules that define the type
  0 is a non-negative integer
  The successor of any non-negative integer is a non-negative integer
* Rely on built-in types (e.g., integers on most systems)
* Rely on mechanisms for combining existing types

As compiler writers, we should type check the programs we receive
* We need to do so to generate correct "machine" code
* We want to warn our programmers that they may be making mistakes
  (and perhaps refuse to compile)

What does it mean to "type check" a program?
* Make sure that operations are called on the proper type
	type
	  c: real;
	  a: array[1..10] of integer;
	...
	  a[c]
          c[2]
	sqrt("a")
* Keep track of the types "defined" for variables (and other things)
* Determine the types of expressions
	a[1] = c + 2;

There are different reactions to type "errors"
* You can report the error
* You can "coerce" one type into another
	long a;
	float b;

	a = b; // Not okay
	b = a; // Probably okay
  "Converting an integer to a float doesn't lose information; Converting a float to an integer almost certainly does."

In order to type check a program, you must:
* Traverse the program to build a "symbol table" that assigns types to names
* Traverse the program to assign types to expressions
* Check that every expression is used correctly

There are two times that type checking is normally done:
* At compile time
  * Catch errors earlier
  * Might get output that's incorrect
  * Code more likely to run faster (as it doesn't have to do run-time type checking)
* At run time
  * Might need to be much more "specific" in your coding
  * Supports polymorphism: You get the right "toString" when pritning objects 
  * Code generation can be faster
  * Can adapt the type "on the fly"
  * Spurious example
  Object foo;
  ...
  System.out.println(((Vector) foo).get(4));

One hard part of type checking: When are two types "compatible"?

	type
	  smallint = 1..10;
	var
  	  a: integer;
	  b: smallint;
	function foo(x: integer);
	...
	function bar(y: smallint);
	...
	foo(2);
	foo(a);
	foo(b);
Should we allow this?
Yes: 
  b is an integer, so why not use it like one (smallint is a subrange of integer)
No
  Types are intended to restrict usage; since we're using smallint not integer, we clearly mean it to be something else
	bar(a);

Related question: Do we check initialization?
* Can be done as part of typechecking.  In the most generally form, is as hard as the halting problem

	a: integer
	while (...)
          ...
        if (test-that-depends-on-the-result-of-the-while-loop)
          a = 5;
        foo(a);

Typechecking gets more fun when you deal with records and arrays
* Same names, different orders
* Different names, same types
* Etc.