[kazinator]

Problem is, a decision has to be made somewhere about which function to pass into that "if-free" block of code. The if-like decision has just moved elsewhere. That is a win if it reduces duplication: if a lambda can be decided upon and then used in several places, that's better than making the same Boolean decision in those several places.

Programs that are full of function indirection aren't necessarily easier to understand than ones which are full of boolean conditions and if.

The call graph is harder to trace. What does this call? Oh, it calls something passed in as an argument. Now you have to know what calls here if you want to know what is called from here.

A few days ago, there was this HN submission: https://news.ycombinator.com/item?id=12092107 "The Power of Ten – Rules for Developing Safety Critical Code"

One of the rules is: no function pointers. Rationale: Function pointers, similarly, can seriously restrict the types of checks that can be performed by static analyzers and should only be used if there is a strong justification for their use, and ideally alternate means are provided to assist tool-based checkers determine flow of control and function call hierarchies. For instance, if function pointers are used, it can become impossible for a tool to prove absence of recursion, so alternate guarantees would have to be provided to make up for this loss in analytical capabilities.

[eru]

In a language like Haskell you wouldn't want to prove the absence of recursion, but that all recursions in the program fit into a handful of patterns. (Eg 'structural-recursion' or 'tail-recursion'.)

Some type systems are strong enough to put that kind of analysis / constraints directly into the language. (Haskell might already be strong enough with GADTs and other language extensions enabled.)

In any case, the Addendum at the end of the blog post provide a different perspective on the problem you mentioned.

[cousin_it]

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]

??? 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]

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.

[wyager]

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]

> 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.)

[kazinator]

The point of tail recursion is using constant space for the environment and control flow meta info, not constant space absolutely.

[tome]

> does Haskell even have a stack?

Yes

[wyager]

While this is true, the contents of the STG stack aren't necessarily obviously related to the conceptual "call stack", right?

[eru]

> 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.

[kazinator]

That coding guideline simply rejects all recursion, even cases that are correct by inspection, or by easy proof.

[eru]

Interesting. I assume they allow the special cases of tail recursion introduced by 'while', 'for' and similar constructs?

[kazinator]

goto is banned; loops must be statically bounded.

[eru]

Thanks for the information!

[bunderbunder]

All valid points.

If you're going to do this sort of thing with much success, you really need to have a language with a fairly powerful type system. If function pointers are your only option for higher-order programming, I wouldn't even try. First class functions or interface polymorphism help, but I'd also want to have a language that makes it relatively easy to create (and enforce) types so that your extension points don't end up being overly generic.

[thaumasiotes]

What distinction are you drawing between "first-class functions" and "function pointers"?

[bunderbunder]

About the same distinction as I'd draw between an integer and a pointer to an integer.

[kazinator]

Both function pointers and "first class functions" refer to function indirection.

In its treatment of expressions, C doesn't draw the distinction between function and pointer to function. When you call printf("foo\n"), the printf part is a primary expression which designates a function, and evaluates to a function pointer. That pointer is then dereferenced by the postfix ().

The main difference between a "first class" function and a function pointer is that a first class function carries an environment, which allows the body of the function to make references to lexically scoped names outside of the function. A function pointer carries a reference to the code only.

[moogleii]

>The main difference between a "first class" function and a function pointer is that a first class function carries an environment

Isn't that specifically a closure? I think first class functions have a more general definition.