Istari’s logic is a *type assignment* system, meaning that
computational terms (more-or-less the untyped lambda calculus) exist
prior to the type system, and the type system assigns types to them.
A term might have no type (in which case we call it ill-typed), or it
might have multiple types.

Membership in a type is a fact that is proven, and it may depend on
all available hypotheses. This means that typechecking is
undecidable. For example, if `M : A(N)`

then whether `M : A(N')`

may
depend on whether `N`

and `N'`

are equal, which is undecidable in
general. Or, as a simpler example, if `void`

follows from the current
hypotheses (which is undecidable), then any term has any type.

The undecidability of typechecking means that typing is a subject of
discourse *within the logic.* Typically, the Istari typechecker
discharges typechecking goals, but under some circumstances the user
might have to prove them. Put another way, Istari affords the user
the opportunity to establish typings that can be established
automatically.

Typing proofs are not part of the terms being typed. Thus, in the
earlier example, the `M`

that belongs to `A(N)`

and the `M`

that
belongs to `A(N')`

are literally the same term. There is no
“transport” from `A(N)`

to `A(N')`

to create obstacles to reasoning
about `M`

and its interaction with other terms. An important
consequence of this design is it streamlines the use of dependent
types.

Istari is a Martin-Löf-style type theory [2], which means (in
part) that a type consists not only of a set of elements, but also an
*equality* relation on its elements. Two terms might be equal in one
type but inequal in another. (This is most obvious with quotient
types, which coarsen the equality of an existing type.)

There is no categorical or Leibniz equality in Istari. Type-theoretic
equality is always relative to a particular type. (But see
*computational equality* below.) This has
some important consequences in the substitution rule.
There also is no “definitional equality” as a separate concept from
the equalities given by types. Put another way, the equality given
by a type **is** definitional equality.

Most Istari equalities are *extensional* in a sense appropriate to the
type. For example, to prove:

```
(fn x . M) = (fn x . N) : (A -> B)
```

one can show that `M = N : B`

assuming `x : A`

.

On the other hand, type equivalence in Istari is *intentional*,
meaning that it depends on the structure of the type expression,
rather than on its set of members or its equality. For example,
consider `A -> B`

and `A' -> B'`

. The two types are equal only when
`A`

is equivalent to `A'`

and `B`

to `B'`

, even though it is easier
for them to have the same membership (such as when `A`

and `A'`

are
empty). Formation is reflexive equivalence (see
below), so without this injectivity property we could
not, for example, conclude from `A -> B`

being well-formed that `A`

and `B`

are well-formed, which in turn would necessitate an extra
premise `B : type`

for every function application.

Every type (and its equality) is closed with respect to *computational
equality*. Thus, in order to show `M : A`

, it is permissible first to
show that `M`

is computationally equivalent to `M'`

and then show that
`M' : A`

.

Computational equality consists of beta equivalence and unfolding of defined constants. Beta equivalence is call-by-name, but that rarely matters since terms have no side effects and most types contain only terminating terms. In the implementation, reductions and certain rewrites express computational equality, and unification also understands computational equality to some extent.

Computational equality unfortunately does *not* include eta
equivalence, although most types’ equalities *are* closed under eta.
This is inevitable since computational equality is prior to types,
because one cannot justify saying `M`

is equivalent to `fn x . M x`

unless one knows that `M`

is a function. Moreover, if `M`

diverges
then clearly it cannot be considered equal to the value `fn x . M x`

.

Martin-Löf type theory is based on four judgements:

- type formation (
`A : type`

) - type equivalence (
`A = B : type`

) - membership (
`M : A`

) - equality (
`M = N : A`

)

In Istari, as in some other realizations of Martin-Löf type
theory [1], the four judgements are collapsed into one
inhabitation judgement, written `A ext M`

. Type-theoretically this
means `M = M : A`

, but the user is presented only with the type `A`

.
The inhabitant (or “extract”) `M`

is obtained automatically from the
proof.

Martin-Löf’s four judgements are internalized as types: `istp`

,
`eqtp`

, `of`

, and `eq`

, respectively. For example, `M = N : A`

is
expressed as the inhabitation of the type `eq A M N`

. Type formation
and membership are in turn defined as reflexive instances of equality;
`istp A`

means `eqtp A A`

, and `of A M`

means `eq A M M`

.

The Istari implementation understands seven sorts of hypothesis:

- term assumptions, written
`x : A`

- future term assumptions, written
`x (later) : A`

- hidden term assumptions, written
`x (hidden) : A`

- type assumptions, written
`t : type`

- future type assumptions, written
`t (later) : type`

