Currying
Z Wikipedii
Currying jest to operacja w funkcyjnych językach programowania polegająca na przekształceniu funkcji, która pobiera parę argumentów i zwraca wynik (f : (P × Q) → R) w funkcję, która po pobraniu argumentu zwraca funkcję, która pobiera argument i zwraca wynik (g : P → (Q → R)). Operacja odwrotna nosi nazwę uncurryingu.
Podstawą dla tej operacji jest ugruntowanie systemu typów w językach funkcyjnych na rachunku lambda z typami. Taki rachunek na mocy izomorfizmu Curry'ego-Howarda jest równoważny pewnej logice intuicjonistycznej, a zatem operacja ta odpowiada tautologii logiki intuicjonistycznej: ((p ∧ q) → r) ↔ (p → (q → r)).