Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 18 Aug 1994 11:54:29 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26882; Thu, 18 Aug 1994 04:46:11 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from relay1.pipex.net by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26878; Thu, 18 Aug 1994 04:45:59 -0600 Received: from q.icl.co.uk by relay1.pipex.net with SMTP (PP) id <05271-0@relay1.pipex.net>; Thu, 18 Aug 1994 11:41:22 +0100 Received: from ming.oasis.icl.co.uk by Q.icl.co.uk (4.1/icl-2.12-server) id AA20075; Thu, 18 Aug 94 11:42:07 BST Received: from norman.win.icl.co.uk (norman.win01.icl.co.uk) on ming.oasis.icl.co.uk id AA21115; Thu, 18 Aug 94 11:39:15 BST From: Roger Bishop Jones Date: Wed, 17 Aug 94 08:29:43 BST Message-Id: <9408170729.4145.0@win.icl.co.uk> To: info-hol@leopard.cs.byu.edu Subject: Re: Where do type constructors come from? Citing a type-free language as the origin of type constructors sounds pretty original to me. Full marks to Garrell for lateral thinking. I would suggest that the origin is Bertrand Russell, in his paper on the Theory of Types, dated 1907. He may not actually use the term "type constructor" and I suppose you might quibble about how close his notion of type is to modern schemes. If you don't like Russell's scheme, I still don't see why you should come any closer than 1940, when Church published his simple theory of types, though I don't know that this was the first publication of a type system close to that of HOL. Aren't all these references in the HOL manuals? (they certainly are in the ProofPower manuals). regards, Roger Jones