Dynamic Typing with Dependent Types
Report ID: TR-695-04Author: Ou, Xinming / Walker, David / Mandelbaum, Yitzhak / Tan, Gang
Date: 2004-04-00
Pages: 26
Download Formats: |PDF|
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.