## The monadic continuity principle

School of Computer Science

University of Nottingham

Thursday, 26 March 2015, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: Brouwer's Continuity Principle states that all
functions are continuous: a function on infinite sequences of numbers
only depends on a finite initial segment of its input. The principle
is justified in computational mathematics: a terminating program will
produce an output after a finite number of steps; therefore it can
only read a finite number of inputs.

However, Martin Escardo proved that adding the continuity principle to
type theory is inconsistent. We think that the problem is caused by
intensionality: the paradox exploits the knowledge of the internal
definition of a stream (infinite sequence).

Brouwer talked about "choice sequences", in which every element is
produced freely, not by a fixed procedure. So no intensional
information should be available. In our opinion, the best way to
formalize this notion is by monadic streams, sequences that are
encased inside a monad. To obtain the head and tail of a stream, we
must execute a monadic action. The standard example is the IO monad in
Haskell: the program must interact with the system and user, with
potential side effects, to obtain the next element.

We formalize the notion of monadic streams and formulate the
continuity principle for functions on them polymorphic on the
monad. Proving that it holds is still elusive. We need to exploit a
form of parametricity, ie the assumption that the functions operate
uniformly on all monads; it works only for linear functions, that
evaluate the monadic action only ones.

However, work by Bauer, Hofmann and Kabyshev show that a simpler
formalization obtains continuity. In their case the input is not a
monadic stream, but a single monadic value that can be evaluated several
times to obtain the stream elements.

Joint work with Paolo
Capriotti.

Tarmo Uustalu

Last update 23 March 2015