Indexed codata types
| Autor: | ThibodeauDavid, CaveAndrew, PientkaBrigitte |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
General-purpose programming language
Functional programming Computer science Programming language 020207 software engineering 0102 computer and information sciences 02 engineering and technology DUAL (cognitive architecture) computer.software_genre 01 natural sciences Computer Graphics and Computer-Aided Design Data type 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering computer Software |
| Zdroj: | ACM SIGPLAN Notices. 51:351-363 |
| ISSN: | 1558-1160 0362-1340 |
| DOI: | 10.1145/3022670.2951929 |
| Popis: | Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make. Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|