paradigm/codata

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

1. 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 [16]. Specifying pre- and post-conditions of protocols, which is available in some object systems [14], is straightforward with indexed, recursive codata types, i.e. objects with guarded methods [40].

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