Brouwer's continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that is incompatible with classical mathematics. Recently Martín Escardό proved that it is also inconsistent in type theory. This shows that we cannot internalize the meta-theoretical observation that every definable function is continuous. However, we can adapt Brouwer's ideas to an important class of functions and propose a reformulation of the continuity principle that is internally provable. We note that Brouwer talked about functions on choice sequences, which are described as free progressions of values not necessarily generated by a rule. The functions must produce their results independently of how the sequences are generated. We formalize them as monadic streams, potentially unending sequences of values produced by steps triggered by a monadic action, possibly involving side effects. We consider functions on them that are uniform, in the sense that they operate in the same way independently of the particular monad that provides the specific side effects. Formally this is done by requiring a form of naturality in the monad. Functions on monadic streams have not only a foundational importance, but have also practical applications in signal processing and reactive programming. We give algorithms to determine the modulus of continuity of monadic stream functions and to generate dialogue trees for them (trees whose nodes and branches describe the interaction of the process with the environment).

A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.

Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination. In this work, we present a method to formalise general recursive algorithms in type theory. Given a general recursive algorithm, our method is to define an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm is then defined by structural recursion on the proof that the input values satisfy this predicate. The method separates the computational and logical parts of the definitions and thus the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Here, we give a formal definition of the method and discuss its power and its limitations.

Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.