Xanadu: Imperative Programming with Dependent Types

( Hindi ) ( Portuegese ) ( Romanian ) ( Spanish )

Principal Investigator Hongwei Xi
Students Chiyan Chen (Graduate), Sa Cui (Graduate), Likai Liu (Undergraduate), Rui Shi (Graduate), Dengping Zhu (Graduate)
Support NSF CCR-0224244, 2000 - 2004
Keywords Dependent Types, imperative programming, Xanadu, DTAL

We propose to enrich practical imperative programming with a type discipline that allows for specification and inference of significantly more precise information on programs than those enforced in languages such as Java and Standard ML (SML).

The primary motivation for developing such a type discipline is to enable the programmer to express more program properties with types and then enforce these properties through type-checking. It is well-known that a type discipline such as the one enforced in Java or SML can effectively facilitate program error detection. Therefore, it can be expected that a stronger type discipline can help detect more program errors, leading to the production of more robust software.

In general, there are two directions for extending a Hindley-Milner style of type system such as the one in SML. One is to extend it so that more programs can be admitted as type-correct and the other is to extend it so that programs can be assigned more accurate types. We are primarily interested in the latter.

The notion of dependent types, which was largely invented for modeling programs with more accuracy, has been studied for at least three decades. However, the use of dependent types in practical programming has been rare if there is any, and this, we think, is mainly caused by some great difficulty in designing a practically useful type inference algorithm for a dependent type system. We have presented an approach to addressing the difficulty in the design of Dependent ML (DML), which extends ML with a notion of restricted form of dependent types. It is also demonstrated that dependent types in DML can facilitate array bound check elimination, redundant pattern matching clause removal, tag check elimination and tagless representation of datatypes. Evidently, an immediate question is whether we can reap some similar benefits by incorporating dependent types into imperative programming. We propose to address this question by designing a dependently typed imperative programming language.

There is yet another motivation for incorporating dependent types into practical programming. In an untrusted computing environment such as Internet, mobile code received from an unknown source may not be trusted. Therefore, code recipient often needs to perform certain static and/or dynamic checks on received mobile code to prevent from happening some undesirable consequences such as security breach. We have designed a dependently typed assembly language (DTAL) in which the type system can guarantee the memory safety of DTAL code, where memory safety consists of both type safety and safe array subscripting. It is, however, difficult to compile into DTAL code a program written in a language such as Java since it often seems ineffective to synthesize from such a program the type information needed in DTAL code. With a dependently typed imperative programming language, we expect to implement a compiler that can translate dependent types at source level into dependent types at assembly level, effectively producing DTAL code.

In short, we propose to design a dependently typed imperative programming language for studying the use of dependent types in practical imperative programming at both source level and assembly level. We expect this study can eventually lead to the production of software that is not only more robust but also less costly to maintain.

  • What is Xanadu?

    Xanadu is a dependently typed imperative programming language. Here is a brief introduction (ppt).

  • Program Examples in Xanadu:

    We present some realistic examples in Xanadu in support of the practicality of Xanadu.

  • Papers on or related to Xanadu

  • Slides

    A talk on Xanadu can be found here

  • Implementation

    An undocumented prototype implementation of Xanadu can be found here. Keep tuned.

  • Hongwei Xi
    Last modified: Tue Feb 6 16:18:29 EST 2001