Codata can be seen as a data-producer on demand, i.e. a stream or a tree-like datastructure produced with lazy-evaluation, i.e. demand-driven programming. It can be used for modelling session-types, that are types related to a protocol.
Corecursion produce data (i.e. a function producing a stream), while recursion consume data.
Data is finite, codata is infinite.
An OOP API can produce codata. For example an iterator.
TODO check ifparadigm/algebraic-effects-handler can be used instead for demand-driven programming, walking in tree, and data on demand
Paper about codata
- Downen, Z. Sullivan, Z. M. Ariola, and S. Peyton Jones, “Codata in Action,” in Programming Languages and Systems, vol. 11423, L. Caires, Ed. Cham: Springer International Publishing, 2019, pp. 119–146. doi: 10.1007/978-3-030-17184-1_5.
Advocate for the explicit presence of codata types in a PL.
Demand-driven programming is con- sidered a virtue of lazy languages, but codata is a language-independent tool for capturing this programming idiom. Codata exactly captures the essence of pro- cedural abstraction, as achieved with λ-abstractions and objects, with a logically founded formalism . Specifying pre- and post-conditions of protocols, which is available in some object systems , is straightforward with indexed, recursive codata types, i.e. objects with guarded methods .
Specifying a codata type is giving an interface—between an implementation and a client—so that instances of the type (implementations) can respond to requests (clients). In fact, method calls are the only way to interact with our objects.
codata Set where IsEmpty : Set -> Bool Contains : Set → Int → Bool Insert : Set → Int → Set Union : Set → Set → Set