On defining "multivariable" functions by partial application in Haskell-like languages

7
votes

So. I'm actually tinkering with the Idris language, by somewhat following Brady's Type-Driven Development with Idris. I don't think what I written here is that tied to a specific programing language (and I don't know any Haskell, for that matter). But I don't know where else I could post this, given that I have no knowledge of partial-application/currying, types, lambdas and all that stuff from the mathematician's perspective.

Some context

In the second chapter of the book the author draws attention to the following scenario.

Given the self-explaining snippet

double : Num a => a -> a
double x = x + x

rotate : Shape -> Shape

where Shape : Type and rotate are holes for the type of a shape and for a function that rotates a Shape by 90 degrees respectively, there is an obvious pattern behind a quadruple and a turn-around function

quadruple : Num a => a -> a
quadruple x = double (double x)

turn_around : Shape -> Shape
turn around x = rotate (rotate x)

which lead us to write a twice (high-order) function capable of applying two times the same operator.

To my eyes, there are mostly two ways to solve the problem. The first is just to follow Brady's code

twice : (ty -> ty) -> ty -> ty
twice f x = f (f x)

where he actually defines the image twice f : ty -> ty of the twice function over an arbitrary f1.

The second one, which seems to me a little bit more elegant, is to define twice by the means of a composite function and/or an anonymous function, by changing a little bit its signature

twice : (ty -> ty) -> ty
twice f = composite f f

composite : (ty_2 -> ty_3) -> (ty_1 -> ty_2) -> (ty_1 -> ty_3)
composite g f = \x => g (f x)

Both approaches lead to the final result

turn_around : Shape -> Shape
turn_around = twice rotate

The question(s)

I'll try to keep my questions as clear as I can, so instead of mistreating elementary compsci terminology I will keep things concrete.

  1. Let's say we have a "multivariable" function

    f : ty_1 -> ty_2 -> ... -> ty_n

    Then f is a function taking x_1 : ty_1 to another function f x_1 : ty_1 -> ... -> ty_n. When should we choose define f by writing

    f x_1 = stuff

    instead of

    f x_1 ... x_{n-2} = stuff2

  2. Could someone clarify me the differences between two two approaches (Brady's and mine) reported above?

1Yes, I'm a math student...
1
haskellidris
It is worth noting that the phrase "partial function" has a different common use than what (I think) you are using here. Usually, a "partial function" is something that is like a function, except that it might not produce an output when given some of the values in its domain (because it isn't defined on that input, because it does not terminate when given that input or throws an exception on that input in a way not described by its codomain). Maybe you're thinking of partial application. – David Young
Of course I meant partial application. I've updated the title. Thank you! – user13383731

1 Answers

6
votes

There's no hard and fast "rule" telling when one should use one style over another.

A function defined as

f x = \y => ...

is exactly equal to the function defined as

f x y = ...

We might prefer the first notation when we want to stress that we like to see f as a 1-ary function whose codomain is made of functions. We would instead use the second notation when we like to see f as a 2-ary function.

For function composition you wrote

composite g f = \x => g (f x)

since composition is commonly regarded as a 2-ary function. We could also have written

composite g f x = g (f x)

but this, albeit shorter, is not as clear, since it suggests the human reader to consider composite as a 3-ary function. Being a human, I also prefer the first form, but there would be no preference for a computer.

If I could not use composition as you did, I would have written Brady's code as

twice f = \x => f (f x)

to stress that we really want to see twice as a function-to-function mapping (endo-to-endo, to be picky). The two forms are completely equivalent.

Finally, a more mathy note: from a foundational standpoint, there is no need for the notation

f x1 ... xn = stuff

which we commonly use to define functions. To be extremely pedantic, the above does not actually define f, but only defines how f behaves when applied to n arguments. Since we know that that uniquely identifies f, we don't care about that. But, if we did, we would define f as we define anything else, i.e. with a defining equation of the form

f = something

and in particular

f = \x1 .. x2 => stuff

So, each definition of the form f x1 .. xn = ... with n>0 can be regarded as syntactic sugar: a notation that we can use to program, but that we can ignore when studying the theory related to the programming language. Concretely, if I need to mathematically prove a property on all programs P, I don't have to consider the cases where P makes use of the syntactic sugar, but only the cases where every equation has the form f = ..., possibly involving lambdas. This simplifies the proof, since we need to deal with fewer cases.

Now, I don't know Idris too much, so I don't know if this conversion to lambdas is possible in all cases, in Idris. In Agda it would not be possible because of how dependent elimination is performed, for instance. In Coq it would instead be possible. Until you need dependent types you should be fine.