- hidden type assumptions, written
`t (hidden) : type`

- let assumptions, written
`x = M`

Most hypotheses are simple term assumptions. Hypothetical types are usually written as term assumptions with a universe as its type, but they can also be expressed without a level using a type assumption.

Future assumptions are used in conjunction with the future modality and recursive types. They represent assumptions that will become available only in the future. When using a rule that moves into the future (such as future introduction), any future assumptions are automatically promoted to become ordinary (term or type) assumptions.

Hidden assumptions have no special status in the type theory. A
hidden assumption, say `x (later) : A`

, expresses the syntactic
restriction that `x`

cannot appear in the extract. This expresses a
sort of proof irrelevance; the extract cannot make decisions based on
`x`

if it cannot refer to `x`

at all. Hidden assumptions arise in
various ways, but especially from subset types: when
destructing `M : { x : A | B(x) }`

, we learn that `B(M)`

must be
inhabited but we have no access to the inhabitant.

A let assumption `x = M`

makes `x`

synonymous with `M`

, which can be
used to manage complexity in proofs. Like hidden assumptions, let
assumptions are unknown to the type theory. When `M`

is a fixed point
`fix (fn x . N)`

, the implementation displays the let assumption as
`x =rec= N`

.

The meaning of a hypothetical judgement is always *functional*. For
example, `x : A |- B ext M`

does **not** merely mean that
`[N/x]M : [N/x]B`

for every `N : A`

. It means that
`[N/x]B = [N'/x]B : type`

and `[N/x]M = [N'/x]M : [N/x]B`

for every
`N = N' : A`

. Additional complications arise in judgements with two
or more hypotheses (see pointwise
functionality below).

Istari supports both predicative and impredicative quantification:

Predicative quantification is accomplished using dependent types and a
cumulative hierarchy of universes. The universe `U(0)`

contains all
small types (*i.e.,* types built without mentioning universes or
kinds). The universe `U(1)`

contains all small types, and also types
built using `U(0)`

. When `j < i`

, the universe `U(i)`

contains all
types in `U(j)`

plus all types built using the universe `U(j)`

.

Note the collection of all types is not merely the union of the
universes. There exist some types that are too large to fit into any
universe. A simple example is `forall (i : level) . U(i)`

.

To quantify universally over all small types, one writes
`forall (a : U(0)) . whatever`

. The resulting type is not small;
it belongs to `U(1)`

, assuming that `whatever`

belongs to `U(1)`

.

Predicative quantification can be done using any valid type as the
domain, and results in a type one level higher. In contrast,
*impredicative* quantification can be done with only certain types,
and results in a type at the same level. The types that may be used
in impredicative quantification are called *kinds.* The type `K(i)`

contains all kinds available at level `i`

. Notably, `U(i)`

belongs to
`K(i)`

.

For example, to quantify
impredicatively over all small types,
one might write `iforall 0 (a : U(0)) . whatever`

. This quantifies
impredicatively at level `0`

, since `U(0)`

belongs to `K(0)`

. Thus,
the resulting type belongs to `U(0)`

, assuming that `whatever`

also
belongs to `U(0)`

. Note that the quantifier in that type ranges over
itself.

(In the implementation, the impredicative quantifier’s level (*e.g.,*
the first `0`

in the example) is kept implicit; it is not displayed
and it is inferred automatically. Thus impredicative quantifiers look
similar to predicative ones.)

In general, a type `A`

is a kind when `A`

is isomorphic to a space in
Istari’s metric-space semantics. Such types include function
spaces (specifically T-functions and K-functions),
non-dependent products,
unit, the future modality, and
guarded recursive types. Impredicative
quantification over guarded recursive types is one of the main
novelties of the Istari type theory.

Note that the indexing for kinds is off by one from the indexing for
universes: `K(i)`

(which contains `U(i)`

) is a subset of `U(i+1)`

.
Unlike universes, kinds are not cumulative. For example, `U(0)`

belongs to `K(0)`

, but not `K(1)`

.

Istari includes four function types. The dependent function space,
`forall (x : A) . B`

, contains functions `(fn x . M)`

such that `M : B`

assuming that `x : A`

. The non-dependent function space `A -> B`

is
the same, except `x`

does not appear free in `B`

.

Function equality is extensional. That is, `(fn x . M)`

and
`(fn x . N)`

are equal at `forall (x : A) . B`

if `M = N : B`

assuming
`x : A`

. Furthermore, since hypotheticals are always interpreted
functionally, it follows that `(fn x . M)`

equals
`(fn x . N)`

at `forall (x : A) . B`

