Author: Georg Neis
Time frame: April 2006 - September 2006
Advisor: Andreas Rossberg
Responsible Professor: Gert Smolka
Open and distributed programming has produced the need to compose programs dynamically, via some form of dynamic loading and linking. To maintain type safety, type-checking has to be performed at link-time. To keep active processes small, loading of additional components should only be performed when needed.
Formalising a language with support for such type-safe, late dynamic linking requires two key ingredients:
However, when both features are combined into a single system, interesting implications arise: type analysis needs to inspect dynamic types; these types have to be computed from (probably higher-order) type expressions that may contain free type variables; the denotation of those type variables in turn may depend on the value of term-level expressions. Since term-level computation may be lazy, type-level computation inevitably has to support laziness as well. That necessitates a new concept: lazy types.
This thesis shall develop a calculus that integrates type analysis with laziness, in the presence of higher-order polymorphism. It will be based on a call-by-value variant of the higher-order polymorphic-calculus (Fω).
The central task is to develop a precise operational semantics of type-level computations, which is usually left implicit in other calculi with higher-order type systems. This requires the choice of a suitable notion of normal form and an appropriate reduction strategy. Moreover, reduction must be extended to account for laziness. Laziness may require type and term-level reductions to interleave, so both reduction regimes must be integrated properly.
The choice of reduction strategy for types has a direct impact on the degree of laziness achievable for type-carrying terms, and should hence be motivated by analyzing possible application scenarios.
Standard soundness properties have to be shown for the calculus.