Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 ?


share|cite|improve this question
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
up vote 3 down vote accepted

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
share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.