exactly when
`[P/x]M = [Q/x]N : [P/x]B`

whenever `P = Q : A`

.

Note that if `A`

is uninhabited, `forall (x : A) . B`

and `A -> B`

are
well-formed types even when `B`

is junk.

The remaining function spaces are T-functions (`A -t> K`

) and
K-functions (`K -k> K'`

). Both of them are equal to the ordinary
function type, so they are are interchangeable with ordinary functions
to a significant degree. A minor difference is the codomain of a T-
or K-arrow must be well-formed without any assumptions, while the
codomain of an arrow may assume the domain.

The distinction of T- and K-arrow is they are kinds, so they can be used in impredicative quantification. In a T-function the domain is an ordinary type (at the same level as the kind), while in a K-function the domain is a kind.

For example, `nat -t> U(0)`

and `U(0) -k> U(0)`

both belong to `K(0)`

,
and `U(0) -t> U(1)`

belongs to `K(1)`

.

The strong sum, `exists (x : A) . B`

is Istari’s dependent type for
pairs. It contains pairs `(M , N)`

such that `M : A`

and
`N : [M / x]B`

. It also requires that `B : type`

assuming `x : A`

,
since this does not follow from the substitution instance `[M / x]B`

being a type.

The defining property of a strong sum is the elimination forms for it
are projection. If `M : exists (x : A) . B`

, then the first
projection from `M`

(written `M #1`

) has type `A`

, while the second
projection (written `M #2`

) has type `[M #1 / x]B`

.

(In contrast, the elimination form for a weak sum (such as the impredicative existential) would only give access to the constituents of the pair in a closed scope. Sometimes the weak sum is called an existential type, but we do not use that terminology in Istari, since Istari uses the strong sum for existential quantification.)

The non-dependent form of the strong sum is the product type, written
`A & B`

. (We reserve the operator `*`

for multiplication.) It plays
the role of the “and” connective.

The disjoint sum type, written `A % B`

, plays the role of the “or”
connective. (We reserve the operator `+`

for addition.) It contains
`inl M`

(“in left”) when `M : A`

, and `inl N`

(“in right”) when `N : B`

.

The intersection type, written `intersect (x : A) . B`

, is the
intersection of `B`

over all `x : A`

. Thus `N`

belongs to
`intersect (x : A) . B`

if for all `M : A`

we have ```
N :
[M / x]B
```

.

The intersection type is much like a dependent function
(particularly one whose argument is marked as implicit), but there is
an important difference: If `f : forall (x : A) . B`

and `M, M' : A`

,
then `f M : [M / x]B`

and `f M' : [M' / x]B`

are *different terms*,
even if the difference is not visually apparent because the argument
is marked implicit. However, if `g : intersect (x : A) . B`

, then
`g : [M / x]B`

and `g : [M' / x]B`

are the exact same term.

We refer to the argument to an intersection type as an *invisible*
argument, to contrast it with implicit arguments, which are present
in the term but not displayed. Invisible arguments can be supplied to
the typechecker using visibilized
application.

Intersection types can be used however the user desires, but their intended use is with levels. Consider:

```
list : intersect (i : level) . forall (a : U i) . U i
```

Recall that `nat : U i`

, for all `i`

, and that `U 0`

is contained in
`U 1`

by cumulativity. Then `list nat : U 1`

two ways: by
instantiating `i`

with `0`

and subsuming `U 0`

to `U 1`

; or by
instantiating `i`

with `1`

. Nevertheless, both paths to `U 1`

are the
*same type.* In contrast, if instead `list`

were a dependent function,
then the two paths would result in two different types, `list 0 nat`

and `list 1 nat`

.

The union type, written `union (x : A) . B`

, is the
union of `B`

over all `x : A`

. Thus `N`

belongs to
`union (x : A) . B`

whenever there exists `M : A`

such that
`N : [M / x]B`

.

The intersection is like a dependent sum
(a.k.a. `exists`

) except that the first constituent of the pair is
missing. Only the second constituent is present.

The missing first component cannot be recovered by an open scope
elimination form. Instead the elimination rule for union types
requires that the union be opened for some closed scope. Thus a union
type is a form of what is called a *weak sum.* (In other settings,
weak sums are sometimes referred to as existential types, but we will
not use that terminology here, since we use strong sums for
existential quantification).

The practical impact of this is if `x`

has a union type, `x`

cannot be
destructed if any other hypothesis refers to `x`

. (This condition can
be obtained by reverting hypotheses if necessary.) This is necessary
because the destruction tactic uses the conclusion as the closed scope
for eliminating the union.

