Seminars on Dependent Types in Practical Programming Seminars/Workshops

Abstract

1. Dependent Types in Practical Programming

We study practical methods for enriching the type system of the functional programming language ML with dependent types. We present an approach to enriching the type system of ML with a special form of dependent types where type index objects are restricted to some constraint domains C, leading to the DML(C) language schema. This aims at providing for specification and inference with significantly more precise type information compared with the current type system of ML, facilitating program error detection at compile-time and compiler optimization. We show that type-checking a sufficiently annotated program in our language can be reduced to constraint satisfaction. We exhibit the unobtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. We demonstrate both current and potential applications of our approach, such as facilitating program error detection, eliminating run-time array bound checks, and dependent type directed partial evaluation. We claim that dependent types can help to produce programs which are not only safer but also more efficient.

Security concerns with mobile code have raised many challenging questions in compiler optimization. A significant example is that array bound checks must be performed at run-time to enforce the memory safety of mobile code. This practice can become prohibitively expensive in cases such as numerical computation. In particular, it can be readily observed that Java applets often incur a vast number of run-time array bound checks when performing tasks related to graphics.

In this talk, we present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types. With such a type system, the memory safety property of mobile code can be captured with types and thus verified through type-checking before execution. This enables us to eliminate array bound checks in mobile code statically, leading to both safer and faster execution. We intend to use this assembly language as a target language for compiling high-level source languages with dependent type annotations.