Lambda the Ultimate

Why bother to allow that sort of mutability? What does it buy you? The important and useful sort of mutability isn't restricted to such local scope.

One reason to disallow mutation in the local case is that it introduces potential problems with refactoring, since mutation creates order dependencies.

So I have to disagree with slide 32. I'm not annoyed, it's just wrong. ;)

[[Why bother to allow that sort of mutability? What does it buy you?]]

The true question should be: why should such functions be restricted?

These functions are pure (their outputs depends only on their inputs) and I don't think that 'potential problems with refactoring' is a strong argument to enforce what I consider an artificial restriction.

One annoying limitation about these 'pure' functions is that you can't log their usage because writing to a file is impure: IMHO while in the strictest sense this is true, it should be possible to have a dedicated log function, after all if the programmer is warned before that the compiler is free to reorder/memoize these pure function why not?
In some case, it may be interesting to log them to detail the cpu usage of your program for example.

Which language or system impose such a strict restriction? How do programmers work around it?

My plan is to allow it but I would be interested in looking at the alternatives. In my case, the language would use message passing and access to the log will be managed as a capability.

To clarify: The issue is only with pure functions, as from a mathematical point of view a 'pure' function cannot be logged because logging is a side-effect..

In my mind, as long as the programmer understand that the compiler can do many tricks with pure functions, this shouldn't be a limitation.

Hypothetically, while the pure function can't be logged its evaluation (if done impurely) could be - just as it will alter the physical state of your computer. This is essentially a variant of an idea Derek Elkins and I both keep meaning to play with - a pure functional language with a Reflection monad (possibly doubling as IO), from which all the traditional lispy things can be done. Naturally the Reflection monad would allow you to completely mess with a function's semantics - that's what it's for! But the unmodified function still has pure semantics, and useful instrumented evaluators can be specified in terms of those semantics. Yes, it's still the preprocessor, but it's a long long way from string-based macros in engineering capability!

The issue is only with pure functions, as from a mathematical point of view a 'pure' function cannot be logged because logging is a side-effect.

I don't see the utility of this viewpoint. It strikes me that the essence of purity is that return values depend only on arguments. What is an allowable side-effect is a question of perspective: function evaluation on a mechanical computer always has the side-effect of generating heat, for example, but we don't care about that. I think we are also likely not to care about logging. Why can't we express that?

I think we are also likely not to care about logging. Why can't we express that?

You can in e.g. Haskell (with common extensions) but it opens a can of worms.

The issue is one of ordering and reordering. A pure function can be reordered pretty arbitrarily or even dropped entirely as long as the directly expressed data dependencies are met. A side effecting procedure cannot be reordered without breaking the programmer's intent - printing "hello" before "world" says something different from doing it the other way around.

How can a compiler know the difference between not-that-important logging and vital-to-correctness IO? It can't. The best it can do is allow the programmer to annotate the difference with an equivalent of performUnsafeIO or Debug.Trace functions and hope he/she understands the potential consequences.

A side effecting procedure cannot be reordered without breaking the programmer's intent

This is a bit too strong--it assumes that every order expressed in the syntax is the result of the programmer's intent. But linear syntax means the programmer has no choice but to state things in a particular order, whether that order is part of his intent or not. He ought to have a way to say that.

In fact, I'd say the terminology reinforces your point of view: a "side" effect ought to be one that can be reordered or discarded without consequence. One that cannot ought to be called a "primary" effect. When printf() writes to stdout, that's a primary effect. When log() does, that's a side effect.

But linear syntax means the programmer has no choice but to state things in a particular order,

First, many languages don't have a completely linear syntax. Much of mathematics, spreadsheets, visual languages...

Second

x + y + z = (x + y) + z = x + (y + z) = (y + x) + z

Properties that are true in spite of the fact that the language used has a linear syntax. And what do you do about x * z + x * y? That absolutely requires that operations be done in an order different from the linear order of the syntax. A smart arithmetician might even rewrite it as as x * (y + z).

Linear syntax and intent and order of operations need not be the same thing.

Third,

map f . map g = map (f . g)

Side effects prevent that optimization from being true.

Fourth, at anything larger than about the individual function/procedure/method level even the most imperative of mainstream languages doesn't try to imply too much by linear ordering. If two different functions happen to do some IO while computing something then the order they are called may be very important and may have nothing to do with where the functions are declared linearly in the text and may even have little directly to do with where their calls appear linearly in the text. Thinking about a program as a group of linear text file is a short road to a lot of misunderstanding. No programmer except the rawest newbie thinks that way.

So why is it somehow more natural that programs work differently at the fine grained level than they do at the large grained level?

In fact, I'd say the terminology reinforces your point of view:

