3 ms·

You do if you want to reach a normal form. Note that the author isn't talking about compiling or optimising, they're talking about normalising. I don't know of

You do if you want to reach a normal form. Note that the author isn't talking about compiling or optimising, they're talking about normalising. I don't know of a Turing-complete language where we can ask to normalise some arbitrary expression including going 'under a lambda' (i.e. performing partial application, etc. inside function invocations; what you refer to as 'inlining'). The closest I can think of is expanding Lisp macros, but they're already a "compile time" transformation so I'm not sure how comparable they are (although of course Lisp can interleave compilation with evaluation!)

skybrian 9y ago
The place where using a non-Turing complete language actually matters is in constructive proofs where it's common to write a function without running it. This can be used to show that a value can be constructed in principle, even if it's not a practical program because it would take billions of years. But practical programming is about writing programs that we actually want to run. The distinction between "takes far too long" and "hangs forever" is unimportant because real-world tasks have at least an informal deadline: how long the user is willing to wait. And most performance testing is done by actually running programs, not via static analysis alone, because we want to know how fast the code is on real-world hardware. This particular language is something you'd use to generate large, repetitive configurations. It makes sense for that use case that you'd want to make sure all macros can be expanded. But you don't have to prove this statically, because you can actually run the program and look at what it generates. Doing config file generation using a Turing-complete language would also work fine; if you accidentally create an infinite loop (or just very slow code), you can hit control-C and fix the bug.
- Gabriel439 9y ago
  For the purposes of evaluation, it's still an improvement to have a total language. As I mentioned in another thread, using a totality checker is like wearing seatbelts: it doesn't protect against everything, but it's still a huge improvement.

skybrian 9y ago

The place where using a non-Turing complete language actually matters is in constructive proofs where it's common to write a function without running it. This can be used to show that a value can be constructed in principle, even if it's not a practical program because it would take billions of years. But practical programming is about writing programs that we actually want to run. The distinction between "takes far too long" and "hangs forever" is unimportant because real-world tasks have at least an informal deadline: how long the user is willing to wait. And most performance testing is done by actually running programs, not via static analysis alone, because we want to know how fast the code is on real-world hardware. This particular language is something you'd use to generate large, repetitive configurations. It makes sense for that use case that you'd want to make sure all macros can be expanded. But you don't have to prove this statically, because you can actually run the program and look at what it generates. Doing config file generation using a Turing-complete language would also work fine; if you accidentally create an infinite loop (or just very slow code), you can hit control-C and fix the bug.

Gabriel439 9y ago
For the purposes of evaluation, it's still an improvement to have a total language. As I mentioned in another thread, using a totality checker is like wearing seatbelts: it doesn't protect against everything, but it's still a huge improvement.