A central requirement for open and distributed programming is the ability to
compose code at run time. In such programs type safety can no longer be
guaranteed by static checks. Additional type checking at link time is
necessary to ensure the integrity of the run-time system. Apart from that, it
is desirable to perform linking as late as possible: this decreases the
startup time of programs, keeps their working set small, and avoids loading
unneeded code.
In this thesis, we present a system that is based on $F_omega$ and models a
language with support for such type-safe, late dynamic linking in the presence
of higher-order polymorphism. Its key ingredients are intensional type
analysis and lazy evaluation. Interesting implications arise from this
combination. Type analysis needs to compare dynamic types, which have to be
computed from (probably higher-order) type expressions that may contain types
from other modules. If lazy linking has delayed the loading of these modules
so far, then the corresponding types are represented by free type variables.
For the type-level computation in our model this means that it may encounter
free type variables whose denotation depends on yet unevaluated term-level
expressions. To proceed, it inevitably has to eliminate these variables by
triggering the necessary evaluations on term-level. In other words: type-level
computation has to account for lazy types. We give two strategies for this and
show soundness properties for the resulting calculi. The second strategy is
more complicated than the first but provides a higher degree of laziness.