[Prev][Next][Index][Thread]
Re: [very] basic question

To: sheldon@alum.mit.edu

Subject: Re: [very] basic question

From: Frank Atanassow <franka@cs.uu.nl>

Date: Thu, 8 Nov 2001 13:08:35 +0100

Cc: scott@projtech.com, types@cis.upenn.edu

InReplyTo: <200111071912.fA7JCSr29851@saul.cis.upenn.edu>; from sheldon@psrg.lcs.mit.edu on Wed, Nov 07, 2001 at 01:46:30PM 0500

References: <200111071546.fA7FkA721288@saul.cis.upenn.edu> <200111071912.fA7JCSr29851@saul.cis.upenn.edu>

UserAgent: Mutt/1.2.5i
Even before going into fixpoints and higherorder functions and domain
equations, one might object to the notion of typesassets on the basis that
it is too finegrained an equivalence. In most programming languages, types
are only defined up to isomorphism, i.e., the particular representations of
values don't really matter. For example, you could model the ML type "unit" as
a oneelement set, but which one? It doesn't matter, and in fact the same
holds for every single type constructor in the typed lambdacalculus.
Having realized that, you might start wondering whether the properties you
need to model typed lambdacalculus really have anything specifically to do
with sets at all! If you formulate those properties, then you discover that
there actually is a large collection of candidate structures, and sets and
functions are only one lone example (though admittedly one with a lot of
historical momentum). The upshot is that, though you can reason about sets
by treating them as types, if you try to reason about types by treating them
as sets, you may go wrong.

Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 2533261 Fax +31 (030) 251379