Programming with Dependently Typed Data Structures ∗
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...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| 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 |
| Summary: | 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 |
|---|