Parametric Polymorphism question in OCaml

0
votes

This polymorphic function allows us to flip the order of the arguments of an arbitrary curried function:

 # let flip f x y = f y x ;;
   val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

That is flip takes a function of type 'a -> 'b -> 'c and returns a function of type b -> 'a -> 'c. But I actually don't get it, why it is correct? how the order of a,b,c are determined by ? Pretty confused about it, can anyone explain for me, thank you.

2
ocamlparametric-polymorphism
The short answer is that the order of a and b are determined by the order of x and y, and c is determined by the return type of f. – Jeffrey Scofield
yes, I see that, but why the order is reversed, the original is x come after f, y come after x (f x y). After flipping it became f y x, but why the order of a,b,c are not mapping the same order as that ? – JJ E
The return type of f doesn't change. So the last type variable will be the same in both cases. Only the type variables for x and y will change, because the order of the parameters is inverted. – Jeffrey Scofield
In the other word, this is may looks silly, I'm wondering why is not ('a -> 'b -> 'c) -> ('a -> 'c -> 'b) ? I think this is make more sense to me. – JJ E
As you say, the input to flip is a function of type a -> b -> c. So the type of f is a -> b -> c. The return type of flip is also a function. Think of what this returned function is going to return itself. It's the same as the return type of the input function. I.e., it's c. So your type can't be right. Your proposed type would return a type that is one of the parameters of f. – Jeffrey Scofield

2 Answers

3
votes

Let's consider types of all given variables. If we have f : 'a -> 'b -> 'c, then from the code f y x in the function definition we have y : 'a and x : 'b. Also a return type of flip (i.e. a type of flip f x y) is a type of f y x, so 'c.

The function flip has three parameters, f, x, and y in this order. And it returns a value of f y x. Therefore the type of flip is:

flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
       ----------------    --    --    --
         |                  |     |     |_ The type of the return value, (f y x)
         |                  |     |_ The type of y
         |                  |_ The type of x
         |_ The type of f
1
votes

Perhaps this might help you. Instead of, 

let flip f x y = f y x ;;

write the equivalent definition,

let flip f = fun x y -> f y x;;

now look at the type, 

val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

it's the same as this, with parenthesis, 

val flip : ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)

the function flip takes a function f of type 'a -> 'b -> 'c and returns the function \fun x y -> f y x of type 'b -> 'a -> 'c.