Exploring Codata: The Relation to Object-Orientation
Zachary Sullivan
Committee: Zena Ariola (chair), Boyana Norris, Stephen Fickas
Directed Research Project(May 2019)
Keywords: Codata,Curry-Howard,Object-orientation

Functional languages are known to enjoy an elegant connection to logic: lambda-calculus corresponds to natural deduction. Unfortunately, the same cannot be said for object-oriented languages. Type systems have been designed to capture all the fancy features present in current object-oriented languages. We believe, however, that the logical foundation of object-orientation has not yet been fully explored. Our goal is to describe how objects arise naturally in logic.

The dual of data, known as codata, can be seen as an object. Whereas data is constructed, codata specifies all the possible ways to use it. Analogously to an object defining a pair, a codata pair gives two methods for accessing the first and second components.

To substantiate this approach we extend a basic language containing both data and codata with the essential object-oriented features of subtyping, classes, and inheritance. This suggests how the functional and object-oriented paradigms can embrace each other; the extended language also provides a suitable intermediate language for the compilation of the two programming paradigms.