5 ms·

Here's a practical example of why it's beneficial to not be Turing complete. In Dhall, you can normalize programs, even if they are functions. For example, th

Here's a practical example of why it's beneficial to not be Turing complete. In Dhall, you can normalize programs, even if they are functions. For example, the interpreter can automatically simplify this Dhall function: let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in let exclaim = λ(t : Text) → t ++ "!" in λ(x : Text) → replicate +3 Text (exclaim x) ... to this one: λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"] ... even though we haven't applied the function to any arguments yet. You can't perform this sort of simplification (in general) if the language is Turing-complete This sort of automatic simplification comes in handy a lot when authoring configuration files. For example, if somebody objects to the import of the remote `replicate` function, you can just simplify the file and (voila!) all the imports are gone because they've all been inlined and reduced. Similarly, if somebody objects to excessive use of abstraction and functions you can similarly simplify them to remove all indirection

skybrian 9y ago
This is inlining a function and unrolling a loop. It's done in many languages, no? More generally, many automatic refactorings are not entirely safe but we do them anyway, assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. Depending on the program, substituting equals for equals might have to be rolled back for performance reasons; computing a mathematically equal value is no guarantee.
- Gabriel439 9y ago
  In a Turing complete language you can't safely inline all functions to completion without risking an infinite loop. In such a language there is no decidable way to know when to stop inlining things
  - skybrian 9y ago
    It doesn't matter in practice, because we don't need to inline every function.
    - Gabriel439 9y ago
      The key word in "automatic simplification" is "automatic". The feature loses value if a human has to intervene to specify which functions to inline or to continue inlining. Imagine how worthless `go fmt` would be if it prompted the user to confirm every change to the source code
      - qznc 9y ago
        Compilers like LLVM and GCC use heuristics not human intervention. For inlining a common heuristic is the size of the function. So we inline (even recursive functions) until the function becomes larger than a certain threshold. The threshold can be specified by a human (-finline-limit), but I believe that is rarely done.
        chriswarbo 9y ago
        This isn't compiling though; it's normalising. A heuristic like function size is useful when optimising a Turing-complete language since (a) we have to rely on some heuristic and (b) smaller binaries are generally more efficient, all else being equal, so we should avoid a size blow up regardless of what we're optimising for (speed, size, memory, etc.). In the case of normalising a non-Turing-complete language, we (a) don't need any heuristics, beta-reduction is a complete and correct strategy and (b) things like the size of a function are useless at telling us whether we've reached a normal form. In fact, I would imagine that normal forms of real Dhall programs are generally much bigger than the programs themselves, since one of the main reasons to use a language like Dhall is to reduce repetition. Also, your heuristic is heavily dependent on the evaluation order: if we have a program like this: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) Then an evaluation strategy like call-by-name will never look at big-thing, since it evaluates the functions first and they discard it: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) (\y -> small-thing) (duplicate 1000000 big-thing) small-thing small-value On the other hand, an evaluation strategy like call-by-value will evaluate big-thing, resulting in some arbitrarily large value (which may cause your heuristic to halt); then it will create 1000000 duplicates of that value (again, causing a size-based heuristic to halt); then finally it will evaluate the functions and discard the big, duplicate expression: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) (\x -> (\y -> x)) small-value (duplicate 1000000 big-thing) (\x -> (\y -> x)) small-value (duplicate 1000000 big-value) (\x -> (\y -> x)) small-value [big-value, big-value, ...] (\y -> small-value) [big-value, big-value, ...] small-value
- Karrot_Kream 9y ago
  > assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. This is a pretty labor-intensive, mechanical guarantee. If I had to run config changes through code review (like SBT configs, for example), then that slows down velocity considerably. Having a language for your config offer these guarantees means that any committer can safely make edits, without having to go through process.
mmirate 9y ago
Isn't this a result of referential transparency, not Turing-incompleteness?
- Gabriel439 9y ago
  Both. In a Turing complete language there are programs without normal forms. For example, in the untyped lambda calculus you will loop forever if you try to normalize the following expression: (\x -> x x) (\x -> x x)

skybrian 9y ago

This is inlining a function and unrolling a loop. It's done in many languages, no? More generally, many automatic refactorings are not entirely safe but we do them anyway, assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. Depending on the program, substituting equals for equals might have to be rolled back for performance reasons; computing a mathematically equal value is no guarantee.

Gabriel439 9y ago
In a Turing complete language you can't safely inline all functions to completion without risking an infinite loop. In such a language there is no decidable way to know when to stop inlining things
- skybrian 9y ago
  It doesn't matter in practice, because we don't need to inline every function.
  - Gabriel439 9y ago
    The key word in "automatic simplification" is "automatic". The feature loses value if a human has to intervene to specify which functions to inline or to continue inlining. Imagine how worthless `go fmt` would be if it prompted the user to confirm every change to the source code
    - qznc 9y ago
      Compilers like LLVM and GCC use heuristics not human intervention. For inlining a common heuristic is the size of the function. So we inline (even recursive functions) until the function becomes larger than a certain threshold. The threshold can be specified by a human (-finline-limit), but I believe that is rarely done.
      - chriswarbo 9y ago
        This isn't compiling though; it's normalising. A heuristic like function size is useful when optimising a Turing-complete language since (a) we have to rely on some heuristic and (b) smaller binaries are generally more efficient, all else being equal, so we should avoid a size blow up regardless of what we're optimising for (speed, size, memory, etc.). In the case of normalising a non-Turing-complete language, we (a) don't need any heuristics, beta-reduction is a complete and correct strategy and (b) things like the size of a function are useless at telling us whether we've reached a normal form. In fact, I would imagine that normal forms of real Dhall programs are generally much bigger than the programs themselves, since one of the main reasons to use a language like Dhall is to reduce repetition. Also, your heuristic is heavily dependent on the evaluation order: if we have a program like this: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) Then an evaluation strategy like call-by-name will never look at big-thing, since it evaluates the functions first and they discard it: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) (\y -> small-thing) (duplicate 1000000 big-thing) small-thing small-value On the other hand, an evaluation strategy like call-by-value will evaluate big-thing, resulting in some arbitrarily large value (which may cause your heuristic to halt); then it will create 1000000 duplicates of that value (again, causing a size-based heuristic to halt); then finally it will evaluate the functions and discard the big, duplicate expression: (\x -> (\y -> x)) small-thing (duplicate 1000000 big-thing) (\x -> (\y -> x)) small-value (duplicate 1000000 big-thing) (\x -> (\y -> x)) small-value (duplicate 1000000 big-value) (\x -> (\y -> x)) small-value [big-value, big-value, ...] (\y -> small-value) [big-value, big-value, ...] small-value
Karrot_Kream 9y ago
> assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. This is a pretty labor-intensive, mechanical guarantee. If I had to run config changes through code review (like SBT configs, for example), then that slows down velocity considerably. Having a language for your config offer these guarantees means that any committer can safely make edits, without having to go through process.

mmirate 9y ago

Isn't this a result of referential transparency, not Turing-incompleteness?

Gabriel439 9y ago
Both. In a Turing complete language there are programs without normal forms. For example, in the untyped lambda calculus you will loop forever if you try to normalize the following expression: (\x -> x x) (\x -> x x)