It's just the 'mathy' type-setting which is hard to read. Types and terms are in the same font & colour and they're on the same line. To paraphrase: You can

It's just the 'mathy' type-setting which is hard to read. Types and terms are in the same font & colour and they're on the same line. To paraphrase: You can curry a function (supply its arguments one-by-one instead of all at once). You have: f(x, y) which has type (τ1 x τ2) -> τ3 You want: f x y which has type τ1 -> τ2 -> τ3 Here's a function which converts what you have to what you want: λx. λy. f(x, y) It has type: ((τ1 × τ2) → τ3) → (τ1 → τ2 → τ3) This type "Curry-Howard"s to the logical formula: (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) Since this logical formula is a tautology, the above conversion function preserves the meaning of the function it converts.