A universality theorem for PCF with recursive types, parallel-or and ∃
Thomas Streicher · Mathematical Structures in Computer Science · 1994
In a PCF-like call-by-name typed λ-calculus with a minimal fixpoint operator, ‘parallelor’, Plotkin's ‘continuous existential quantifier’ ∃ and recursive types together with constructors and destructors, all computable objects can be denoted by terms of the programming language. According to A. Meyer's terminology (cf. Meyer (1988)), such a programming language is called universal in the sense that any extension of it must be conservative, as all computable objects can already be expressed by program terms. As a byproduct, we get that, in principle, recursive types could be totally avoided, as they appear as syntactically expressible retracts of the non-recursive type → , where and are the flat domains of natural numbers and boolean values, respectively.