2 ms·
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
by sn41 8y ago
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/cc2d3c44fb051067581e3947c3b9f9af1d5c.pdf https://pdfs.semanticscholar.org/3888/cc2d3c44fb051067581e39...
- man-and-laptop 8y agoThey 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.