Since last TP, some modifications have been made on the subject:
Thanks Loïc for noticing these mistakes !
The goal of this session is to implement a static type analysis to our language.
It should be able to detect if a program is type-safe (i.e. there is no dynamic type error at execution).
This analysis is similar to the computing the denotational semantic of the language, but the values are replaced by their types (
The language is the same as last week
Your goal is to complete the
Hint: You may first want to define a type
If you didn’t have time to finish it last week, complete the
Since your analysis is both automatic and sound (if your analysis conclude the program is type safe then it cannot raise a type error) and the absence of type errors is not decidable, your analysis is incomplete
Find an false-positive example showing that your analysis is incomplete, i.e. a program flagged as not type-safe though it does not raise a type error in the concrete semantic
If you have some time left, you could implement one of the following extensions:
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.
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.