Currying

Currying is an operation that exploits the following mathematical isomorphism of types:

$$\funtype {t,t'}{t''} \;\simeq\; \funtype {t}{(\funtype {t'}{t''})}$$ (4.1)

which can be generalized to its multiple form:

$$\funtype {t_1,\ldots,t_n}{t} \;\simeq\; \funtype {t_1,\ldots,t_k}{(\funtype {t_{k+1},\ldots,t_n}{t})} \;\;\;k=1,\ldots,n-1$$ (4.2)

When function currying is enabled, this means that type-checking/inference must build this equational theory into the type unification rules in order to consider types equal modulo this isomorphism.