Detail

Subtyping first class polymorphic components

We present a statically typed, class-based object-oriented core language where classes are first class polymorphic values.

In our language it is possible to manipulate (e.g., compose, parametrize, instantiate, extend) type-parametric classes (cf., C++ template classes) at runtime, in a statically verified type safe way.

A main contribution of this work is the design of a type system that combines first class polymorphic values with structural equirecursive types and admits a subtyping algorithm which is arguably much simpler than existing alternatives. The type inference system is decidable and possesses the minimal type property.

The talk will be given in a tutorial style, surveying the state of the art on related type systems.