When Is A Functional Program Not A Functional Program?

When Is A Functional Program Not A Functional Program?, John Longley. ICFP 1999.

In an impure functional language, there are programs whose behavior is completely functional (in that they behave extensionally on inputs) but the functions they compute cannot be written in the purely functional fragment of the language. That is, the class of programs with functional behavior is more expressive than the usual class of pure functional programs. In this paper we introduce this extended class of "functional" programs by means of examples in Standard ML, and explore what they might have to offer to programmers and language implementors.

After reviewing some theoretical background, we present some examples of functions of the above kind, and discuss how they may be implemented. We then consider two possible programming applications for these functions: the implementation of a search algorithm, and an algorithm for exact real-number integration. We discuss the advantages and limitations of this style of programming relative to other approaches. We also consider the increased scope for compiler optimizations that these functions would offer.

I like this paper because it shows how some of the most abstract bits of formal logic (realizability models of higher order logic) suggest actual programs you can write.

As a barely-related aside, even a brief look into this realizability stuff also taught me a good deal of humility -- for example, it seems that at higher types, what you can represent mathematically depends on the specific notion of computation you're using. So the mathematical consequences of the Church-Turing thesis are rather more subtle than we might initially expect. (Andrej Bauer discusses a related point in more detail in this blog post.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Compare with Escardo

It's interesting to compare with Escardo's work on fast exhaustive search. Longley points out that we can sum values of a function quickly if we can detect whether or not the function depends on its arguments. Escardo does a similar stunt where he's able to *quickly* search the space of binary streams by implicitly testing whether or not a function depends on part of its argument, and even better, immediately jumping to that part of the argument on which it depends. Amazingly, he does this in a purely functional way. Unfortunately it can't be adapted to the sum of series case, but it does show that it's not trivial to tell what you can and can't do in a purely functional manner.

You can 'do' anything

You can 'do' anything in a purely functional way if you're willing to interpret 'do' liberally enough. Trivially you have that they're both just Turing complete. But more to the point it seems like you should be able to mimic everything done in this paper by systematically programming in a monadic style wherever you want the sort-of-introspection presented in the paper. IMO this is another point for why you might want ubiquitous Monad integration in a language.

That would be an encoding

Unless you use Haskellers' best friend, unsafePerformIO, that would change the interfaces (types) of the functions involved.

That bears repeating

You can indeed 'do' anything, but some of what you wish to do will leak into your types (unless you cheat). So Monads (or CPS) are solutions, but that will change your types.
The original point was that, at certain types, there are operations that seem rather sensible but turn out to be impossible. At other types, in which you can inject your previous type, one gets more power. [I am sure the Yoneda Lemma has a lot to say about that.]

Sensible?

Consider the following:

foo f = 1
foo' f = if f 0 == 0 then 1 else 1

If I understand correctly, the "modulus" of foo and foo' are different despite the fact that we probably want them to denote the same value. I think the ability to introspect functions in this way really needs to be part of the type. (Edit: I really mean part of the value - this is about purity, not types)

They don't denote the same value


Good point ;)