It's a point of view based on the fact that "print" declares it takes a string and returns a unit(void) but somehow something else happens "on the side" that has nothing to do with converting a string to unit. Sure that thing that happens on the side is probabably the effect the programmer wanted, but it's still "on the side." And it's still an "effect" that's hard to reason about using the simple logic implied by the equations above. IO1() + IO2() isn't the same thing as IO2() + IO1().

So, look, I use many side effecting languages. It's fine. Not even inherently evil. I just know the price I'm paying for doing so and have no problem calling a spade a spade.

One that cannot ought to be called a "primary" effect. When printf() writes to stdout, that's a primary effect. When log() does, that's a side effect.

That's a fine idea. It's not really what's meant by "side effect" - nobody means that side effect implies "lesser importance." But, hey, I'll join your campaign to change what the world means by the phrase. In the meantime, how does a compiler know the difference and prove that you're using the distinction correctly? I mean, I might call a special "log" function to do my logging, but then again I might want to log to a database or to a network socket or...

Haskell (plus extensions) allows you to make that distinction with no attempt to prove that you're using it right. If it's important you put it in the IO monad. The type system now knows its important and the user of your code knows its important. If it's not important or you think you can prove that your code will be called at the right time you use unsafePerformIO (or cousins) and cross your fingers that you made the right call.

It's a point of view based on the fact that "print" declares it takes a string and returns a unit(void) but somehow something else happens "on the side" that has nothing to do with converting a string to unit.

Right. The output that print does is a primary effect, not a side effect.

It's not really what's meant by "side effect" - nobody means that side effect implies "lesser importance."

It's certainly what I mean, and the word "secondary" appears in the dictionary definition of the term as well.

... your campaign to change what the world means by the phrase ...

Point taken. :-)

how does a compiler know the difference and prove that you're using the distinction correctly?

The compiler knows the difference because you tell it; this is demonstrably the only answer possible. As to the question of the compiler proving you told it the right thing, when does that ever happen?

Giving the programmer the opportunity to more precisely specify his intent is usually regarded as a good thing--except when it comes to I/O. I don't really understand the reaction.

Giving the programmer the opportunity to more precisely specify his intent is usually regarded as a good thing--except when it comes to I/O. I don't really understand the reaction.

The reaction is that the right way to do it in Haskell is actually to build subset-of-IO monads that run from within the IO monad. It's a shame that the standard libs make this such a pain though! The main issue being that there aren't typeclasses for individual (groups of) operations. There's one bolted on for IO in general, though it requires a lift function.

More generally, I'd be pretty perturbed if what I thought was a pure function started trying to log when I used it on a system that didn't even have a device to log to :-) Side effects in your sense shouldn't be ignorable without at least explicitly saying "scratch that, use a null implementation for all those logging functions" or similar. The trick's finding ways to avoid them occupying too much of your attention while you work on everything else.

Haskell, for one. As far as working around it: when really necessary, they cheat. They also rely more heavily on profiling and similar external tools. The "log messages everywhere" approach familiar to Java programmers is not at all common in Haskell.

It should be pointed out that it's very, very rarely necessary: when people (myself included) use Debug.Trace it's in lieu of a debugger - something we now actually have. It'd be cool to have a scriptable debugger though.

For actual logging, the done thing is to use a Writer monad (which still gives you a pure external interface, makes calling pure code trivial and is easy to add logging calls to). Writer's a restriction of State which only allows you to use the internal state to build up a value via a monoidal operation - the list concatenation monoid being the obvious way to log. The downside is that you can't trace evaluation order that way, though it doesn't have to fix it where it wasn't fixed before - even the State monad has a lazy implementation by default now.

While logging everywhere's not all that common, it's got more to do with the size of typical Haskell projects and typical engineering style - we're generally just not writing applications where it's useful enough to be worth the effort, even if we might want to log the thin IO spine of an app or something like that. I imagine that's an attitude that would change if we were writing more of the sorts of applications Java is commonly used for, and most certainly if such logs became a part of application requirements!

Thankfully, the usual Haskeller trick of using minimally impure sublanguages to write code that's provably pure works wonders - the thing about the fallacy of the preprocessor is that it still doesn't invalidate properties that hold by virtue of being written in the target language at all. That, and when you define one language in terms of another it's much easier to retain desirable properties. Throw in the ability to both compose languages and compose programs across multiple languages and you have an extremely powerful combination - one which even starts to resemble OO in some interesting ways.

Haskell doesn't allow any mutable variables, even local ones.
But to say just this, while true, is unjust because for some years now, Haskell has proposed a Monad "ST" which allows to use local vars (except we call them refs here, like some other functional languages) or local mutable structures (like mutable arrays) and use the type system to ensure that you use them in a single threaded fashion and thus the whole computation is pure.

Really impure operations are restrained to the IO monad, and you can cheat and "purify" an IO action explicitly, but in this case you must prove that this doesn't affect the purity of the computation yourself instead of letting the type system do it for you.

