One often-subtle but definitely-nice improvement to language ergonomics is easy currying. For example, in languages without generics, you would need to rewrite curry for each kind of thing you want to curry. But in languages with relatively easy currying, you can easily denote things like “map a partially-applied function over some stuff, so we can apply the other arguments later”.
Haskell functions are already curried by default. But let’s say they weren’t. We could write a curried version of addition like this:
This makes use of an existing
curry function. Here’s its canonical form.
Once we have currying around, we can separate our function calls.
Haskell’s currying hides just a bit of type-based magic behind the scenes. We can make the kinds of
c explicit, and pass
f as a whole, using a lambda for its arguments instead of providing them. Here that is, in Lean
def curry (a b c : Type) (f : a × b → c) : a → b → c := fun x y, f (x, y)
Application is fairly straightforward here as well.
Python has the ability to define functions inside of functions, and it shows off the “nested” aspect of currying well.
It’s probably cleaner to use a lambda though.
Application looks essentially the same as in the other languages so far.
We can even curry in environments with more complicated static type systems, but without the simple parametricity of languages like Haskell. Here’s a C++ example. It really helps to have a language with decent lambdas!