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; Wed, 24 May 1995 23:04:35 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA085240232;
          Wed, 24 May 1995 15:17:12 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from maui.cs.ucla.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA085150228;
          Wed, 24 May 1995 15:17:08 -0600
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.27) 
          id AA25832; Wed, 24 May 95 14:15:32 PDT
Message-Id: <9505242115.AA25832@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Cc: chou@cs.ucla.edu
Subject: Curry and uncurry
Date: Wed, 24 May 95 14:15:32 PDT
From: chou@cs.ucla.edu


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.

However, I don't know whether the above question makes sense at all!
I'd appreciate any comments.

- Ching Tsun