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 14:36:54 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28396; Thu, 18 Aug 1994 07:32:04 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA28391; Thu, 18 Aug 1994 07:31:57 -0600 Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <326469>; Thu, 18 Aug 1994 15:27:33 +0200 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <326465>; Thu, 18 Aug 1994 15:26:59 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8079>; Thu, 18 Aug 1994 15:26:36 +0200 From: Konrad Slind To: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk In-Reply-To: <9408181226.AA12399@switha.dcs.gla.ac.uk> (tfm@dcs.gla.ac.uk) Subject: Re: Where do type constructors come from? Message-Id: <94Aug18.152636met_dst.8079@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 18 Aug 1994 15:26:23 +0200 > There seems to be a little confusion, at least in my mind, as > to whether the original post was asking about > > (1) type constructors, as in part of the syntatic apparatus of the type > language -- e.g. in HOL things like (_)list and (_,_)fun. > > (2) type constructors, as in the term constants that denote the functions > and constant values from which the elements of a type are built -- > e.g. NIL and CONS, or INL and INR (or for that matter 0 and SUC). I was asking for both. In the ML section of the HOL book, there is a clear distinction made between type constructors and constructors. The latter are used for pattern matching. It seems to me that both are significant ideas and I thought someone would have an idea of where they came from. Alas, there is no consensus! I have had 5 replies, all different. Konrad.