37 ms·

Several recent languages that came from the FP community recently tend to achieve this. This is the case of Agda, for instance, and I believe Idris also has tot

by pyrale 6y ago

Several recent languages that came from the FP community recently tend to achieve this. This is the case of Agda, for instance, and I believe Idris also has totality checking.

adwn 6y ago
Maybe you mean optional totality? As in, a function can be declared to be total and the compiler tries to prove it? A language cannot be Turing-complete if it completely forbids non-termination, there is no way around this. Or stated differently: If a language is Turing-complete, then there are programs that don't terminate. If a Turing-complete language only has functions which are total (i.e., which always terminate), then it has another mechanism which allows non-termination, e.g. unbounded loops and mutable state.
- pyrale 6y ago
  > A language cannot be Turing-complete if it completely forbids non-termination, there is no way around this. I do acknowledge this. My point is that turing-completeness is not necessarily a desirable aspect of a language. You can check out Agda if you are interested in what can be done with a total language. For some use-cases, like seting up a mainloop, you need an escape hatch because that mainloop is not going to be total. But not every program needs that. Conversely, a programming language that doesn't care about totality won't be able to sere other use-cases, such as building proven programs. My understanding is that it's much easier to build an escape hatch in total languages, than it is to retrofit non-total languages to prove programs.
  - adwn 6y ago
    > My point is that turing-completeness is not necessarily a desirable aspect of a language. Ah, okay, I see. > For some use-cases, like seting up a mainloop, you need an escape hatch because that mainloop is not going to be total. But not every program needs that. Hmm, I would argue that in practice, nearly all programs will need that, because they're either potentially non-terminating (let's call this "type 1") or have a runtime with a bound which is not determined by any of its inputs ("type 2"). Examples for type 1 include firmware, kernels, drivers, database engines, any kind of server, all programs with a GUI, all REPLs, and many Unix-style utilities that process or generate streams (thing grep, cat, sed, dd). Examples for type 2 include all programs with non-blocking IO (because even if the input and output are known to be bounded, the number of read/write calls is potentially unbounded) and most programs which take a file name as input (because the file size is not part of the program's input). That doesn't leave many exceptions. I admit, however, that in most cases you could structure your program so that it has a non-total mainloop which exclusively calls proven total functions. But I don't think this is very useful, because even in safety-relevant, hard real-time contexts, termination is not sufficient, but termination within a certain timespan.
    - pyrale 6y ago
      > That doesn't leave many exceptions. Examples of programs which are useful and terminate are batch programs. Besides that, even in a server, you may want to ensure that a subset of the program terminates. For instance, if you're using a serverless architecture, knowing that your lambda will terminate may be useful. Much like the separation between pure and impure functions in fp, having a distinction between total and non-total functions means that you can limit your non-total code to a couple dozen LoCs, which is a reasonable thing to manually check. > But I don't think this is very useful, because even in safety-relevant, hard real-time contexts, termination is not sufficient, but termination within a certain timespan. Once you've broken the non-termination issue, it becomes much more reasonable to start working on time estimates. Basically, once you've said that the number of instructions needed to solve the problem is a function of your input size, calculating that function becomes a possibility.

by pyrale 6y ago

Several recent languages that came from the FP community recently tend to achieve this. This is the case of Agda, for instance, and I believe Idris also has totality checking.

adwn 6y ago

Maybe you mean optional totality? As in, a function can be declared to be total and the compiler tries to prove it? A language cannot be Turing-complete if it completely forbids non-termination, there is no way around this. Or stated differently: If a language is Turing-complete, then there are programs that don't terminate. If a Turing-complete language only has functions which are total (i.e., which always terminate), then it has another mechanism which allows non-termination, e.g. unbounded loops and mutable state.

pyrale 6y ago
> A language cannot be Turing-complete if it completely forbids non-termination, there is no way around this. I do acknowledge this. My point is that turing-completeness is not necessarily a desirable aspect of a language. You can check out Agda if you are interested in what can be done with a total language. For some use-cases, like seting up a mainloop, you need an escape hatch because that mainloop is not going to be total. But not every program needs that. Conversely, a programming language that doesn't care about totality won't be able to sere other use-cases, such as building proven programs. My understanding is that it's much easier to build an escape hatch in total languages, than it is to retrofit non-total languages to prove programs.
- adwn 6y ago
  > My point is that turing-completeness is not necessarily a desirable aspect of a language. Ah, okay, I see. > For some use-cases, like seting up a mainloop, you need an escape hatch because that mainloop is not going to be total. But not every program needs that. Hmm, I would argue that in practice, nearly all programs will need that, because they're either potentially non-terminating (let's call this "type 1") or have a runtime with a bound which is not determined by any of its inputs ("type 2"). Examples for type 1 include firmware, kernels, drivers, database engines, any kind of server, all programs with a GUI, all REPLs, and many Unix-style utilities that process or generate streams (thing grep, cat, sed, dd). Examples for type 2 include all programs with non-blocking IO (because even if the input and output are known to be bounded, the number of read/write calls is potentially unbounded) and most programs which take a file name as input (because the file size is not part of the program's input). That doesn't leave many exceptions. I admit, however, that in most cases you could structure your program so that it has a non-total mainloop which exclusively calls proven total functions. But I don't think this is very useful, because even in safety-relevant, hard real-time contexts, termination is not sufficient, but termination within a certain timespan.
  - pyrale 6y ago
    > That doesn't leave many exceptions. Examples of programs which are useful and terminate are batch programs. Besides that, even in a server, you may want to ensure that a subset of the program terminates. For instance, if you're using a serverless architecture, knowing that your lambda will terminate may be useful. Much like the separation between pure and impure functions in fp, having a distinction between total and non-total functions means that you can limit your non-total code to a couple dozen LoCs, which is a reasonable thing to manually check. > But I don't think this is very useful, because even in safety-relevant, hard real-time contexts, termination is not sufficient, but termination within a certain timespan. Once you've broken the non-termination issue, it becomes much more reasonable to start working on time estimates. Basically, once you've said that the number of instructions needed to solve the problem is a function of your input size, calculating that function becomes a possibility.