Atomic judgments

RedPRL currently has five forms of atomic (non-hypothetical) judgments that may appear in subgoals.

  1. Truth asserts that a type is inhabited.
  2. Type equality asserts an equality between two types.
  3. Subtyping asserts a subtyping relation.
  4. Subkinding asserts that some type is actually a universe in which all types has a particular kind.
  5. Term lets the user give an expression.

Note that these judgment forms differ from our semantic presentations in papers.

Truth

A truth judgment

a true

or simply

a

means a is an inhabited type. Any inhabitant can realize this judgment. For example, the expression 1 realizes

int

because 1 is in the type int. This is commonly used to state a theorem or specify the type of the program to be implemented. In fact, all top-level theorems (see Defining theorems) must be in this judgmental form.

Type equality

A type equality judgment

a = b type

means a are b are equal types (without regard to universe level), and its realizer must be ax, the same as the realizer of equality types. For example, we have

int = int type

realized by ax. Multiverses are supported through kind markers such as kan or discrete:

a = b discrete type
a = b kan type
a = b coe type
a = b hcom type
a = b pre type

where a = b kan type means a and b are equal Kan types. (The judgment a = b type is really an abbreviation of a = b pre type because pre is the default kind.) Following the PRL family of proof assistants which use partial equivalence relations, well-typedness is defined as the equality of the type and itself; to save some typing, a type stands for a = a type and a kan type stands for a = a kan type.

In the presence of universes and equality types, one might wonder why we still have a dedicated judgmental form for type equality. That is, one may intuitively treat the judgment

a = b type

as (= (U l) a b) true for some unknown universe level l. It turns out to be very convenient to state type equality without specifying the universe levels; with this, we survived without a universe level synthesizer as the one in Nuprl, which was created to alleviate the burden of guessing universe levels.

Subtyping

A subtype judgment

a <= b type

states that a is a subtype of b. More precisely, the partial equivalence relation associated with a is a subrelation of the one associated with b. The realizer must be ax. There is no support of kind markers because the subtyping relation never takes additional structures into consideration.

This is currently used whenever we only need a subtyping relationship rather than type equality. For example, if a function f is in type (-> a b), the rule to determine whether the function application ($ f x) is in type b' will only demand b <= b' type rather than b = b' type. That said, the only non-trivial subtyping relation one can prove in RedPRL now is the cumulativity of universes. One instance would be

(U 0 discrete) <= (U 1 kan)

realized by ax.

Subkinding

The following are subkind judgments:

a <= discrete universe
a <= kan universe
a <= coe universe
a <= hcom universe
a <= pre universe

They assert that a is a subuniverse of the universe of the specified kind at the omega level. Intuitively, a <= k universe would be the subtyping judgment a <= (U omega k) type if we could internalize universes at the omega level. The realizer must be ax. These judgments play the same role as subtyping judgments except that they handle the cases where the right hand side is some omega-level universe. Suppose a function f is in type (-> a b). The rule to determine whether the function application ($ f x) is a type will demand b <= pre universe rather than b = (U omega) type (or b = (U l) type for some universe level l).

Term

A term judgment is displayed in the sort of the expression it is asking for, for example:

dim
exp

The realizer is the received term from the user. This is used to obtain motives or dimension expressions. For example, the rewrite tactic requires users to specify the parts to be rewritten by fulfilling term subgoals.