The Essence of Codata and Its Implementations
Loading...
Date
2018-09-06
Authors
Sullivan, Zachary
Journal Title
Journal ISSN
Volume Title
Publisher
University of Oregon
Abstract
Data types are a widely-used feature of functional programming languages that
allow programmers to create abstractions and control branching
computations. Instances of data types are introduced by applying one of a
disjoint set of constructors and are eliminated by pattern matching on the
constructor used. Dually, codata types are defined by their destructors, are
introduced by copattern matching on their context, and eliminated by applying
destructors.
We extend motivation for codata types to include adding types that satisfy the
extensional laws and adding an abstraction for constraining clients of code. We
also improve on work implementing codata by developing an untyped compilation
technique for codata that works for both call-by-name and call-by-value
evaluation strategies and scales to simple and indexed type systems. We
demonstrate the practicality of our technique by implementing a prototype
compiler and a Haskell language extension.
Description
Keywords
Codata, Compilation, Duality