2
votes

Currently I am trying to learn Haskell with the book 'Learn You a Haskell' and I'm trying to understand the implementations of the flip function in chapter 5. The problem is that the author states that if g x y = f y x is valid, then f y x = g x y must be also true. But how and why does this reversal affects the two function definitions?

I know how currying works and I also know that the -> operator is right-associative by default so the type declarations are in fact the same. I also understand the functions apart from each other but not how the reversal of g x y = f y x is in relation with this.

first flip function

flip' :: (a -> b -> c) -> (b -> a -> c)
flip' f = g
    where g x y = f y x

second flip function

flip' :: (a -> b -> c) -> b -> a -> c
flip' f y x = f x y
2
Both functions are equivalent, what is the problem? - Willem Van Onsem
I have no idea what the author is trying to say there either. - melpomene
Possibly confusion over f being used in the definition of g, since it's not an argument of g? - chepner

2 Answers

8
votes

I think the argument the author has in his head got wildly abbreviated to the point that it's not even sensical. But here is my guess about the reasoning. We start with the first definition:

flip f = g where g x y = f y x

Now we observe that this is a curried thing, and we use all the discussion of associativity of (->) and junk to write the same thing, but with two extra arguments to f. Like this:

flip f x y = g x y where g x y = f y x

Now we have the equation that he called out as going both ways: g x y = f y x and vice versa. We can rewrite the body of the flip using this equation, like this:

flip f x y = f y x where g x y = f y x

Since the body of the definition no longer mentions g, we can delete it.

flip f x y = f y x

And now we're pretty much there. In the final definition, the author has swapped the names x and y everywhere. I don't know why they chose to do so, but it is a legal move that you can make in equational reasoning, so no problem there. Doing so gives us their final equation:

flip f y x = f x y
3
votes

flip takes a function and returns the flipped version of the function. One way to define flip' is to include the application in the definition itself, since

flip' f y x = f x y  ===> flip' f y = \x -> f x y
                     ===> flip' f = \y -> \x -> f x y

That is, flip' f is a function that applies f to its own arguments in reverse order.

The second definition simply gives the anonymous function \y -> \x -> f x y a name first, then uses that name as the definition of flip' f x y.

                     ===> flip' f = g where g = \y -> \x -> f x y
                     ===> flip' f = g where g y = \x -> f x y
                     ===> flip' f = g where g y x = f x y

That is, flip' f is some function g, where g is defined to apply f to the arguments of g in reverse order.

The definitions g x y = f y x and g y x = f x y are equivalent up to alpha conversion. In both cases, f is a free variable in the definition of g; g is as a closure over the f argument to flip'.