Induction by Coinduction and Control Operators in Call-by-Name

TL;DR

This paper demonstrates how control operators in call-by-name languages enable the emulation of inductive types from coinductive types, overcoming limitations due to the absence of initial algebras.

Contribution

It introduces a method to derive certain inductive types from coinductive types using control operators in call-by-name languages.

Findings

Natural numbers can be represented by streams.

Control operators enable emulation of induction from coinduction.

Restricted inductive types are derivable from coinductive types with control.

Abstract

This paper studies emulation of induction by coinduction in a call-by-name language with control operators. Since it is known that call-by-name programming languages with control operators cannot have general initial algebras, interaction of induction and control operators is often restricted to effect-free functions. We show that some class of such restricted inductive types can be derived from full coinductive types by the power of control operators. As a typical example of our results, the type of natural numbers is represented by the type of streams. The underlying idea is a counterpart of the fact that some coinductive types can be expressed by inductive types in call-by-name pure language without side-effects.