Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 13:48:23 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27991;
          Thu, 18 Aug 1994 06:41:04 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA27987;
          Thu, 18 Aug 1994 06:40:59 -0600
Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <13020-0@goggins.dcs.gla.ac.uk>;
          Thu, 18 Aug 1994 13:27:01 +0100
Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA12399;
          Thu, 18 Aug 94 13:26:57 BST
From: tfm@dcs.gla.ac.uk
Message-Id: <9408181226.AA12399@switha.dcs.gla.ac.uk>
To: Roger Bishop Jones <rbj@win.icl.co.uk>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Where do type constructors come from?
In-Reply-To: Your message of "Wed, 17 Aug 94 08:29:43 BST." <9408170729.4145.0@win.icl.co.uk>
Date: Thu, 18 Aug 94 13:26:57 +0100


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 think (2) is what Garrell meant and (1) is what Roger meant.  In any case,
it may be pretty hard to decide exactly where to attribute the "invention"
of these things -- or at least the ideas behind them.

Tom