[Haskell-cafe] Re: Theory about uncurried functions

[Achim Schneider]

Peter Verswyvelen <bugfact at gmail.com> wrote:

> Lambda calculus is a nice theory in which every function always has
> one input and one output. Functions with multiple arguments can be
> simulated because functions are first class and hence a function can
> "return" a function. Multiple outputs cannot be done, one must embed
> these outputs in some data type, e.g. using a tuple, or one must use
> continuation passing style.
> 
Both input- and output currying are completely orthogonal, for a
sufficiently bent definition of orthogonal:

forall f :: (a, b) -> c exists g :: a -> b -> c

"likewise":

forall f :: a -> (b, c) exists (g :: a -> c, h :: a -> c)


This is, of course, abstract nonsense[1]: Usually, splitting a function
with multiple retvals into two is just a crime against efficiency, if
not clarity. I doubt any compiler could be decisive enough to get
Sufficiently Smart in this context.

> Now, does a similar theory exist of functions that always have one
> input and one output, but these inputs and outputs are *always*
> tuples? Or maybe this does not make any sense?
>
I fear it doesn't, at least if the functions are allowed to be passed
and return tuples containing bottom or unit, as you'd be left with
syntactically awkward versions of single-argument functions, or unary
tuples, whatever. 

Generally speaking, functions are more fundamental than product
types[2]:

cons :: a -> b -> ((a -> b -> c) -> c)
cons a b m = m a b

car :: ((a -> b -> a) -> c) -> c)
car z = z (\p q -> p)

cdr :: ((a -> b -> b) -> c) -> c)
cdr z = z (\p q -> q)

...as a comparison, try to define eval and apply in terms of tuples.

OTOH, you might be thinking of things like applicative functors, which
are product types[2] and can't (necessarily) be escaped from, and not
collapsed, either, as would be the case with monads. These are things
that are described in terms of a theory, not a theory themselves,
though. The important notion is that inside a specific functor, one
part of its type always stays the same (or it wouldn't be that functor
anymore... duh.)

So, to conclude: You aren't likely to find any fundamental theory
restricting inputs and outputs to tuples, but you are going to find
fundamental theories that enable you to say very interesting things
about functions which have their inputs and outputs restricted to
arbitrary types, be it sums or products.


[1] Specifically, distilled from
http://golem.ph.utexas.edu/category/2008/03/computer_scientists_needed_now.html
, which is a _very_ good and enlightening read

[2] Stolen straight from Exercise 2.4 in the Wizard Book

[3] Of a type tag and a value. Stop nitpicking. Tagged lists spoiled me.

-- 
(c) this sig last receiving data processing entity. Inspect headers
for copyright history. All rights reserved. Copying, hiring, renting,
performance and/or quoting of this signature prohibited.