Hacker News new | past | comments | ask | show | jobs | submit login

No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't.

See also https://news.ycombinator.com/item?id=12403508

Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".

Not all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact