Programming with Dependently Typed Data Structures ∗

• Main Author: Hongwei Xi
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Subjects: Haskell; DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.110.5578; http://www.cs.bu.edu/~hwxi/academic/papers/DTref.pdf

The mechanism for declaring datatypes in functional programming languages such as ML and Haskell is of great use in practice. This mechanism, however, often suffers from its imprecision in capturing various invariants inherent in data structures. The introduction of dependent datatypes in Dependent ML (DML) can partly remedy the situation, allowing the programmer to model data structures with significantly more accuracy. In this paper, we present several programming examples (e.g., implementations of random-access lists and red-black trees) to illustrate some practical use of dependent datatypes in capturing relatively sophisticated invariants in data structures. We claim that dependent datatypes can enable the programmer to implement algorithms in a manner that is more efficient, more robust and easier to understand. 1