From owner-qed Mon Aug 8 09:30:14 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA09428 for qed-out; Mon, 8 Aug 1994 09:29:13 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA09417 for ; Mon, 8 Aug 1994 09:29:04 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Mon, 8 Aug 1994 15:28:47 +0100
To: qed@mcs.anl.gov (qed list)
Subject: Re: Types Considered Harmful
In-reply-to: Your message of "Mon, 08 Aug 94 01:40:14 MDT." <199408080740.BAA07142@chelm.nmt.edu>
Date: Mon, 08 Aug 94 15:28:37 +0100
From: John Harrison
Message-ID: <"swan.cl.cam.:196540:940808142854"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
Victor Yodaiken writes:
| Did I miss something, or is this just a not so wonderful re-explanation
| of how everything can be encoded in sets?
I thought its message was really "Types considered unnecessary". The
argument that types get in the way of mathematics is, in my view, true in
certain cases (one Javier Thayer and I discussed was finding the algebraic
closure of a field) but there is no supporting evidence given in this
paper -- it's merely stated as a fact.
The discussion of undefinedness is far too offhand -- I believe that a
more elaborate treatment of undefinedness (as in IMPS) is implicit in many
mathematical notations and habits.
Riemann integration is something that can just as well be done in simple
type theory (it has, in a slightly different form, been done in HOL). And
as I never tire of saying, lambda calculus provides a good way of dealing
with variable binding constructs.
The final remark about mathematicians having "gotten along" without types
for 2000 years might equally be applied to sets.
But the paper was quite a good read, and the topic merits discussion. I'm
an agnostic on the question, though I am much more familiar with formal
proofs in type theory than set theory. It may only be when we push
formalization into more complicated parts of mathematics that we have the
perspective to decide the issue.
John.