The guarded type, written `A -g> B`

, is equivalent to `B`

if `A`

is
true. When showing membership or equality in `A -g> B`

, one may
assume `A`

. Thus when `A`

is false, `A -g> B`

contains everything.

A guarded type is similar to a non-dependent intersection
type, but not quite the same. If `A`

is
inhabited, then `intersect (_ : A) . B`

is extensionally equivalent to
`B`

(*i.e.,* they contain the same elements) but they are not equal
types. However, if `A`

is inhabited then `A -g> B`

is *equal* to `B`

.

The future modality, written `future A`

expresses that `A`

will be
true *in the future*. It contains `next M`

when `M : A`

. But, while
checking `M : A`

, any future assumptions in the context
are promoted to the present.

For example, suppose the context contains `x (later) : A`

. Then
within the `next`

, the context contains `x : A`

. Consequently we may
conclude `next x : future A`

.

Future assumptions are also promoted while showing that a future
modality is well-formed. For example, suppose again that the context
contains `x (later) : A`

. Then `future (x = x : A)`

is a well-formed
type.

The future modality is eliminated by the `let next`

form. If
`M : future A`

, then `let next x = M in N`

will add a future
hypothesis `x (later) : A`

(corresponding to the body of `M`

) while
typechecking `N`

. Moreover, `let next x = next M in N`

is beta
equivalent to `[M / x]N`

.

The main use of the future modality is (directly or indirectly) in conjunction with recursive types.

An alternative way to eliminate the future modality is using the
“previous” form, written `M #prev`

. Previous is the inverse of
next, so `(next M) #prev`

is beta equivalent to `M`

, and ```
next (M
#prev)
```

is eta equivalent to `M`

. However, type checking `#prev`

is
more baroque than `let next`

. When `M : future A`

, we may say that
`M #prev : A`

**provided** that `M #prev`

appears within a form that
moves into the future (such as `next`

or `future`

). This is necessary
because previous moves us backward in time, and we must avoid moving
all the way into the past.

(We must avoid moving into the past because the future modality is justified by a step-indexed semantics, and it is important that indices be well-ordered, so negative indices cannot be allowed.)

The two elimination forms are actually equivalent. In fact,
`let next x = M in N`

is defined to mean `[M #prev / x]N`

. Thus, ```
let
next
```

is `#prev`

wrapped up to make it more convenient to use.

Recursive types are written `rec t . A`

. As usual,
`rec t . A`

is equal to `[rec t . A / t]A`

.
However, Istari’s recursive types are *guarded* recursive types, which
means that every occurrence of `t`

in `A`

must be guarded by moving
into the future, usually using the future modality.

For example, the type `bar A`

is defined as
`rec t . A % future t`

, which means `A`

at some point in the future.
The recursive occurrence of `t`

is guarded by placing it within the
`future`

.

The guard requirement ensures that one cannot write nonsensical types
such as `rec t . t -> void`

. If it were a legal type (let’s call it
`S`

), then one could inhabit `void`

using the omega combinator:

```
(fn (x : S) . x x) (fn (x : S) . x x)
```

With the guard requirement in place, the closest one can write is
`rec t . future t -> void`

. That is a legal type, but it cannot be
used to give a type to the omega combinator.

However, one can use guarded recursive types to give a type to a
variation on the Y combinator. Let `T`

be `rec t . future t -> A`

.
Observe that the recursive occurrence of `t`

is properly guarded.
Then the following ornamented Y combinator has the type
`(future A -> A) -> A`

:

```
fn (f : future A -> A) .
(fn (x : future T) . f (let next x' = x in next (x' x)))
(next (fn (x : future T) . f (let next x' = x in next (x' x))))
```

Thus, to prove `A`

it is sufficient to prove `A`

assuming that `A`

is
true in the future. This is tantamount to proving `A`

by induction
over time. This is developed (with some minor differences) in the
partial types library `Bar`

.

One of the main features of the Istari type theory is that recursive types are not only legal types, but they are also kinds, and are thus eligible for use as domains for impredicative quantification. With some work, this makes it possible to express a store-passing transformation for imperative code [3].

In a proof, one can unroll recursive types using the
rewrite `unrollType`

.

A different self-referential type is the inductive type. Inductive types form the basis for the datatype mechanism, which is usually more convenient to use. However, there are some inductive idioms that cannot be expressed as datatypes.

An inductive type is written `mu t . A`

. The type `mu t . A`

is
extensionally equivalent to `[mu t . A / t]A`

in the sense that they
contain the same elements. However, they are not equal types.
As with recursive types, not every inductive type
expression is legal. For `mu t . A`

