5 ms·

> For one thing, unbounded loops are situationally fine. The key distinction is that the program has to make forward progress regardless, which is not always th

> For one thing, unbounded loops are situationally fine. The key distinction is that the program has to make forward progress regardless, which is not always the same thing as escaping the loop. The article somewhat alludes to this, although they don't use the notion of progress that you use, which is extremely important. > This rule does not, of course, apply to iterations that are meant to be nonterminating—for example, in a process scheduler. In those special cases, the reverse rule is applied: It should be possible for a checking tool to prove statically that the iteration cannot terminate. As a further searchable term, people can look up "total functions." Total functions must either terminate (loop ends) or be productive (always make forward progress). That as many functions as possible should be total is a pretty good rule of thumb in any codebase.

TeMPOraL 3y ago
>> In those special cases, the reverse rule is applied: It should be possible for a checking tool to prove statically that the iteration cannot terminate. This part made me pause for a moment, but then it clicked, and I'm remembering the rare and unusual experience of facing a process that escaped a loop that was supposed to go on indefinitely. A software equivalent of transmission belt slipping off. Most frequently seen in video games, where it's mostly harmless - but imagining a scheduler in an embedded system quitting on me like this fills me with dread to irrational extent. > As a further searchable term, people can look up "total functions." Total functions must either terminate (loop ends) or be productive (always make forward progress). That's a new one to me. I'm not deep into more advanced flavors of functional programming, but I thought total functions are defined as terminating in finite time for all inputs. I suppose it depends on whether you consider infinite loop a successful termination in infinity or not, but personally I wouldn't, at least not when it's clear the function is plain running in circles (as opposed to asymptotically approaching a value).
- AlotOfReading 3y ago
  Yep, it's a bit terrifying to contemplate. If you're ever unfortunate enough to do safety critical systems, you'll have to remember that you have to protect against this not only at the software level with formal methods, but also at the hardware level to ensure that e.g. a bit flip in the CPU registers or the instruction sequence as it travels from memory also doesn't violate your safety model.
