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 [4], 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:
A : type)A = B : type)M : A)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:
x : Ax (later) : Ax (hidden) : At : typet (later) : typet (hidden) : typex = MMost 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 coguarded type, written A &g B, is equivalent to B if A is
true. When showing membership or equality in A &g B, one must also
prove A. Conversely, from a proof of A &g B one may conclude that
A is true; although that fact will be hidden and thus
not available to computational content.
A guarded type is similar to a non-dependent union type, but not quite the same. Since the union type is a weak sum, it has a limited destruction rule, but the only limitation when destructing a coguard is the hypothesis representing its left-hand-side is hidden.
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
simulated 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 [5].
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.
Partial types make it possible to express possibly non-terminating
computations [2, 6, 3]. We refer to such computations as partial
objects. The partial type, partial A, contains all the elements of
A, in addition to all divergent terms. Two terms are equal at
partial A if they have the same halting behavior, and if they are
equal at A if they halt.
There are three main ways to inhabit a partial type:
First, the canonical divergent term bottom (defined as
fix (fn x . x)) inhabits every partial type.
Second, we say that a type A is strict if A <: partial A.
Since partial A contains all the members of A, the only fact we
need to say that A is strict is that the inclusion of A into
partial A preserves equality. For that to be the case, we need
A not to equate any convergent term with any divergent term, since
in partial A terms with different halting behavior are never
equal.
Most types in Istari are strict. Indeed, most types in Istari have
the stronger property of totality, meaning they contain only
convergent terms. Thus one may usually take members of A to be
members of partial A.
Third, we can create a partial object by recursion, using the fixpoint induction rule.
Given a term F with type partial A -> partial A, fixpoint
induction allows us to conclude (under certain circumstances) that
fix F : partial A. Alas, this principle is available only for types
A that are admissible, and there do exist
non-admissible types.
Roughly speaking, a type A is semantically admissible if whenever
A contains an infinite chain of approximations to some recursive
computation M, it also contains M. However, within the logic we
cannot reason about such chains directly and we must instead rely on a
set of rules for showing that types are admissible. For example,
A -> B is admissible whenever B is admissible, and A & B is
admissible whenever both A and B are admissible.
One major device for showing that a type is admissible is
upwards-closure. We say that A is an uptype (short for
“upwards-closed type”) if whenever M : A and M computationally
approximates M' then M' : A. Every uptype is admissible since the
members of a chain approximate their limit.
Uptypes are a useful way to show admissibility because most types are
uptypes. The main exceptions are partial types (bottom approximates
everything but partial types do not contain everything) and universes
(which can talk about membership in a partial type).
(Note that more admissibility and uptype rules could be added than Istari currently supports.)
The type halts M expresses the fact that M halts; it is
well-formed when M belongs to any partial type. If
M = N : partial A and halts M, we can conclude that M = N : A.
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) : types(x) = s'(x) : s(A)A is functional in an appropriate senseOne 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] Robert L Constable and Scott Fraser Smith. Partial Objects in Constructive Type Theory. In Second IEEE Symposium on Logic in Computer Science. 1984.
[3] Karl Crary. Type-Theoretic Methodology for Practical Programming Languages. Ph.D. dissertation, Cornell University, 1998.
[4] 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.
[5] François Pottier. A Typed Store-Passing Translation for General References. In Thirty-Eighth Symposium on Principles of Programming Languages, 1996.
[6] Scott Fraser Smith. Partial Objects in Type Theory. Ph.D. dissertation, Cornell University. 1989.