Résumé de séminaire

Résumé :

Foundational type systems are guided by logic. One of the most popular is system F; it provides with universal polymorphism a flexible technique for composition, and it provides with abstract (or: existential) types a powerful means for encapsulation.

Object-oriented programming is guided by modelling systems. OOP also offers with subtyping a flexible technique for composition, and it offers with private members a somewhat weaker form of encapsulation.

Advanced object-oriented languages contain many concepts first studied in foundational type systems, even though they often use them in an ad-hoc and pragmatic way. On the other hand, pure foundational type systems have been applied to object-oriented programming but programs written in practice often require fairly heavy encodings.

This talk discusses a type system for object-oriented programming which attempts to be general and pragmatic at the same time. Its key element are nested type declarations, which can be either abstract or concrete. Abstract nested types may be overridden in subtypes of the containing types.

This idea provides a simple and general scheme to express many typing problems occurring in object and module systems. In particular, we show how we can model OO encapsulation such as class-private or package-private members. We also show how one can model self types and specialization of families of classes. The type system can express many aspects that were traditionally relegated to advanced module systems, in particular we show hwo one can express the analogue of SML's sharing constraints.