TP2 - Typage

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 (int, bool or error).

The language is the same as last week

  • Start by selecting the right TP number in analyzer.ml

Environment

Your goal is to complete the TypingEnv functor in environment.ml

  • Give a definition for the env type.

Hint: You may first want to define a type ty_value for type values and define the env type as a map from variables to type values. This ty_value should denote elements of the type lattice defined in the lecture.

  • Implement the other functions. Feel free to add utility functions.

Interpreter

If you didn’t have time to finish it last week, complete the MakeConcrete functor in interpreter.ml

Incompleteness

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

Extensions

If you have some time left, you could implement one of the following extensions:

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.