[tel]

Also to explain that strange "adjunction" comment, currying results from the notion that the things of type

    (a, b) -> c

are exactly equivalent to the things of type

    a -> (b -> c)

An adjunction (F, G) occurs when the things of type (F a -> c) are equivalent to things of type (a -> G c), so if we pick F x = (x, b) and G x = (b -> x) then we see that currying is an adjunction between (,b) and (b ->).

[evincarofautumn]

One intuition for this is that (a, b) is the product type (a × b) and the function arrow (a → b) corresponds to exponentiation (b^a), so you get the isomorphism for free from the identity c^(a × b) = (c^b)^a.