[Prev][Next][Index][Thread]
Re: [very] basic question
Here is another reply to Scott Finnie on types versus sets.
Types and sets are not the same; but sets can be interpreted as types,
as done so elegantly by Peter Aczel in a series of basic papers,
e.g. The type theoretic interpretation of constructive set theory.
Also types can be interpreted as sets as done by Doug Howe in this
paper Semantic Basis for Embedding HOL in Nuprl (see below for more
references and citations).
Basically, the members of types are structured data elements, and the
type describes the structure, telling how the elements are constructed.
Even in pure type theory, the primitive data elements include ordered
pairs, functions, lists, streams, tagged elements (members of disjoint
unions), numbers, atoms, etc. In pure set theory, everything is a set.
Another obvious difference shows up with equality. The function spaces
A->B and A'->B' are equal as types iff A=A' and B=B'. As sets these
are equal iff they have the same elements, so-called extensional
equality. This equality can be defined in type theory in terms of the
subtype relation, A[=B (A is a subtype of B) and B[=A implies that A==B
extensionally.
A key practical difference is that functions in the type A->B are
polymorphic whereas those in the set of functions from A to B are not.
This makes subtypes behave differently than subsets, so for example if
A[A' (A is a proper subtype of A') and B[B', then (A'->B)[(A->B'),
i.e. subtyping is co-variant on the domain. This basic difference
shows up in the definition of records for example.
In computational type theory, the elements of the function space are
computable functions, and computability is a primitive axiomatic notion.
In set theory computability must be defined internally, and it is not
defined on all function spaces as it is in type theory. (Note, in both
the constructive theory and a classical one, the function space over
the natural numbers is not countable inside the theory, but is
countable from the outside.)
It is standard in type theory to include among the types collections
whose elements are types; these collections are called "kinds" or "large
types" or "universes." In set theory these correspond to large sets
called "inaccessible cardinals," and they are not part of the standard
axiomatizations.
I don't think that types are the same things as domains, so they need
not come with a partial order relation. In Nuprl we define domains as
a special kind of type, types of partial objects.
You can find more references in my 1998 article Types in Logic,
Mathematics and Programming, in the Handbook of Proof Theory, edited by
Sam Buss, Elsevier Science. I cite Aczel, Howe and many other authors
who address this topic. You can also get on-line access to the 1986
book Implementing Mathematics at our Nuprl web page:
http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html
This book presents a formal version of a very rich type theory that
unifies programming language types, logical types and mathematical types.
Under the heading of Introduction at this Web site, there is
introductory material about types, sets and domains, and in the section
Math Library there is an e-book by Stuart Allen that provides an
on-line introduction to the Nuprl type theory, one of the richest
formalizations. There are literally thousands of theorems about basic
mathematics and systems available at this site.
Bob Constable