We develop the Scott model of the programming language PCF in constructive predicative univalent type theory. To account for the non-termination in PCF, we work with the partial map classifier monad (also known as the lifting monad) from topos theory, which has been extended to constructive type theory by Knapp and Escardo. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or higher inductive-inductive types. We show that one can do without these extensions.
Partiality in type theory has been the subject of recent study. We briefly discuss the different approaches. First, there are Capretta's delay monad and its quotient by weak bisimilarity, which have been studied by Uustula, Chapman and Veltri @cite_1 . A drawback of the quotient is that some form of choice is needed (countable choice suffices) to show that it is again a monad. Another approach is laid out in @cite_3 by Altenkirch, Danielsson and Kraus. They construct (essentially by definition) the free @math -cpo with a least element using a higher inductive-inductive type. Moreover, show that, assuming countable choice, their free @math -cpo coincides with the quotiented delay monad. In @cite_2 , Knapp showed that, assuming countable choice, a restricted version (using a dominance) of the lifting is isomorphic to the quotiented delay monad.
@cite_1 @cite_3 @cite_2
2767001837 2963889233 2905240033
Capretta's delay monad can be used to model partial computations, but it has the wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right''notion of equality, weak bisimilarity. However, recent work by suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory---a higher inductive-inductive type---we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications. We investigate partial functions and computability theory from within a constructive, univalent type theory. The focus is on placing computability into a larger mathematical context, rather than on a complete development of computability theory. We begin with a treatment of partial functions, using the notion of dominance, which is used in synthetic domain theory to discuss classes of partial maps. We relate this and other ideas from synthetic domain theory to other approaches to partiality in type theory. We show that the notion of dominance is difficult to apply in our setting: the set of �0 1 propositions investigated by Rosolini form a dominance precisely if a weak, but nevertheless unprovable, choice principle holds. To get around this problem, we suggest an alternative notion of partial function we call disciplined maps. In the presence of countable choice, this notion coincides with Rosolini’s. Using a general notion of partial function,we take the first steps in constructive computability theory. We do this both with computability as structure, where we have direct access to programs; and with computability as property, where we must work in a program-invariant way. We demonstrate the difference between these two approaches by showing how these approaches relate to facts about computability theory arising from topos-theoretic and typetheoretic concerns. Finally, we tie the two threads together: assuming countable choice and that all total functions N - N are computable (both of which hold in the effective topos), the Rosolini partial functions, the disciplined maps, and the computable partial functions all coincide. We observe, however, that the class of all partial functions includes non-computable partial functions.