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.