- dwohnitmok 3y ago
  > I'm not deep into more advanced flavors of functional programming, but I thought total functions are defined as terminating in finite time for all inputs. The main paper that lays this out is "Total Functional Programming" (https://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf https://www.jucs.org/jucs_10_7/total_functional_programming/...). But to briefly summarize: I was playing a bit fast and loose with wording since most notions of total functions are built on top of FP languages as you point out and therefore ultimately on the lambda calculus where we don't have a native notion of a loop. Instead of loops in FP languages we have lists (and folds on the list or an unfold to generate the list) and other data structures that reify the notion of iteration. Hence what I was really saying is that a total function can also generate an infinite data structure, which is only roughly like saying an infinite loop. Totality is usually formally defined in terms of data and codata (or equivalently recursion and corecursion). The co- prefix may sound a bit scary, but an informal way of thinking about it is that data is always finite and codata can be infinite. The canonical example is that a list is an example of data and an infinite, lazy stream is an example of codata. This seems like a lot of ceremony for no real good reason if you consider an "infinite" data structure as simply a finite data structure that can store functions that happens to have additional computation in it hidden behind some closure. And indeed you are still correct that an informal and usually sufficiently useful definition of totality for a function is that it terminates in finite time for all inputs (after all even if you generate an "infinite" data structure you still terminate in finite time and just hide the additional computation within a finite data structure). It's still nice to have the data vs codata distinction though. Practically speaking bringing in the notion of codata gives us a nice little heuristic for checking termination when creating an infinite data structure. Only types marked as codata are allowed to have infinite descent and when returning them from a function we have to always follow a certain syntactic pattern known as guarded recursion. Otherwise if we didn't have the notion of codata, a naive termination checker would have a hard time with checking termination of a function that recurses on itself, but only behind a lambda. E.g. // Pseudo-code data class Stream(head: Int, rest: () => Stream) // generateIncrementingStream(0) generates the infinite stream 0, 1, 2, ... generateIncrementingStream(start: Int): Int = { Stream(start, () => generateIncrementingStream(start + 1)) // This appears to a naive termination checker to never terminate // You could try to simply check if the recursive call is inside a function // but then you run into other issues if e.g. the entire function is called // again and it becomes very thorny very quickly // e.g. Stream(start, {(() => generateIncrementingStream(start + 1))(); () => generateIncrementingStream(start + 1)} // never terminates even though all calls to generateIncrementingStream are // contained behind lambdas. You might have to start doing some annoying // symbolic computation. } vs // Note that the recursive call to Stream in rest is no longer behind a lambda // Under the hood this might be implemented with lambdas codata class Stream(head: Int, rest: Stream) def generateIncrementingStream(start: Int): Stream = { // Much easier heuristic: all recursive calls must be inside a codata // constructor, i.e. "guarded" by a constructor call hence "guarded recursion" Stream(start, generateIncrementingStream(start + 1)) } The general idea here is that a function that generates codata is productive and hence total if it generates a finite amount of the potentially infinite codata structure before its next recursive call. A nice heuristic that captures most useful cases is guarded recursion (of course because of the halting problem this is only a heuristic). The usual heuristic is that for functions that generate data, you must have structural recursion, i.e. every recursive call must be on a piece of data "smaller" than the original input. On the other hand if you generate codata, you must have guarded recursion, i.e. every recursive call must be guarded behind a codata constructor. This resolves some things quite nicely. E.g. if have a recursive function that accepts a codata `Stream` and wants to return some data, e.g. a finite `List`, then we must have some other argument that gets smaller every function call. E.g. // Taking in infinite codata and producing finite data def take(stream: Stream, n: NaturalNum): List[Int] = { n match { // This passes totality checking because m is "smaller" than n, which here // means we had to strip away one level of NaturalNum constructors // hence Successor(m) => Cons(stream.head, take(stream.rest, m)) Zero => EmptyList } } def streamIdentity(stream: Stream): Stream = { // Since we're producing codata, we check for guarded recursion // Passes totality checker because streamIdentity is guarded behind Stream Stream(stream.head, streamIdentity(stream.rest)) } def listIdentity<A>(list: List[A]): List[A] = { list match { case EmptyList => EmptyList // Since we're producing data, we check for structural recursion // Passes totality checker because the recursive call is on a smaller piece of data case Cons(x, rest) => Cons(x, listIdentity(rest)) } } // Can't blindly produce finite data from an infinite piece of codata! def nontotalStreamToList(stream: Stream): List[Int] = { // Looking for structural recursion // Does not pass totality checker because stream.rest is not considered to be smaller than stream since Stream is codata Cons(stream.head, nontotalStreamToList(stream.rest)) } // Can definitely produce infinite codata from finite data though def padOutListWithInfiniteZeroes(initialSegment: List[Int]): Stream = { initialSegment match { case Cons(x, rest) => Stream x (padOutListWithInfiniteZeroes(rest)) case EmptyList => Stream 0 (padOutListWithInfiniteZeroes(initialSegment)) } } Bringing in the notion of codata also gives us some theoretical nicety. How do you express totality for a program that must run forever, e.g. a server? You say that the IO type a la Haskell is codata and that's that! Then you know that `main` having the `IO` type means that it can potentially run forever, but it will always generate a finite amount of stuff on every codata "iteration" and therefore is productive and is not just spinning its wheels in a pointless infinite loop that does nothing.

TeMPOraL 3y ago

>> In those special cases, the reverse rule is applied: It should be possible for a checking tool to prove statically that the iteration cannot terminate. This part made me pause for a moment, but then it clicked, and I'm remembering the rare and unusual experience of facing a process that escaped a loop that was supposed to go on indefinitely. A software equivalent of transmission belt slipping off. Most frequently seen in video games, where it's mostly harmless - but imagining a scheduler in an embedded system quitting on me like this fills me with dread to irrational extent. > As a further searchable term, people can look up "total functions." Total functions must either terminate (loop ends) or be productive (always make forward progress). That's a new one to me. I'm not deep into more advanced flavors of functional programming, but I thought total functions are defined as terminating in finite time for all inputs. I suppose it depends on whether you consider infinite loop a successful termination in infinity or not, but personally I wouldn't, at least not when it's clear the function is plain running in circles (as opposed to asymptotically approaching a value).

