[Prev][Next][Index][Thread]

Re: [very] basic question

On Wed, 31 Oct 2001, Scott Finnie wrote:

> Could someone explain the difference between types & sets?  The maths
> texts I have available (undergrad comp. sci. stuff) state their
> equivalence explicitly, yet many writings I've looked up on the web
> differentiate between them.

You've had a few responses from a computer science point of view now; I'd
like to give my opinion, coming from a more mathematical background.  I
think the one thing that's been made clear so far is that this is not a
very basic question at all; it's quite a profound one.  There is by no
means one correct opinion that type theorists have settled on.  I am often
disappointed that attention to type theory has largely been confined to
computer scientists so far, when I think there are many issues (such as
this one) that mathematicians and philosophers are better placed to
investigate.

Type theory and set theory are both formal theories that try to deal with
our notion of "collection of things"; but they do so in different ways.  
The differences are subtle, and, when stated informally, they sound
pedantic or hair-splitting; but they lead to important differences in the
way the theories can be used.  Please don't spend too long analysing the
exact words I use; I'm doing my best to express things that aren't fully
understood.  I'm afraid the only real way to understand the differences is
to get involved in the formal theories yourself.

On the level of the logic used, the major difference is that, in set
theory, "a (epsilon) A" (a is a member of the set A) is one proposition
among many.  We can make it the hypothesis or conclusion of an implication
(If a (epsilon) A then ...), we can make it part of a disjunction (Either
a (epsilon) A or b (epsilon) A), and so forth.

Whereas, in type theory, "a : A" (a is an object of type A) is on a
different level to the propositions that the logic deals with.  We can
define predicates on the objects of a given type and use them to form
propositions, we can quantify over them (For all objects of type A,...;
There exists an object of type A such that ...), but that's as far as it
goes.  As far is the logic is concerned, which objects are of which type
is a given, and not something that can be reasoned about; it is not false
to state that an object is of the wrong type, it is meaningless, or not
well-formed.  Perhaps a better way of putting it is that the types are
constraints on which propositions can be formed, rather than objects in
their own right that we can form propositions about.

When setting up a set theory, we take the objects as given, and talk about
in what ways they can be formed into collections.  When setting up a type
theory, the objects come with the type; to specify a type is to state how
its objects behaved.  Function spaces give a good example: in set theory,
the statement of the existence of functions, and the description of the
behaviour of an individual function, is completely separate from the
statement that there is a set consisting of all the functions from A to B.
Whereas, in type theory, the rules that make the objects of A->B functions
from A to B are also the rules that make A->B the type of all such
functions.

A few formal details will (I hope) make this difference much clearer.  In
set theory, we can define:

"A function f from A to B is an object such that, given any x in A, there
is exactly one y in B such that (x,y) is in f."

We can then state

"For any term t(x) such that t(x) is in B whenever x is in A, there is a
function f from A to B whose value at any x in A is t(x)."

and this is completely separate from the statement

"There exists a set whose members are all and only the functions from A to
B."

In type theory, we have the rules

x : A |- t(x) : B              f : A -> B       a : A
----------------------         ----------------------
lambda x:A.t(x) : A->B              f(a) : B

(read "If, whenever x : A, t(x) : B, then the function with value t(x) for
any x:A is in A->B" and "If f:A->B and a:A then f(a):B")

These rules describe what it is to be a function from A to B, and set up
the type A->B, together; the two cannot be separated.

I hope I've been of help to you; I hope, at least, I've shown how deep the
question runs.  Please feel free to mail the list, or contact me directly,
if you think I can be of more help.

--
Robin Adams