to be valid, `A`

must be
*positive* in `t`

.

We say that `A`

is positive in `t`

if it satisfies the following
grammar:

```
P ::= t
| M
| P & P
| P % P
| N -> P
| forall (x : N) . P
| exists (x : P) . P
| future P
| mu x . P
| if M then P else P
N ::= M
| N & N
| N % N
| P -> N
| forall (x : P) . N
| exists (x : N) . N
| future N
| mu x . N
| if M then N else N
```

Here, `P`

and `N`

express when a type is positive/negative in `t`

,
while `M`

refers to expressions that do not mention `t`

free at all.
These are merely the connectives that Istari currently supports;
several other connectives could be added without any semantic obstacle.

In a proof, one can unroll inductive types using the
rewrite `unrollType`

.

Positivity ensures both the usual monotonicity condition that one
expects for inductive types, and also a condition specific to Istari
called *robustness*. Both are necessary for an inductive type to be
semantically well-formed. Robustness is a technical condition in the
semantics pertaining to candidates arising from impredicative
quantification. Suppose `C`

and `D`

are equivalent candidates (in the
sense of having the same membership and equality), but `D`

resides in
a higher universe than `C`

. Roughly speaking, we say that `A`

is
robust in `t`

if `[C / t]A`

being well-formed implies that `[D / t]A`

is also well-formed and has the same meaning. Most type expressions
are naturally robust — since most connectives cannot distinguish
between equivalent candidates — but type expressions (notably
equality types) that can refer to `t`

being a member of a type are not
necessarily robust.

Istari’s primitive base types are `void`

, `unit`

, and `bool`

.
(Integers can also be regarded as a base type.) As
usual, `void`

is uninhabited, `unit`

contains the unit term (written
`()`

), and `bool`

contains `true`

and `false`

.

The natural number type `nat`

is introduced by `zero`

and `succ`

and
eliminated by `natcase`

and `nat_iter`

. (See the
`Nat`

library for details.)

Natural numbers are defined as `mu t . unit % t`

rather than using the
datatype mechanism because the implementation of datatypes relies on
natural numbers.

The universe type `univ i`

contains all types at level `i`

. (Recall
the discussion above.)

The universe type `kind i`

contains all the types at level `i`

that
correspond to spaces in Istari’s metric-space semantics, and are
therefore eligible for impredicative quantification. (Recall the
discussion above.)

Levels are numbers used to express levels in the universe hierarchy. Semantically levels are simply natural numbers, but in the implementation it is convenient to consider levels and natural numbers to be distinct types.

Levels are expressed using `lzero`

, `lsucc`

, and `lmax`

, with the
expected meanings. In a level expression, `lzero`

is written `0`

,
`lsucc i`

is written `1 + i`

, and `lmax i j`

is written `[i j]`

.

Equality is written `M = N : A`

. The type is well-formed whenever
`M : A`

and `N : A`

. If true, its inhabitant is `()`

. It belongs to
universe `U(i)`

whenever `A`

belongs to `U(i)`

. Equality is
always symmetric, transitive, and closed under beta equivalence. Its
other properties depend on the type `A`

.

Typing, written `M : A`

, is defined to mean `M = M : A`

. As such it
is closed under beta equivalence, and, if true, its inhabitant is
`()`

.

Since `M : A`

is defined to mean `M = M : A`

, it is well-formed when
`M : A`

. Thus, `M : A`

is well-formed exactly when it is true. This
gives rise to a phenomenon called *negatability*, which is something
of a wart in Martin-Löf-style type theory.

Typing cannot usefully be written in an antecedent position such as
`(M : A) -> B`

. The type is well-formed only when we already know
`M : A`

, so the implication serves no purpose. In the extreme case,
`not (M : A)`

, which is defined to mean `(M : A) -> void`

, can never be
true. It is well-formed only when it is false. Thus we say that
typing is *not negatable.*

Note that this does *not* mean that typing (or other non-negatable
types) cannot appear in hypotheses. On the contrary, typing
hypotheses can be very useful. It just means that typing hypotheses
do not usually arise from implication.

It is sometimes useful to say that two types are equal without
reference to a universe, either because the universe is unknown, or
the types actually do not belong to a universe. The type expressing
this fact is written `A = B : type`

. Note that this is not a form of
the equality type and there is no type called `type`

.

The type `A = B : type`

is well-formed when `A`

and `B`

are
well-formed types. If true, its inhabitant is `()`

. It belongs to
universe `U(i)`

when `A`

and `B`

both belong to universe `U(i)`