(Edit: This does still illustrate a problem you'd have if you tried to do this in a language without _|_, though)

Actually

Even in a non-total language, I think it can be useful to view _|_ as aberrant program behavior so that a compiler is always allowed to optimize foo' to foo (or optimize away multiplication by 0, e.g.). So I think this is still a reasonable argument against allowing this kind of thing.

substitutability

His first example of a function that can't be implemented purely, namely F in section 0, raises an interesting point. In Haskell, if the compiler was able to prove that a function f:(()->()) -> () terminates, it is safe to substitute top for f, because the two are indistinguishable. In impure ML, this optimization could change program behavior.

Safe?

If you have a function f :: (() -> ()) -> (), that terminates, but performs (terminating) IO using unsafePerformIO (e.g. writes a constant to an IORef), then is the substitution safe or merely a documented case of undefined or implementation defined behavior?

From the docs for

From the docs for unsafePerformIO:

"For this to be safe, the IO computation should be free of side effects and independent of its environment."

Any guidelines on making other uses work are implementation-specific.

When a Haskell function is labelled unsafe, it means it - not just that you could corrupt the RTS, but that it'll potentially mess up the language's semantics before it gets anywhere near run-time. They're intended to be used correspondingly infrequently - I forget if I've ever actually used unsafePerformIO at all rather than considered it in a couple of unusual contexts.

So, it is just like C.

So, it is just like C.

It is not much like C at all

No. There are many circumstances in which a compliant C implementation could decide you wanted your program to play a nice game of Rogue (to pick an example that's actually been seen in the wild) or to make monkeys fly out of your backside (for one that hasn't, I hope). A Haskell implementation can't just do whatever it likes with unsafePerformIO - it has to treat the IO code on the inside as if it were pure code and perform the action whenever it is evaluated. This means that any rectal monkeys are significantly the fault of the IO action wrapped by unsafePerformIO, and at that point you should be more concerned by the fact an implementation could legitimately evaluate it more than once!

If I'm given a trustworthy library set, I would be quite willing to use a Haskell implementation created by a deity with a nasty sense of humour. I wouldn't touch the same deity's C implementation from anywhere less safe than another universe.

Lovely rhetoric, but still exactly the same

In both cases you have a language that offers constructs whose behavior is not defined in all cases. IOW, the language spec has holes. In both cases, responsibility for avoiding the holes is shifted to the programmer, via legalese, while the compiler is allowed to pretend that the holes don't exist.

implementation could decide you wanted your program to [...] make monkeys fly out of your backside (for one that hasn't, I hope)

I see that happening all the time. :-)

You have an awfully funny notion of exactness

In Haskell's case the behaviour is defined perfectly clearly - but the evaluation order is no more defined here than anywhere else, that being part of the language's raison d'etre. Behaviour that is defined to include non-determinism is not the same as undefined behaviour. The compiler isn't "allowed to pretend it doesn't exist", it's obliged to!

There is, yes, an opportunity to tell the compiler "just trust me". But it can be grepped for without producing a pile of false positives, isn't necessary for many techniques (indeed, is never, ever truly necessary if you're allowed to refactor in a type-altering manner) and has behaviour that it is entirely possible to reason about in all circumstances. In this regard it's almost, but not quite, entirely unlike C's unsafe constructs, and I am not aware of a single language with an FFI (the only standard in which unsafePerformIO is given, it's not part of Haskell98 per se) that is safer.

re: Entirely possible to reason about in all circumstances

[Haskell/unsafePerformIO] has behaviour that it is entirely possible to reason about in all circumstances

How do you reason about the cases where unsafePerformIO is known to be type unsafe, such as in the example given here?

In Haskell's case the behaviour is defined perfectly clearly - but the evaluation order is no more defined here than anywhere else, that being part of the language's raison d'etre.

The type unsafe example given on the page I pointed to has nothing to do with evaluation order. It also doesn't interface with any foreign language.

Continued:

I am not aware of a single language with an FFI [...] that is safer.

I am. I know that is possible to have a language, with an FFI, in which it is impossible to write a coerce function with the (polymorphic) type a -> b that could potentially return a value.

Fair catch

Fair enough, I forgot about the need for a value restriction.

That said, it's a bit difficult to prevent someone using an FFI to call an external coerce - the design tradeoff was between preventing it happening outside the IO monad and allowing foreign code to be considered pure. There'll be an awful lot of languages you can write coerce in so long as you reimport it via the FFI.

It's still an improvement on C where equivalently unsafe code is endemic and in practice modules can't easily be shown free of risk. I have a high level of confidence that my own code is still monkey-free.

more than that

I have a high level of confidence that my own code is still monkey-free.

More than that: you can have a high level of confidence that anyone's code is monkey-free, provided they don't use unsafePerformIO. Granted, the presence of unsafePerformIO in the language could be considered a security risk, but types aren't necessarily for security. There is a wide, wide chasm of difference between the level of safety in Haskell and the level of safety in C. You'd be hard-pressed to write useful C without pointers. You can write useful Haskell without unsafePerformIO.

(And if you are talking about security, Vesa, isn't the existence of an FFI generally just as much of a security risk, if not more, as unsafePerformIO?)

Monomorphic types

That said, it's a bit difficult to prevent someone using an FFI to call an external coerce - the design tradeoff was between preventing it happening outside the IO monad and allowing foreign code to be considered pure. There'll be an awful lot of languages you can write coerce in so long as you reimport it via the FFI.

One way to prevent that is to only allow monomorphic types in the FFI (i.e. import (and export) only with monomorphic types). For interfacing with a low level language like C, monomorphic types are enough.

Neophyte question about "functional"

The paper comments on the Modulus and says that if the return value helps you figure out the order of operations within the function, then it is not functional: "...since it would allow us to distinguish between different implementations of the same function G".

But I guess I thought it was G itself that was recording calls to h, which means if G1 does things in a different order than G2, and thus returns different lists, then that is not un-functional. I mean, if I have Foo() and Bar() that return different lists, there's nothing wrong with that.

I guess the crux is that the paper is saying Modulus is what generates h, rather than G itself? Even so, if I have a function Foo( Bar() ) where Bar appends values to a reference, and I change to Foo2( Bar() ), I don't see how one can claim that Foo-with-signature-X must == Foo2-with-signature-X. Signatures don't define equality between functions. As long as Foo and Foo2 return the same output for the same input... [Edit: individually, not when comparing them side-by-side.]

(Sorry for what is probably extreme cluelessness.)

[drat, this should have gone in with the discussion above about mod.]

G is some function invoking

G is some function invoking one of its parameters h (which is a function int -> int). To compute the Modulus of G applied to h (sharing the name for argument / parameter) we prepare a function h' which calls h and logs the parameter and result. For this Modulus to be a well defined function of its parameter and not dependent on choice of implementation of G, it must return a value that doesn't depend on the order of (parameter, h value) pairs. So for example we could sort the list before returning it.

Many thanks for the note

Unfortunately, I think I'm too thick to get some crux of the nut & should give up before wasting more bandwidth :-} I think what doesn't click for me is probably that "h' must return things sorted" iff "M is well defined".

[Edit: So re-reading the paper, it isn't like G(h) thence G(h'(h)), with h' sorta being M, it is more like M(G,h) which runs G(h'(h)). But I am still clueless about what is wrong with putting in G2 and getting a different output, since you've just changed one of the inputs. Like, if you give fold a different lambda to use you can get different results, no? Is that similar / just as 'bad'?]

h' doesn't return things

h' doesn't return things sorted, Mod does. h' logs a single call to h. Mod runs G with h' passed in instead of h, so that it can gather up all of the places where G calls its parameter. Mod has to sort the list of calls so that it gives the exact same answer for another function G' which has the same observable behavior as G, but which makes its calls to h in a different order.

Replying to your edit

Your first sentence looks maybe right. The answer to your second question is, I think, that there are many function expressions which we want to consider identical functions. Things like f x y = x + y and f' x y = y + x. In a pure language one of the guarantees you have is that you can pass f' anywhere you can pass f and get the same result. In a language where x and y can have side effects when evaluated, you no longer have that. The point of this paper is constructing some functions which respect this substitution property but which aren't constructible in a pure language. (We want Mod to give the same result not for any G and G', but for any G and G' which are observably identical)

might be starting to clue in, i can hope...

(many thanks for your posts)

so is it because it is done by references? if the "log" was generated with return values instead of side-effects, would that change/improve/simplify things? not that we want to do that, i'm just asking to see if the references/using-side-effects is a key point.

G and h are supposed to be

G and h are supposed to be arbitrary functions - you don't get to modify them to do the logging.

Church-Turing thesis

Actually I don't think this kind of research tells us much about the Church-Turing thesis. IMO the most natural notion of computability deals with partial functions that take and return scalar values. If you want to pass one function to another, bite the bullet and pass the Godel number.

In that setting, the main example from the paper vanishes in a puff of smoke, because there are many more functions ((unit->unit)->unit) than top, mid, bot. And the other famous example of computability at higher types, the "parallel or" function, becomes trivial because computable functions (just like actual computers) have no trouble with single-stepping two programs at once.

Of course if you restrict the notion of computability, e.g. by enforcing totality or passing functions as black boxes, you'll get a whole zoo of other complicated notions. But none of them will be as important as the one true notion :-)

Computability at higher types

Of course if you restrict the notion of computability, e.g. by enforcing totality or passing functions as black boxes, you'll get a whole zoo of other complicated notions.

Indeed, the fact that there is no single notion of higher-type computability is well-known in the academic literature. I think that the best reference to date is John Longley's Notions of Computability at Higher Types.

But none of them will be as important as the one true notion :-)

Can you justify that statement? Most programming languages where programs can abstract over functions (e.g., ML or C) do not work by passing source code around. And their reflection facilities are either non-existant or too weak to recover the body of a function argument. Thus Gödel numbers do not shed light on their properties.

whither function bodies

I am always surprised when some JavaScript logging shows me the actualy function body text! I wish that were actually the standard thing for programming languages these days. At least if the debug flag is used when compiling!