Loading...
Please wait, while we are loading the content...
Similar Documents
Leveling up dependent types: generic programming over a predicative hierarchy of universes
| Content Provider | ACM Digital Library |
|---|---|
| Author | Sheard, Tim Diehl, Larry |
| Abstract | Generic programming is about writing a single function that does something different for each type. In most languages one cannot case over the structure of types. So in such languages generic programming is accomplished by defining a universe, a data structure isomorphic to some subset of the types supported by the language, and performing a case analysis over this datatype instead. Such functions support a limitied level of genericity, limited to the subset of types that the universe encodes. The key to full genericity is defining a rich enough universe to encode all types in the language. In this paper we show how to define a universe with a predicative hierarchy of types, encoding a finite set of base types (including dependent products and sums), and an infinite set of user defined datatypes. We demonstrate that such a system supports a much broader notion of generic programming, along with a serendipitous extension to the usefulness of user defined datatypes with existential arguments. |
| Starting Page | 49 |
| Ending Page | 60 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781450323840 |
| DOI | 10.1145/2502409.2502414 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2013-09-24 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Dependent types Universes. Generic programming |
| Content Type | Text |
| Resource Type | Article |