AlotOfReading 3y ago
Yep, it's a bit terrifying to contemplate. If you're ever unfortunate enough to do safety critical systems, you'll have to remember that you have to protect against this not only at the software level with formal methods, but also at the hardware level to ensure that e.g. a bit flip in the CPU registers or the instruction sequence as it travels from memory also doesn't violate your safety model.
dwohnitmok 3y ago
> I'm not deep into more advanced flavors of functional programming, but I thought total functions are defined as terminating in finite time for all inputs. The main paper that lays this out is "Total Functional Programming" (https://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf https://www.jucs.org/jucs_10_7/total_functional_programming/...). But to briefly summarize: I was playing a bit fast and loose with wording since most notions of total functions are built on top of FP languages as you point out and therefore ultimately on the lambda calculus where we don't have a native notion of a loop. Instead of loops in FP languages we have lists (and folds on the list or an unfold to generate the list) and other data structures that reify the notion of iteration. Hence what I was really saying is that a total function can also generate an infinite data structure, which is only roughly like saying an infinite loop. Totality is usually formally defined in terms of data and codata (or equivalently recursion and corecursion). The co- prefix may sound a bit scary, but an informal way of thinking about it is that data is always finite and codata can be infinite. The canonical example is that a list is an example of data and an infinite, lazy stream is an example of codata. This seems like a lot of ceremony for no real good reason if you consider an "infinite" data structure as simply a finite data structure that can store functions that happens to have additional computation in it hidden behind some closure. And indeed you are still correct that an informal and usually sufficiently useful definition of totality for a function is that it terminates in finite time for all inputs (after all even if you generate an "infinite" data structure you still terminate in finite time and just hide the additional computation within a finite data structure). It's still nice to have the data vs codata distinction though. Practically speaking bringing in the notion of codata gives us a nice little heuristic for checking termination when creating an infinite data structure. Only types marked as codata are allowed to have infinite descent and when returning them from a function we have to always follow a certain syntactic pattern known as guarded recursion. Otherwise if we didn't have the notion of codata, a naive termination checker would have a hard time with checking termination of a function that recurses on itself, but only behind a lambda. E.g. // Pseudo-code data class Stream(head: Int, rest: () => Stream) // generateIncrementingStream(0) generates the infinite stream 0, 1, 2, ... generateIncrementingStream(start: Int): Int = { Stream(start, () => generateIncrementingStream(start + 1)) // This appears to a naive termination checker to never terminate // You could try to simply check if the recursive call is inside a function // but then you run into other issues if e.g. the entire function is called // again and it becomes very thorny very quickly // e.g. Stream(start, {(() => generateIncrementingStream(start + 1))(); () => generateIncrementingStream(start + 1)} // never terminates even though all calls to generateIncrementingStream are // contained behind lambdas. You might have to start doing some annoying // symbolic computation. } vs // Note that the recursive call to Stream in rest is no longer behind a lambda // Under the hood this might be implemented with lambdas codata class Stream(head: Int, rest: Stream) def generateIncrementingStream(start: Int): Stream = { // Much easier heuristic: all recursive calls must be inside a codata // constructor, i.e. "guarded" by a constructor call hence "guarded recursion" Stream(start, generateIncrementingStream(start + 1)) } The general idea here is that a function that generates codata is productive and hence total if it generates a finite amount of the potentially infinite codata structure before its next recursive call. A nice heuristic that captures most useful cases is guarded recursion (of course because of the halting problem this is only a heuristic). The usual heuristic is that for functions that generate data, you must have structural recursion, i.e. every recursive call must be on a piece of data "smaller" than the original input. On the other hand if you generate codata, you must have guarded recursion, i.e. every recursive call must be guarded behind a codata constructor. This resolves some things quite nicely. E.g. if have a recursive function that accepts a codata `Stream` and wants to return some data, e.g. a finite `List`, then we must have some other argument that gets smaller every function call. E.g. // Taking in infinite codata and producing finite data def take(stream: Stream, n: NaturalNum): List[Int] = { n match { // This passes totality checking because m is "smaller" than n, which here // means we had to strip away one level of NaturalNum constructors // hence Successor(m) => Cons(stream.head, take(stream.rest, m)) Zero => EmptyList } } def streamIdentity(stream: Stream): Stream = { // Since we're producing codata, we check for guarded recursion // Passes totality checker because streamIdentity is guarded behind Stream Stream(stream.head, streamIdentity(stream.rest)) } def listIdentity<A>(list: List[A]): List[A] = { list match { case EmptyList => EmptyList // Since we're producing data, we check for structural recursion // Passes totality checker because the recursive call is on a smaller piece of data case Cons(x, rest) => Cons(x, listIdentity(rest)) } } // Can't blindly produce finite data from an infinite piece of codata! def nontotalStreamToList(stream: Stream): List[Int] = { // Looking for structural recursion // Does not pass totality checker because stream.rest is not considered to be smaller than stream since Stream is codata Cons(stream.head, nontotalStreamToList(stream.rest)) } // Can definitely produce infinite codata from finite data though def padOutListWithInfiniteZeroes(initialSegment: List[Int]): Stream = { initialSegment match { case Cons(x, rest) => Stream x (padOutListWithInfiniteZeroes(rest)) case EmptyList => Stream 0 (padOutListWithInfiniteZeroes(initialSegment)) } } Bringing in the notion of codata also gives us some theoretical nicety. How do you express totality for a program that must run forever, e.g. a server? You say that the IO type a la Haskell is codata and that's that! Then you know that `main` having the `IO` type means that it can potentially run forever, but it will always generate a finite amount of stuff on every codata "iteration" and therefore is productive and is not just spinning its wheels in a pointless infinite loop that does nothing.