6 ms·

"And they might be right. But mathematical functions have one big advantage over non-mathematical ones — their type signature tells you everything that the func

"And they might be right. But mathematical functions have one big advantage over non-mathematical ones — their type signature tells you everything that the function does. This is probably the reason why most functional languages are strongly-typed." I'm confused about this statement. types give you important contextual information about the function in a summarized form, but surely we can have two functions with the same type signature that perform different mappings.

mrkeen 3y ago
> surely we can have two functions with the same type signature that perform different mappings. Yes - and you can count the mappings! Enums are sometimes referred to as 'sum types' because you can just add up the number of different states they can be in. Structs are sometimes call 'product types' because you can calculate the number of states they can be in by multiplying the number of states of their members. And functions are 'exponential types'.
edgyquant 3y ago
This might be true in a programming language but it’s not for mathematical functions which is what they refer to in the first half of this paragraph. I think what they mean is that two functions won’t have the exact same signature and result typings, though in practice this isn’t normally true for computer systems. Although there’s an argument that if it has those exact same things maybe you don’t need two functions but to improve your one function to be more robust.
justincredible 3y ago
I've usually heard this phrased as the signature implies only one possibly function, but that is in a very abstract sense. This phrasing is more intuitive as it's saying the signature constrains what the function could possibly do. For example, if you have a function of type ℕ x ℕ -> ℕ you know it could be doing addition, multiplication or exponentiation, but it can't do division because then it could only be a partial function. A more abstract signature ℕ x ℕ x Op -> ℕ, where Op is the set of binary operations on the natural numbers, can really only do one thing (apply the operands to the operation). Another example, [A] -> A could be any fixed indexing function, but it can't be a function that produces a value of A not found in the list as the true signature of that function is just A per se. As a sibling comment points out, in the context of programming the signature isn't as constraining as it would be in maths as the distinction between total and partial functions is often ignored and you can have side effects. But the more you model your functions to be pure and total the more you can reason about them abstractly.

mrkeen 3y ago

> surely we can have two functions with the same type signature that perform different mappings. Yes - and you can count the mappings! Enums are sometimes referred to as 'sum types' because you can just add up the number of different states they can be in. Structs are sometimes call 'product types' because you can calculate the number of states they can be in by multiplying the number of states of their members. And functions are 'exponential types'.

edgyquant 3y ago

This might be true in a programming language but it’s not for mathematical functions which is what they refer to in the first half of this paragraph. I think what they mean is that two functions won’t have the exact same signature and result typings, though in practice this isn’t normally true for computer systems. Although there’s an argument that if it has those exact same things maybe you don’t need two functions but to improve your one function to be more robust.

justincredible 3y ago

I've usually heard this phrased as the signature implies only one possibly function, but that is in a very abstract sense. This phrasing is more intuitive as it's saying the signature constrains what the function could possibly do. For example, if you have a function of type ℕ x ℕ -> ℕ you know it could be doing addition, multiplication or exponentiation, but it can't do division because then it could only be a partial function. A more abstract signature ℕ x ℕ x Op -> ℕ, where Op is the set of binary operations on the natural numbers, can really only do one thing (apply the operands to the operation). Another example, [A] -> A could be any fixed indexing function, but it can't be a function that produces a value of A not found in the list as the true signature of that function is just A per se. As a sibling comment points out, in the context of programming the signature isn't as constraining as it would be in maths as the distinction between total and partial functions is often ignored and you can have side effects. But the more you model your functions to be pure and total the more you can reason about them abstractly.