Re: [very] basic question

To: Scott Finnie <scott@projtech.com>
Subject: Re: [very] basic question
From: Jamie Andrews <andrews@csd.uwo.ca>
Date: Thu, 8 Nov 2001 23:14:46 -0500 (EST)
cc: type theory mailing list <types@cis.upenn.edu>
In-Reply-To: <200111071546.fA7FkA721288@saul.cis.upenn.edu>

Slightly different take on this...

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.

     One could view a type as being basically the same thing as
the set of all terms that are members of that type.  I believe
that in the 1970a and early 1980s there were some papers written
taking that view, and basing typechecking on set theory. 
(Sorry, can't think of any references offhand.)

     Eventually, the more recent view prevailed.  I would
characterize that view as saying that we don't understand the
significance of a type except in the context of a formal system
which tells us what terms are in what types.

     The more recent view is somewhat more convenient because by
taking it, we can base typechecking on formal systems, use them
as our reference to settle all disputes, and tune them to other
purposes, such as decidability.  For instance, if someone brings
up the embarrassing point that types A and B have exactly the
same terms inhabiting them but we don't consider one to be a
subtype of the other, then we can just say "we don't consider a
type to be a set; we consider the subtype relation to be given
by this here formal system, which is consistent with the type
inhabitation relation but which doesn't necessarily work like a
subset relation."

     Hope this helps.

--Jamie.