4 ms·

> It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs). Note that, according to definition of 'f

> It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs). Note that, according to definition of 'function' most common in math, this is false. A function need not even be implementable. Aside: As someone trained in math I've always found explanations of type theory "fractally confusing" because of stuff like this: type theorists' words mean something different from my words, and in the explanation of what they do mean, they use words that also mean something different.

xelxebar 6y ago
> > ... a function is both its implementation and its "extension" (its effect on all inputs). > Note that, according to definition of 'function' most common in math, this is false. The standard definition of function in ZFC is a set of tuples pairing every "input" with an "output", so I think the previous commenter was correct with this reading. > A function need not even be implementable. However, if you are alluding to computable functions, then certainly, the story is a lot more interesting!
lmm 6y ago
A function is rather like a group: it's more important as an idea than as a rigorous definition. Working mathematicians may be vaguely aware that a function "is" a set of ordered pairs (just as they may be vaguely aware that a real number "is" a Dedekind cut), but they're unlikely to think about a function in those terms when they're actually working with it (unless they're working specifically on foundational issues). Indeed the set-theoretic model of a function accommodates impossible functions - but that's one of the main problems that type theory exists to solve. The type-theoretic model of a function does not correspond directly to the ZFC model of a function, but the hope of type theory is that it should correspond more closely to the day-to-day working concept of a function (whether you're a mathematician or a programmer).

xelxebar 6y ago

> > ... a function is both its implementation and its "extension" (its effect on all inputs). > Note that, according to definition of 'function' most common in math, this is false. The standard definition of function in ZFC is a set of tuples pairing every "input" with an "output", so I think the previous commenter was correct with this reading. > A function need not even be implementable. However, if you are alluding to computable functions, then certainly, the story is a lot more interesting!

lmm 6y ago

A function is rather like a group: it's more important as an idea than as a rigorous definition. Working mathematicians may be vaguely aware that a function "is" a set of ordered pairs (just as they may be vaguely aware that a real number "is" a Dedekind cut), but they're unlikely to think about a function in those terms when they're actually working with it (unless they're working specifically on foundational issues). Indeed the set-theoretic model of a function accommodates impossible functions - but that's one of the main problems that type theory exists to solve. The type-theoretic model of a function does not correspond directly to the ZFC model of a function, but the hope of type theory is that it should correspond more closely to the day-to-day working concept of a function (whether you're a mathematician or a programmer).