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.