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

Type-two theory has a huge disadvantage: it elevates the type of all operations by a level. For example, real numbers become functions. Hence addition becomes a type 2 functional. Integration becomes type 3. It is very hard to reason about the efficiency (and computability, come to think of it) of type 3 functionals. There's some esoteric example involving the fan functional [1].

The complexity theory of type-2 functionals is a theory which is natural to ask for, but after results by Cook, Bellantoni, Kapron, Seth, Pezzoli and others, has come to an impasse and now seems abandoned.

[1] https://pdfs.semanticscholar.org/3888/cc2d3c44fb051067581e39...

They effectively change the structure of your code. Every time you do an operation on a real number, it essentially launches a new process that runs indefinitely in the background. I would file that under speed problems. To control the speed penalty, you need to make deep changes to your code. I think Andrej Bauer came to this conclusion.

Regarding computability, it's not so bad. Basically a continuous operator is usually computable. Example: Integration is continuous, hence (likely, and in this case actually) computable.

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