Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: chou@cs.ucla.edu, info-hol@leopard.cs.byu.edu
Cc: chou@cs.ucla.edu
In-Reply-To: <9505242115.AA25832@maui.cs.ucla.edu> (chou@cs.ucla.edu)
Subject: Re: Curry and uncurry
Message-Id: <95May26.111852met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 26 May 1995 11:18:51 +0200


> 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.

I can't claim to have the big picture yet, but the following is a place
to start:

    UNCURRY f (x,y) = f x y

can be seen as a "case" statement for pairs. Analogues are easy to
define for other types:

    (num_case v f 0 = v) /\ (num_case v f (SUC x) = f x)
    (list_case v f [] = v) /\ (list_case v f (CONS h t) = f h t)
    (sum_case f1 f2 (Inl v) = f1 v) /\ (sum_case f1 f2 (Inr w) = f2 w)

In general, a datatype with "n" constructors yields a case theorem with
"n" clauses. The case theorem for a type ty can be used to break apart a
term with type ty and safely apply a function of the right type to the
components. How does this help? Well, it generalizes the "pair problem",
and so makes it more attractive to add extensive support for case
expressions. For instance, case-expressions give pattern matching style
lambda abstractions, and that ought to be supported by making
GEN_BETA_CONV a bit more general and defining it earlier so that other
tools can use it instead of BETA_CONV. For quantifiers, the idea of
paired quantifications can perhaps be extended to pattern-matching
quantifications, maybe by extending the restricted quantification
machinery.

All this amounts to building support on top of the existing
logic. Changing the prelogic to accomodate the equivalence of 'a -> 'b
-> 'c and 'a # 'b -> 'c would also be an interesting alternative. I can see
that it would make the basic operations slower, but that might be worth
it for the user.

Konrad.