Question

I'm trying to understand why the type of:

(flip .) is: (a -> a1 -> b -> c) -> a -> b -> a1 -> c

First of all, the type of:

flip: is (a -> b -> c) -> b -> a -> c (.): is (b -> c) -> (a -> b) -> a -> c

I will rename the variables to be more clear in my explanation, so the types:

flip: is (ax -> bx -> cx) -> bx -> ax -> cx (.): is (by -> cy) -> (ay -> by) -> ay -> cy

Then I try substituing like this:

ax = (by -> cy) bx = (ay -> by) cx = ay -> cy

So the resulting type is: (ay -> by) (by -> cy) -> ay -> cy, which is different with the correct result.

Any help?

Thanks, Sebastián.

Was it helpful?

Solution

(flip .) is (.) flip, so:

  • (.) :: (bx -> cx) -> (ax -> bx) -> ax -> cx
  • flip :: (ay -> by -> cy) -> by -> ay -> cy
  • In (.) flip,
    • bx is ay -> by -> cy
    • cx is by -> ay -> cy
    • so it’s all (ax -> (ay -> by -> cy)) -> ax -> (by -> ay -> cy),
      which is just (ax -> ay -> by -> cy) -> ax -> by -> ay -> cy,
      which matches up with (flip .) :: (a -> a1 -> b -> c) -> a -> b -> a1 -> c.
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top