Hacker News Reader

Comment by Smaug123 | Hacker News Reader

It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs). You don't need to know how `sort` is implemented, if you know that it sorts; similarly, you don't need to know how Bolzano-Weierstrass is proved if you want to use it.

View on HN

> 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.

> > ... 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!

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).

Reply on news.ycombinator.com