(Writing to a log isn't really a pure action but since it normally don't affect the purity, you're allowed to do it, though you may be screwing some optimisations by doing so the semantic of the program will stay correct)

You could say that Haskell philosophy is the opposite of D here : the default in Haskell is pure ("safe"), while in D it is impure ("unsafe") but both allows you to separe the two types of computation and communicate between them which I found is a real progress.

Haskell will have linear types then? I think that eventually it is unavoidable, because side effects is what programming is about (i.e. to change the "world" in a meaningful way).

Linear types are like tuples right?
I don't think it is necessary to make them mutable, you can get away with using an 'altered' copy -- a copy with a few fields changed. Of course the compiler can optimise the altering copy operation into an in-place change where appropriate (at least that is my hope for dodo).

It's far from unavoidable, and really IO is way down the list of good reasons to do it. The IO monad is plenty adequate, and plays well with a style of programming that does a good job of handling effects that aren't state-like. To put it another way, you'll want the monad for error-handling anyway!

Linear types would be far more useful for issues like resource-handling and using mutability as an optimisation of pure algorithms. They just don't make a good solution to the effect problem in general.

The problem with monads is that they neither compose well nor scale well. The IO monad is fine for diagnostic output, but it's completely inadequate for a large-scale state machine program such as a kernel. Hmm. That could be argued, but the jury is still out, and House is not a counter-example.

monad transformers do compose and scale quite well -- at least I've found that to be the case in my dabblings into Haskell. (I'm assuming you mean "scale" in the non-performance related sense here.)

Yes, they're slightly "heavier" than your standard monads, but I believe there's work underway to fix this -- e.g. MonadLib and IIRC the GHC people are adding some automatic instance derivation support which will reduce the amount of boilerplate needed.

EDIT: s/derviations/derivation support/

For me, monads and linear types are one and the same: they "linearize" computations over variables, i.e. instead of the data be applied to the computations, the computations are applied to the data, in a linear fashion.

Could you please elaborate why linear types do not make a good solution to the effect problem?

Fundamentally, monads just aren't about linearisation - not in the sense you're using the word. They provide something a bit like an ordering, but that doesn't have to be a straight evaluation sequence at all. Additionally, monads also allow you to do things with control flow - the classic examples are the Maybe and Either monads commonly used in place of exceptions and the list monad used to provide non-determinism. Control flow effects are every bit as important as mutability!

Linear types don't offer anything to control flow whatsoever. Try implementing exceptions in terms of them: when you finally succeed, you'll find that the linearity was either irrelevant or a restriction.

A type and single effect system is equivalent to monads however.

To individual monads, yes. This is deceptive though: the ability to nest computations from different monads inside each other, the existance of monad transformers and the ease of writing restricted wrapper monads combine to enable something rather more sophisticated. You're not just working with one type-and-single-effect system across the whole Haskell program.

To put it another way: monads aren't first-class citizens as typically implemented[1], but they are second-class ones on a par with typeclass instances. A type-and-single-effect system in an otherwise ordinary language isn't even a citizen. There's a pretty big difference in power, because the single effect at any given point can be equivalent to the set of effects actually involved.

[1] But if you can encode first-class modules you're off and away!

A type-and-single-effect system in an otherwise ordinary language isn't even a citizen.

I've often wondered why one couldn't declare effects just as one could declare types:

type 'a list = Nil | Cons of 'a
effect take_hd = None | Raise Empty_List
val hd: 'a list -{take_hd}-> 'a

Fundamentally, the language defines a few core effects, and more effects can be constructed from others. That would make them first-class, no?

Linear types don't offer anything to control flow whatsoever.

In the abstract, it would be surprising if this was true, since if one has a type system with linear connectives in it which has cut-elimination, the proof of cut-elimination result should impose an order and tell you what happens before and after the operation corresponding to the linear connective occurs.

In particular, Dale Miller has done some excellent work showing how linear types allow imperative control structures to be modelled, and his former student's PhD thesis discusses how exceptions can be modelled [1].

There's two caveats about this: first, this is not programming languages in which code is written that happens to have a certain linear type, but a logical framework which is used to specify a language with exceptions, where the exception combinators have linear types. The work uses the so-called "internal logic" approach, and so I think that this is something of a distinction without a difference.

Second, the logical framework is Forum, which is based on classical linear logic, whilst linear operators in FP generally use the underpowered intuitionistic linear logic.

[1]: Jawahir Chirimar (1995). A proof-theoretic approach to specification languages (large pdf). PhD thesis, Penn State.

So I have to disagree with slide 32. I'm not annoyed, it's just wrong. ;)

Which sense of "wrong" do you mean here? If you mean, local mutability is a poor design choice, then I can see an argument for that.

If you mean "wrong" as in factually incorrect, then I think you are mistaken.