# How is the following ML Curry expression evaluated

This question is not homework but it's related to material in a general course I take about programming languages, so I don't know whats the site policy about this

In ML the following expression:

fun f x y z = x (y , z) = x (z, y) ;


Evaluates to this:

val ('a, ''b) f = fn : ('a * 'a -> ''b) -> 'a -> 'a -> bool


I understand the type inference done here, but not the structure of the expression returned.

Can someone explain how this works ?

Thanks

-
I'm confused as to what you don't understand. The type of f is a function of three arguments: the first argument is a function of type 'a * 'a -> 'b, and the two other arguments are of type 'a. The result is of type bool. Is this what you don't understand? –  cody Feb 19 '13 at 19:46
@cody Yeah thats what I don't understand. I understand the first part of 'a * 'a -> ''b but not the second part ? What's the general approach of understanding this ? How would you convert it to a normal function ? –  Michael Feb 19 '13 at 19:49

It seems that what you are confused about is the common practice of Curryfication: the function $$(\alpha\times \alpha\rightarrow \beta)\rightarrow \alpha\rightarrow \alpha\rightarrow \mathrm{bool}$$

Is parenthesized as:

$$(\alpha\times \alpha\rightarrow \beta)\rightarrow (\alpha\rightarrow (\alpha\rightarrow \mathrm{bool}))$$

and is equivalent to a different function: $$(\alpha\times \alpha\rightarrow \beta)\times \alpha\times \alpha\rightarrow \mathrm{bool}$$

The reason for this is the following. Take a function:

$$f:A \rightarrow (B\rightarrow C)$$ This is a function that takes an element $a:A$ and returns a function $$f\ a: B\rightarrow C$$ Apply this to an element $b:B$ and you have $$f\ a\ b:C$$

It is clear that this is equivalent to a function $f':A\times B\rightarrow C$ that takes a pair $(a,b):A\times B$ and returns an element of $C$. The equivalence can be explicitely written:

curry : ('a * 'b -> 'c) -> ('a -> 'b -> 'c)
curry f' = function x -> function y -> f' (x,y)


or more simply

curry f' x y = f' (x,y)


The other direction goes:

uncurry : ('a -> 'b -> 'c) -> ('a * 'b -> 'c)
uncurry f = function p -> let (x,y) = p in f x y


or simply

uncurry f (x,y) = f x y

-