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

Re: [very] basic question

Even before going into fixpoints and higher-order functions and domain
equations, one might object to the notion of types-as-sets on the basis that
it is too fine-grained 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 one-element set, but which one? It doesn't matter, and in fact the same
holds for every single type constructor in the typed lambda-calculus.

Having realized that, you might start wondering whether the properties you
need to model typed lambda-calculus 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) 253-3261 Fax +31 (030) 251-379