Dynamic Typing with Dependent Types

Abstract:

Dependent type systems
allow programmers to specify
and enforce rich data invariants. Consequently, they
are important tools in global computing environments where
users must certify and check deep properties of
untrusted mobile programs.
Unfortunately, programmers who use these languages are
required to annotate their programs with
many typing specifications to help guide the type checker.
This paper shows how to make the
process of programming with dependent types more palatable
by defining a language in which programmers have
fine-grained control over the trade-off between the
number of dependent typing annotations they must place on programs
and the degree of compile-time safety. More specifically,
certain program fragments are marked dependent, in which case
the programmer annotates them in detail and a
dependent type checker verifies
them at compile time.
Other fragments are marked simple,
where programmers can just put simply-typed code
without any dependent annotations.
To ensure safety, the compiler automatically
inserts coercions when control passes in between
dependent and simple fragments.
These coercions are dynamic checks that make
sure dependent constraints are not violated by
the simply-typed fragment at run time.
The language semantics are defined
via a type-directed translation from a surface
language that mixes dependently and simply typed
code into an internal language that is completely dependently-typed.
In the internal language all dynamic checks on dependent constraints
are explicit. The translation always produces type-safe
internal language code and the internal language type system is sound.