4 ms·

Tee hee, Haskell doesn't have tail recursion (e.g. foldl takes linear space), and structural recursion in Haskell isn't guaranteed to terminate (e.g. if you're

Tee hee, Haskell doesn't have tail recursion (e.g. foldl takes linear space), and structural recursion in Haskell isn't guaranteed to terminate (e.g. if you're given an infinite list). If I were in charge of developing a safety critical system, and someone came to me with a proposal to write it in Haskell, I'd be very skeptical.

wyager 10y ago
??? Haskell absolutely has tail recursion; foldl just evaluates non-strictly and therefore can leave thunks in memory. This is fine for e.g. reversing a cons-list. Regardless, it is tail recursive (and uses constant stack space). foldl' is also tail recursive and has strict semantics. Structural recursion can't be guaranteed to terminate in any language that supports codata unless you have some sort of totality checker (e.g. via a monotonically structurally decreasing requirement imposed at the type or value level). I don't think any mainstream language supports this out of the box. Liquid Haskell does offer this, though. I agree that standard Haskell is inappropriate for safety critical software, but only because it allows dynamic allocation. Any program using dynamic allocation is probably unsuitable for safety critical software. Now, a terminating and fixed-memory subset of Haskell a la Clash would be interesting for safety critical software...
- cousin_it 10y ago
  The point of tail recursion is using constant space, not constant stack space (does Haskell even have a stack?) Anyways, the Haskell spec allows foldl' to use linear space just like its lazier counterparts. The fact that it uses constant space is an implementation detail of GHC. Reference: https://github.com/quchen/articles/blob/master/fbut.md#seq-does-not-specify-an-evaluation-order https://github.com/quchen/articles/blob/master/fbut.md#seq-d... Structural recursion always terminates in SML. Supporting infinite/cyclic values in algebraic data types is a misfeature, and they are trivial to rule out without using a totality checker. Heck, I can implement a guaranteed finite linked list in Java :-) I think something like MLKit would be a more promising start for implementing a safety critical system. Tail and structural recursion actually work there, and it statically replaces most uses of GC with region inference. Though it's still a very long shot, I'd prefer something more proven.
  - wyager 10y ago
    Tail recursion can't use constant space if it's strictly generating another data structure of the same size. That doesn't even make sense. Interesting fact about foldl'. Regardless, in practice it is strict and tail recursive. As I mentioned earlier, this does not mean the same thing as constant space unless the reduction function returns a fixed size result. Yes, you can guarantee that a linked list in Java is finite because Java does not support codata. Haskell's tail call recursion is also often optimized to be allocation-free, unless, again, it is generating some data structure.
    - eru 10y ago
      > Yes, you can guarantee that a linked list in Java is finite because Java does not support codata. What about another thread running that keeps generating pieces to the end of the linked list? (No problem, with mutation.)
      - cousin_it 10y ago
        To prevent these and similar "what abouts", here's an implementation of a guaranteed finite linked list in Java. class LinkedList<T> { public final T value; public final LinkedList<T> next; public LinkedList(T value, LinkedList<T> next) { this.value = value; this.next = next; } } Here's how you construct it: LinkedList<String> myList = new LinkedList("Hello", new LinkedList("World", null)); Here's how you iterate over it in constant space: while (myList != null) { System.out.println(myList.value); myList = myList.next; }
  - tome 10y ago
    > does Haskell even have a stack? Yes
    - wyager 10y ago
      While this is true, the contents of the STG stack aren't necessarily obviously related to the conceptual "call stack", right?
- eru 10y ago
  > Now, a terminating and fixed-memory subset of Haskell a la Clash would be interesting for safety critical software... Definitely. I something think Haskell should treat non-terminating code the same way they treat IO: only allow it in portions of the code-base that are tagged somehow. If there's something that doesn't cause a side-effect, but the compiler doesn't know that, you can tell it with unsafePerformIO. If there's something that terminates, but the compiler doesn't know, (eg calculating the hailstone sequence for a number), there could also be a suitable escape hatch to be used with care.

wyager 10y ago

??? Haskell absolutely has tail recursion; foldl just evaluates non-strictly and therefore can leave thunks in memory. This is fine for e.g. reversing a cons-list. Regardless, it is tail recursive (and uses constant stack space). foldl' is also tail recursive and has strict semantics. Structural recursion can't be guaranteed to terminate in any language that supports codata unless you have some sort of totality checker (e.g. via a monotonically structurally decreasing requirement imposed at the type or value level). I don't think any mainstream language supports this out of the box. Liquid Haskell does offer this, though. I agree that standard Haskell is inappropriate for safety critical software, but only because it allows dynamic allocation. Any program using dynamic allocation is probably unsuitable for safety critical software. Now, a terminating and fixed-memory subset of Haskell a la Clash would be interesting for safety critical software...

cousin_it 10y ago
The point of tail recursion is using constant space, not constant stack space (does Haskell even have a stack?) Anyways, the Haskell spec allows foldl' to use linear space just like its lazier counterparts. The fact that it uses constant space is an implementation detail of GHC. Reference: https://github.com/quchen/articles/blob/master/fbut.md#seq-does-not-specify-an-evaluation-order https://github.com/quchen/articles/blob/master/fbut.md#seq-d... Structural recursion always terminates in SML. Supporting infinite/cyclic values in algebraic data types is a misfeature, and they are trivial to rule out without using a totality checker. Heck, I can implement a guaranteed finite linked list in Java :-) I think something like MLKit would be a more promising start for implementing a safety critical system. Tail and structural recursion actually work there, and it statically replaces most uses of GC with region inference. Though it's still a very long shot, I'd prefer something more proven.
- wyager 10y ago
  Tail recursion can't use constant space if it's strictly generating another data structure of the same size. That doesn't even make sense. Interesting fact about foldl'. Regardless, in practice it is strict and tail recursive. As I mentioned earlier, this does not mean the same thing as constant space unless the reduction function returns a fixed size result. Yes, you can guarantee that a linked list in Java is finite because Java does not support codata. Haskell's tail call recursion is also often optimized to be allocation-free, unless, again, it is generating some data structure.
  - eru 10y ago
    > Yes, you can guarantee that a linked list in Java is finite because Java does not support codata. What about another thread running that keeps generating pieces to the end of the linked list? (No problem, with mutation.)
    - cousin_it 10y ago
      To prevent these and similar "what abouts", here's an implementation of a guaranteed finite linked list in Java. class LinkedList<T> { public final T value; public final LinkedList<T> next; public LinkedList(T value, LinkedList<T> next) { this.value = value; this.next = next; } } Here's how you construct it: LinkedList<String> myList = new LinkedList("Hello", new LinkedList("World", null)); Here's how you iterate over it in constant space: while (myList != null) { System.out.println(myList.value); myList = myList.next; }
- tome 10y ago
  > does Haskell even have a stack? Yes
  - wyager 10y ago
    While this is true, the contents of the STG stack aren't necessarily obviously related to the conceptual "call stack", right?
eru 10y ago
> Now, a terminating and fixed-memory subset of Haskell a la Clash would be interesting for safety critical software... Definitely. I something think Haskell should treat non-terminating code the same way they treat IO: only allow it in portions of the code-base that are tagged somehow. If there's something that doesn't cause a side-effect, but the compiler doesn't know that, you can tell it with unsafePerformIO. If there's something that terminates, but the compiler doesn't know, (eg calculating the hailstone sequence for a number), there could also be a suitable escape hatch to be used with care.