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; Fri, 26 May 1995 05:04:14 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA286299334;
          Thu, 25 May 1995 21:35:34 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from lmumail.lmu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA286269332;
          Thu, 25 May 1995 21:35:33 -0600
Received: from ccMail by lmumail.lmu.edu (IMA Internet Exchange 1.04b) 
          id fc5478a0; Thu, 25 May 95 20:14:18 -0700
Mime-Version: 1.0
Date: Thu, 25 May 1995 19:50:50 -0700
Message-Id: <fc5478a0@lmumail.lmu.edu>
From: RToal@lmumail.lmu.edu (Ray Toal)
Subject: Re: Curry and uncurry
To: chou@cs.ucla.edu, info-hol@leopard.cs.byu.edu
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Description: cc:Mail note part


Ching-Tsun,

>We all know that the types 'a -> 'b -> 'c and 'a # 'b -> 'c 
>are isomorphic and the bijections between them are CURRY and 
>UNCURRY.  But I wonder whether there is a type theory in 
>which those two types are in fact _identical_, so that we 
>don't need
>CURRY and UNCURRY, don't need to worry about whether a function 
>should be curried or not, can do away with all the codes needed 
>to handle tuples (like those in the library "pair"), and 
>perhaps can even gain some efficiency.

Of course you do not *need* the type pair at all in Type Theory.
It is not primitive.  Probably what you could say is that
pairs do not exist and that f(a,b) is just syntactic sugar
for f a b.

Ray Toal