Lambda the Ultimate

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.

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

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

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)

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

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.

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

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.

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

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.

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

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

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.

If the I/O computation wrapped in unsafePerformIO performs side effects, then the relative order in which those side effects take place (relative to the main I/O trunk, or other calls to unsafePerformIO) is indeterminate.

...whereas C programmers can expect to control the order of all their IO actions.

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.

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

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)

(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 arbitrary functions - you don't get to modify them to do the logging.

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.

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!