TP2 — Typing
Comes mainly from here.Thanks Antoine!
The goal of this session is to add types, and a static type analysis, to our language.
Language
Start by downloading the package.
The language is the same as last week.
A single declaration can declare an arbitrary number of variables var1, var2, etc.
Note that there is no static type information in declarations: the language is dynamically typed.
Each variable name is optionally followed by an initialization of the form = expr,
which behaves similarly to an assignment. If there is no initialization expression, the variable is
assumed to be non-initialized. Note that using a non-initialized value in an expression results in a
value error, but not a type error, and detecting the use of non initialized variables is thus out of
the scope of the type analysis we develop here.
A variable declared in a block starts existing at the point of declaration and stops existing at the end of the block; this is the variable scope. It is important to distinguish variables of the same name, in case several of them exist at the same time (in nested scopes). Scoping is already resolved in the base package.
The program is dynamically typed, à la Python: upon assignation, a variable takes the type of the value it is assigned. In our simple language, there are only boolean and integer values. There is a type error in case an integer value is used with a boolean operator, or the converse.
Type analysis
The goal of this exercise is to write a static analyzer that automatically discovers whether the program is type safe (no dynamic type error at execution). The analysis is similar to computing the denotational semantics of a non-deterministic language, but sets of values (integers, booleans, errors) are replaced with abstract values, i.e., types.
You have to implement only the typing environment domain. You can use the iterator of the concrete interpreter.
Extensions
Possible extensions and variants include:
- Polymorphic types. A polymorphic type system allows several types for programs. As our language has only a finite set of types, we can represent polymorphism by listing the set of possible types. Program a polymorphic type analyzer that propagate sets of type assignments instead of a single type assignment.
- Flow-insensitive types. A static type analysis allows the same variable to change its type throughout the execution of the program. Standard type systems are, however, flow-insensitive: a single type assignment should be valid at all program points. Program a flow-insensitive type analyzer that ensures this property and rejects programs requiring variables to change type.