Каррирование — λ-исчисление

А что, если функция двух переменных? А такие вообще бывают? Ответ простой: нет, не бывают. Ладно-ладно, шучу. Бывают, просто они, как луковица, завёрнуты в оболочки, а такой концепт называется каррированием в честь Хаскелла Карри. Да, это тот самый Haskell Curry, в честь которого назван и язык Haskell.

f(x, y) \quad\rightsquigarrow\quad f = \lambda x.\,\lambda y.\,M, \qquad f\,a\,b = (f\,a)\,b

(1.9)

Формально это изоморфизм, то есть биекция между двумя множествами функций.

\mathrm{Hom}(A \times B,\, C) \;\cong\; \mathrm{Hom}(A,\, \mathrm{Hom}(B,\, C))

(1.10)

В формуле слева — функции из пары $A \times B$ в $C$ , справа — функции из $A$ в функции из $B$ в $C$ . Каждой функции двух аргументов $g \colon A \times B \to C$ отвечает ровно одна каррированная $\hat g \colon A \to (B \to C)$ по правилу $\hat g(a)(b) = g(a, b)$ , и наоборот — $g(a, b) = \hat g(a)(b)$ . Эти два перехода взаимно обратны, ничего не теряя и не добавляя, поэтому оба множества функций попросту неразличимы.

Несколько примеров из Haskell:

-- тип функции нескольких аргументов — правоассоциативная цепочка стрелок
f :: a -> b -> c   -- то же самое, что a -> (b -> c)

-- частичное применение: add 2 — «недоданная» функция
add :: Int -> Int -> Int
add x y = x + y
add2 :: Int -> Int
add2 = add 2
map add2 [1, 2, 3]  -- [3, 4, 5]

-- переходники curry и uncurry — свидетели изоморфизма
curry   :: ((a, b) -> c) -> a -> b -> c
uncurry :: (a -> b -> c) -> (a, b) -> c

-- сечения операторов — то же частичное применение
(+3)  :: Num a => a -> a
(*2)  :: Num a => a -> a