Andreas
Rossberg
Max Planck
Institute for Software Systems
Typed
Open Programming -- A higher-order typed approach to dynamic modularity
Abstract:
Open programming
-- the
development of programs that support dynamic exchange of
higher-order
values and components -- is a domain currently dominated by
untyped or
weakly-typed
languages. I present an approach for reconciling open programming
with
ML-style
strong
static typing.
I give a brief overview over the design of a concrete programming
language,
Alice ML, that extends Standard ML with a set of
orthogonal features
like
higher-order modules, dynamic type checking, higher- order pickling,
and concurrency.
On top of these a flexible system of dynamic components and a
simple
but
expressive notion of distribution is realised. The central concept
in
this
design is the "package", a first-class value embedding a module along
with its signature, which is dynamically checked whenever the module is
extracted.
The
standard existential model of
type abstraction is invalidated by the presence of primitives for
dynamic type
analysis. To maintain abstraction safety, I hence develop a calculus
using
dynamic generation of type names and a novel notion of "abstraction
kinds" classifying abstract types. In order to recover ML-style
after-the- fact type abstraction and type translucency, I further show
how to extend
the system with higher-order coercions over types and (dependent) kinds.