Functions (or closures) are the prototypical codata... a co-inductive codata can be presented as a function space from an inductive datatype into some other type. It has a coinduction principle, derived from the induction principle of the parameter type. Traditional imperative code can be represented through the use of a free monad over a functor representing some command language, and the free monad is a codata as well.