,
although that is rarely important. Type equality is always symmetric,
transitive, and closed under beta equivalence.

Type formation, written `A : type`

, is defined to mean `A = A : type`

.
As such it is closed under beta equivalence, and, if true, its
inhabitant is `()`

. Like typing, type formation is
non-negatable.

Subtyping is written `A <: B`

. It means that every element of `A`

is
an element of `B`

, and equal elements of `A`

are also equal in `B`

.
The type is well-formed whenever `A`

and `B`

are well-formed types.
If true, its inhabitant is `()`

. It belongs to universe `U(i)`

whenever `A`

and `B`

belong to `U(i)`

. Subtyping is always transitive
and closed under beta equivalence.

One can almost define `A <: B`

as `forall (x : A) . x : B`

. In fact,
the latter is sufficient to establish the former. However, the latter
is well-formed only when `A`

is a type, and when `x : B`

for all
`x : A`

. In other words, it is well-formed only when it is true, so
it is non-negatable. In contrast, the former
only requires `A`

and `B`

to be types. This means that one can
usefully express lemmas that take subtyping as antecedents.

The subset type `{ x : A | B }`

contains all the elements `M : A`

such
that `[M / x]B`

is inhabited. This is different from the dependent
sum `exists (x : A) . B`

in that the subset type does not retain the
proof of `B`

. For example, the elements of `{ x : nat | is_even(x) }`

are just numbers, while the elements of
`exists (x : nat) . is_even(x)`

are pairs of numbers and proofs.

Destructing `x : { x : A | B }`

produces `x : A`

and `y : B`

, but
since the proof of `B`

is not retained, the `y`

hypothesis must be
*hidden* to ensure that it is not used in the extract.

Equality of subset types is strong as regards the type, but weak as
regards the predicate. For `{ x : A | B }`

to be equal to
`{ x : C | D }`

, we must have that `A`

and `C`

are equal types, but
`B`

and `D`

merely need to imply each other. This is usually
convenient as it makes subset types much more likely to be equal, but
a less-desirable consequence is that we cannot conclude from
`{ x : A | B } = { x : A | C } : type`

that `x : A |- B = C : type`

.
A special case of this is we cannot conclude from
`{ x : A | B } : type`

that `x : A |- B : type`

, and that means that
eliminating a subset-type hypothesis must usually generate a subgoal
to ensure the predicate is well-formed.

A variation on the subset type (the *intensional* subset type) chooses
the other side of the tradeoff. For `iset (x : A) . B`

to equal
`iset (x : C) . D`

requires that `B`

and `D`

be equal, and not
merely imply each other. This allows one to conclude
`x : A |- B : type`

from `iset (x : A) . B : type`

, which allows us to
eliminate a premise in some rules. Intensional subset types are less
useful for most purposes due to their restricted equality, but
they are occasionally preferable due to their streamlined inference
rules. Istari uses them internally in its treatment of datatypes.

A degenerate form of the subset type that is often useful is the
squash type: `{ A }`

is defined to mean `{ _ : unit | A }`

. The
squashed type `{ A }`

is inhabited (by `()`

) exactly when `A`

is
inhabited, but one can prove a squash type without computational
access to the evidence, as might happen for example if the evidence is
in a hidden hypothesis.

Also observe that `{ A }`

is equal to `{ B }`

whenever `A`

and `B`

imply each other. This means that the squash type collapses all
inhabited types to a single type, which is useful for some purposes.

The quotient type `quotient (x y : A) . B`

coarsens the equality of
`A`

. In the quotient type, `M`

and `N`

are equal whenever
`[M / x, N / y]B`

is inhabited.

For the type `quotient (x y : A) . B`

to be well-formed, we need `A`

and `B`

to be well-formed, but we also need `B`

to be symmetric and
transitive in an appropriate sense. We do not require `B`

to be
reflexive, so the quotient type could fail to contain some elements of
`A`

.

The laws of functionality mean that some extra work must be done when
eliminating a quotient type. To show that `f`

belongs to
`(quotient (x y : A) . B) -> C`

, one must not only show that `f`

produces a `C`

for every argument in `A`

, but that it produces the
*same* `C`

for arguments that are equivalent according to `B`

.

Universal and existential quantification enjoy impredicative versions,
which might be written `iforall i (t : A) . B`

and
`iexistsi (t : A) . B`

. (In the implementation, the `i`

is kept
implicit; it is not displayed and it is inferred automaticaly.) In
each, `A`

must be a kind belonging to `K(i)`

and `B`

must be a type
belonging to `U(i)`

. Then each belongs to `U(i)`

