Functions are just a different kind of value. Needing to know the type of the values you're using when you use them isn't "nonlocal reasoning". And it's not li

Functions are just a different kind of value. Needing to know the type of the values you're using when you use them isn't "nonlocal reasoning". And it's not like curried function application involves type-driven parsing or anything. (f x y) is just parsed and compiled as two function calls ((f x) y), regardless of the type of anything involved, just as (x * y * z) is parsed as ((x * y) * z) in mainstream languages. (Except for C, because C actually does have type-driven parsing for the asterisk.) Another way to look at it: languages like Haskell only have functions with one argument, and function application is just written "f x" instead of "f(x)". Everything follows from there. Not a huge difference.