The monadic continuity principle
Venanzio Capretta
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