Return to search

The Essence of Codata and Its Implementations

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


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.
Date06 September 2018
CreatorsSullivan, Zachary
ContributorsAriola, Zena
PublisherUniversity of Oregon
Source SetsUniversity of Oregon
Detected LanguageEnglish
TypeElectronic Thesis or Dissertation
RightsAll Rights Reserved.

Page generated in 0.0029 seconds