|
|
|
|
|
by cousin_it
3629 days 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-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. |
|
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.