Higher-Order and Symbolic Computation, 13(3)179-216
Higher-Order UnCurryingJohn Hannan, Department of Computer Science and Engineering, The Pennsylvania State University, University Park, PA 16802, USA
Patrick Hicks, Department of Computer Science and Engineering, The Pennsylvania State University, University Park, PA 16802, USA
|
Abstract: We present a formal specification of unCurrying for a
higher-order, functional language with ML-style let-polymorphism. This
specification supports the general unCurrying of functions, even for
functions that are passed as arguments or returned as values. The
specification also supports partial unCurrying of any consecutive
parameters of a function, rather than only unCurrying all of a
function's parameters. We present the specification as a deductive
system that axiomatizes a judgment relating a source term with an
unCurried form of the term. We prove that this system relates only
typable terms and that it is correct with respect to an operational
semantics. We define a practical algorithm, based on algorithm W, that
implements unCurrying and prove this algorithm sound and complete with
respect to the deductive system. This algorithm generates maximally
unCurried forms of source terms. These results provide a declarative
framework for reasoning about unCurrying and support a richer form of
unCurrying than is currently found in compilers for functional
languages.
Keywords: semantics-based program analysis, type systems, program transformations |
This article can be downloaded [here].