Publication details

Saarland University Computer Science

A Semantics For Lazy Types

Georg Neis

Bachelor's Thesis, September 2006

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.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009