. In contrast, if
the usual predicative quantification were used, then each would belong
to `U(1 + i)`

, since `A`

would belong to `U(1 + i)`

, not `U(i)`

.

The impredicative universal is like an intersection type in that the
argument `t`

is not passed as an argument to the “function.” This is
because impredicative quantification relies on the function being
*parametric*, but if the `t`

were available to the function, it could
discriminate on it. (In the polymorphic lambda calculus, the
dependency is typically written as a function, but there is a
syntactic separation that prevents the terms from discriminating on
types. In Istari there is no such syntactic separation.)

Similarly, the impredicative existential does not pair the witness `t`

with the inhabitant of `B`

. Thus, the impredicative existential is a
weak sum, like union types, and is subject to the same
limitations.

A related type provides impredicative polymorphism: The type
`foralltp t . B`

contains `M`

if `M : [A / t]B`

for every type `A`

(regardless of `A`

’s universe, if any). Like the impredicative
universal, `A`

is not passed as an argument to `M`

. Impredicative
polymorphism can be used with any type regardless of universe, but it
never belongs to a universe.

For technical reasons, one cannot deduce from
`iforall i (t : A) . B : type`

that `t : A |- B : type`

. (Briefly,
constructing intentional versions of impredicative types seems to
require a form of self-reference that cannot be shown to be
well-founded.) Consequently, eliminating impredicative types (and
introducing impredicative existentials) requires generating a subgoal
to establish that `B`

is well-formed. This makes impredicative
quantification not useful for typing lemmas, as such lemmas could only
be called when one knows the result already.

Both a level and a kind are necessary to determine a space. This is
why the impredicative quantifiers need to mention a level, internally
at least. In normal cases, indeed in all non-degenerate cases, the
level is uniquely determined by the kind, so it can be kept implicit.
But the type theory must include them because it is difficult to
exclude the degenerate cases, such as `rec t . future t`

.

Integers can be defined as a quotient over pairs of natural numbers:

```
quotient (a b : nat & nat) . a #1 + b #2 = a #2 + b #1 : nat
```

This is worked out in the internals of the `Integer`

library.

However, integers defined this way computationally perform very badly, like the natural numbers they are based on. For practical arithmetic, Istari provides “native” integers, where native means using the bignum library in your ML implementation. This is native enough to achieve tolerable performance.

Thus native integers do not exist in the semantics at all. Instead, the implementation supplies axioms that assert that native integers are isomorphic to defined integers in an appropriate way. (This relies on the bignum implementation being correct, of course.)

The introduction form for native integers are the integer literals
(written `z`-1`

, `z`0`

, `z`1`

, `z`2`

, etc.) An elimination
form `integer_iter`

is provided by the Integer
library, and a variety of native operations are
provided as well.

Symbols are a simple base type representing impoverished strings.
Symbol literals are written like `sym`"foo"`

, and the only operation
on symbols is equality.

The semantic meaning of the judgement `G |- A ext M`

is for all
closed substitutions `s`

and `s'`

that are equivalent at `G`

, ```
s(A) = s'(A) :
type
```

and `s(M) = s'(M) : s(A)`

. The subtle point is what it means
for two substitutions to be equivalent at a context.

(This account is a simplification of the actual Istari semantics — for various technical reasons — but it is not misleading for the purpose of understanding pointwise functionality.)

Suppose that `G`

binds each variable at most once. We say that `s`

and `s'`

are equivalent at `G`

if for all `x`

in the domain of `G`

:

`x`

is in the domain of`s`

and`s'`

`s(A) = s'(A) : type`

`s(x) = s'(x) : s(A)`

`A`

is**functional**in an appropriate sense

One notion of functionality, called *full functionality*, would
require that `t(A) = t'(A) : type`

for any closed substitutions `t`

and `t'`

that are equivalent at the context obtained by truncating `G`

immediately before `x`

’s binding. (It is easy to prove that one can
drop the functionality requirement from this latter equivalence
without changing anything.)

Full functionality is a common requirement in mathematics, but it
turns out not to work well in this sort of type theory. Instead, we
employ a looser notion of functionality called **pointwise**. Note that
looser functionality means more substitutions are equivalent, and
therefore the semantics of judgements is stronger. Thus, a theorem
proved with pointwise functionality holds true with full functionality
as well. However, pointwise functionality provides a stronger
invariant that is useful in induction arguments.

Under pointwise functionality, we require that `s(A) = s''(A) : type`

for any `s''`

that is equivalent to `s`

(again, at the context
obtained by truncating `G`

immediately before `x`

’s binding). Thus,
we require that `A`

