Because of the intimate connection between values and notations in constructive mathematical notation, there are two manners, or "moods", of discourse involving types (ontic and semantic). There are two corresponding notions of "type", (ontic and semantic), plus a third notion of type, "intensional type", which is exploited in the formulation of Nuprl's logic (see
Ontic Types and Ontic Mood.
The ontic "mood" is that of
a priori discourse about values; it is the one most like informal, pre-theoretical discourse. Thus, one talks about numbers, functions, pairs, etc. In this mood, a type is a class of values, and a type expression stands for such a class.
In the ontic mood,
It is the formalization of the ontic mood that the logic of computational type theory aims at, but to do this carefully requires us to engage in a form of semantic discourse.
Semantic Types and Semantic Mood.
The semantic mood is that of discourse about expressions and reference. For example,
The general semantic form we adopt for types is to associate with each type expression a so-called partial equivalence relation, i.e. a symmetric transitive relation, on expressions; this relation is called the "equality" of the type. The semantics of computational type theory requires a notion of "expression" whose syntax and execution semantics is independent of the definition of types. Restrictions on candidates for an equality relation include that any expression satisfying the relation is closed, i.e. has no free variables, and that if
As a practical matter, Nuprl further requires that rewriting any subexpression of an expression, of whatever type, by a step of computation must result in an "equal" term of that type. It turns out that this constraint will follow from a few painless restrictions on the computation and type definition, which we do not further discuss here; this result is due to Doug Howe (see also
Ontic vs Semantic.
So, in the ontic mood, we may truly say that the boolean type
In the semantic mood,
One tends to use both moods since in order to be able to talk intuitionistically about a class of values, one must adopt a notation for those values that is computationally adequate.
Standard examples are natural numbers and functions.
A notation for natural numbers counts as constructively adequate just when one can effectively determine from any notation for a number whether that number is zero, and if it is not, one can effectively find a notation for its predecessor.
Let us suppose we have such a method for notating numbers, and call it
A notation for a function, say from naturals to naturals, using the notational method