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 15:49:07 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28896; Thu, 18 Aug 1994 08:42:57 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from gmdzi.gmd.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA28892; Thu, 18 Aug 1994 08:42:50 -0600 Received: from borneo.gmd.de (borneo) by gmdzi.gmd.de with SMTP id AA02728 (5.65c8/IDA-1.4.4 for ); Thu, 18 Aug 1994 16:38:36 +0200 Received: from borneo.gmd.de by borneo.gmd.de with SMTP id AA02884 (5.67b8/IDA-1.5); Thu, 18 Aug 1994 16:38:31 +0200 Message-Id: <199408181438.AA02884@borneo.gmd.de> To: tfm@dcs.gla.ac.uk Cc: info-hol@leopard.cs.byu.edu From: Matthew Morley Subject: Re: Where do type constructors come from? In-Reply-To: Your message of "Thu, 18 Aug 94 13:26:57 BST." <9408181226.AA12399@switha.dcs.gla.ac.uk> Date: Thu, 18 Aug 94 16:38:29 +0200 They're found under gooseberry bushes... The thing that puzzled me -- I'll own up to being the "someone" Konrad mentioned in his post -- was that the HOL system is based on Church's simple type theory, so it says, but Church never talked about sums, only funs. So HOL's type language is enriched quite a bit with (t1,...tn)op constructors. HOL is a much more powerful type theory than I hitherto imagined -- this I need to digest. Meanwhile, whence came (t1,...tn)op? M