be functional not over *all pairs* of equivalent
substitutions, but merely over substitutions that are equivalent to
the one under consideration. (Again, one can prove that one can drop
the functionality requirement from this latter equivalence without
changing anything.)

There are various ramifications to pointwise functionality, but the most important pertains to induction. Consider a proposed rule for natural number induction:

```
G |- [M/x]C
>>
G |- M : nat
G |- [0 / x]C
G, x:nat, y:C |- [succ x / x]C
G, x:nat |- C : type
```

Consider the fourth and final premise. It establishes that `C`

is
well-formed for all natural numbers `x`

. The premise is necessary
with full functionality: without it we cannot show that there are
*any* substitutions that are equivalent at `G, x:nat, y:C`

, and
without knowing that, the third premise (the inductive case) is
useless.

However, the fourth premise is a non-starter for the Istari type
theory. In many important cases, `C`

is not even well-formed unless
it is true. Every typing lemma is an example. (Recall the discussion
of negatability above.) In such cases, it is
impossible to prove the well-formedness of `C`

before proving its
truth. Consequently, one cannot reason by induction!

Pointwise functionality allows us to scrap the fourth premise. Since
we only need to know that `C`

is functional over substitutions
equivalent to the one under consideration, we can establish that `C`

is well-formed simultaneously with its truth. The second premise
tells us that `[0 / x]C`

is well-formed and true, while the third
premise tells us that if `[n / x]C`

is well-formed and true, then
`[succ n / x]C`

is well-formed and true.

The absence of any categorical equality in Istari has as an impact on the substitution rule:

```
G1, x : A, G2 |- B ext N
>>
G1, x : A, G2 |- B : type
G1, x : A, G2 |- x = M : A
G1, [M / x]G2 |- [M / x]B ext N
```

The equality in the second premise does not guarantee that we can
replace `x`

with `M`

in any context (as would be the case with
categorical equality), but only that `x`

are `M`

are equal at type
`A`

. Thus, without the first premise, Istari has no way of knowing
that `[x / x]B`

is equal to `[M / x]B`

.

(But note: a simpler rule applies when `x`

does not appear free in
`B`

, in which this issue does not arise.)

As a consequence, one cannot use substitution unless `B`

is already
known to be well-formed (or `x`

is not free in `B`

). This can cause a
problem when `C`

is a hypothesis that is not well-formed unless it is
true, as is the case in typing lemmas. (Recall the discussion
of negatability above.) Fortunately, there are usually
workarounds that do not require substitution.

The generalization rule allows one to generalize occurrences of a term in the conclusion:

```
G |- [M / x]B ext [M / x]N
>>
G |- M : A
G, x : A |- B ext N
```

But observe that the rule does not generalize occurrences of `M`

in
the context. It would be nice to have a rule that does so, such as:

```
G1, [M / x]G2 |- [M / x]B ext [M / x]N
>>
G1 |- M : A
G1, x : A, G2 |- B ext N
```

Alas, this rule is unsound. Consider the goal `G, y : [M / x]B |- C`

.
Faced with this goal, we can assume that the substitution instance
`[M / x]B`

is well-formed, but it does not follow that `B`

is
well-formed for all `x : A`

, even when `M : A`

. But if we proceeded
to the premise `G, x : A, y : B |- C`

, that is exactly what we would
be promising.

In order to generalize in this example, we must show that `B`

is
well-formed for all `x : A`

. The easiest way to do so is to move the
hypotheses that we want to generalize to the right-hand side:

```
G |- [M / x]B -> C
```

Then we can generalize, obtaining `G, x : A |- B -> C`

, and finally
reintroduce the hypothesis: `G, x : A, y : B |- C`

. That final step of
reintroducing the hypothesis generates the premise
`G, x : A |- B : type`

.

Note that the situation with generalization is opposite to that of substitution. In substitution we must generate premises requiring the conclusion to be well-formed, while in generalization we must generate premises requiring hypotheses to be well-formed.

[1] R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland,
J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler,
P. Panangaden, J.T. Sasaki, and S.F. Smith. *Implementing Mathematics
with the Nuprl Proof Development System.* Prentice-Hall, 1986.

[2] Per Martin-Löf. Constructive mathematics and computer
programming. In *Sixth International Congress of Logic Methodology and
Philosophy of Science,* volume 104 of *Studies in
Logic and the Foundations of Mathematics*. North-Holland, 1982.

[3] François Pottier. A Typed Store-Passing Translation for
General References. In *Thirty-Eighth Symposium on Principles of
Programming Languages,* 1996.