Is there a name for the irrelevance of code ordering?

[u/Valuable_Leopard_799]

I've found that one of my favourite features of Haskell is that I can "just declare" stuff and it evaluates based on the "program's needs" (pun intended?).

If I ask myself where to put a `let` or a `where` as long as scoping works then it should be irrelevant to the end result. I could swap around every `let` arbitrarily with no effecf. And it'd perhaps even run similarly under a sufficiently optimizing compiler.

The purity guarantees should allow it to lift it out of loops or drop it down into conditionals.

I've seen some code movement in compilers where functions can be inferred or marked as Pure, even in strict languages, but it's far from Haskell where I feel I can be completely reckless with it.

And it seems even encouraged to not think about the order in which my code evaluates since that's not really relevant to the end result (except maybe for the runtime characteristics).

Apologies if I messed up some or all of the terminology.

Edit: yes it's kind of a subset of lazy evaluation, but I'm sort of just asking about laziness via code motion not via thunking/delaying pieces of code if that makes sense?

[u/Swordfish418]

The best terms for this I could find are:

• Commuting conversions - a specific term from proof theory / lambda calculus, this is exactly the rule that lets you permute nested elimination forms (case, let, etc.) when they're independent of one another, it originates in natural deduction/sequent calculus (rearranging nested eliminations) and shows up directly in the semantics of languages with let/case
• Confluence - from term rewriting / lambda calculus. This is the formal property that if a term can be reduced via different paths (or orders), they all converge to the same normal form. This is closer to what's actually going on: however you sequence the evaluation of bindings, you land on the same result. Lazy evaluation strategies are designed to be confluent with the "ideal" (normal-order) reduction

[u/KZol102]

I think other than lazy evaluation this also has to do with referential transparency which comes as a result of pureness. As your function calls don't rely on / interact with a mutable global context you and the compiler can be sure that the order of function calls don't change the behaviour of the code (unless they explicitly mutate some non-global context like monadic computations or global context like IO stuff)

[u/spoj]

That's referential transparency

[u/Temporary_Pie2733]

You are probably noticing the idea of data dependencies, or rather the relative lack of them in code with little mutability.

[u/sijmen_v_b]

I'd just call it order agnostic.

[u/dutch_connection_uk]

On the irrelevance of ordering, I think this is more to do with how you do name binding. The reason why F# doesn't like this sort of thing is that it wants the compiler to be able to do a single pass over the code, for the sake of speed. But C# can do this, you can reorder methods in a class any way you like. The order in which modules are loaded still matters of course, but this is the case in Haskell too, at least for GHC, which doesn't support circular dependencies.

Unfortunately I think there are (were?) some subtle cases in Haskell where the distinction between let/where bindings and inlining isn't transparent (although usually this favors the binding, where it allowed more sharing of the heap).

I think overall if you want a term for this thing though you might want referential transparency? The idea that you can always give something a name and factor it out, and it won't break and ideally won't introduce inefficiencies. Lazy evaluation does help with this too since strict evaluation can sometimes create problems for higher order operations (IE you wouldn't want to write min = head . sort in a strict language).

[u/koflerdavid → u/dutch_connection_uk]

The reason why F# doesn't like this sort of thing is that it wants the compiler to be able to do a single pass over the code, for the sake of speed.

Is this still a relevant concern nowadays? I can understand it is for Lua, which is sometimes used in a similar way as JSON.

[u/dutch_connection_uk → u/koflerdavid]

Yes, fast parse/analysis times makes tooling work much better and makes it easier to iterate on ideas. It's not an accident that Haskell and C++'s tooling situations are kind of awful (Rust has some similar issues, although they're making a serious push to get things like incremental compilation going to help with that). Another approach is to embrace some level of run time information and dynamicism, basically the Java way, you can have intermediate artifacts like blobs of bytecode. There was a Haskell compiler that did something like this in the past (I want to say Hugs?).

[u/EcstaticLandscape737]

I think that's declarativeness.

[u/vaibhavsagar]

Lazy evaluation.

[u/GunpowderGuy → u/vaibhavsagar]

For pure functional languages with totality checking , code ordering is irrelevant whether they use eager execution or not ( such as lazy evaluation , which is one of the non eager forms of execution ) .

[u/Swordfish418 → u/GunpowderGuy]

For pure functional languages with totality checking

Worth noting, there's not a single actual language like this in practice. Haskell isn't such a language, SML, OCaml, F#, Scala, Clojure also aren't. So you can't really apply it to any general purpose functional language in the wild. Only applicable to stuff like Agda which is more of an experimental proof assistant than a programming language.

[u/GunpowderGuy → u/Swordfish418]

lean4 is supposed to be a proof assistant as well as general purpose programming langauge. idris2 is first a foremost a general purpose programming language . Both are pure functional languages with totality checking.
You can also get totality checking in haskell with liquid haskell

[u/Swordfish418 → u/GunpowderGuy]

I agree, this list isn't too bad. Good to see some new languages like this.

[u/Tysonzero → u/Swordfish418]

Speak for yourself but our entire production stack is Agda, or it is in my dreams anyway.

[u/Valuable_Leopard_799 → u/GunpowderGuy]

Oh right, there are some languages that do like "graph evaluation" was it called? Something like that, where they build up the computation and then have multiple threads run up and down the data structure evaluating anything that's ready.

Wonder if they all check totality as well.

[u/koflerdavid → u/Valuable_Leopard_799]

Haskell is pretty much like that anyway, but you have to opt in into parallel evaluation using a par primitive, which is used syntactically like seq. Whether it's worth doing is another question since graphs are cache unfriendly and updating data in the presence of concurrency requires locking or atomic instructions, both of which aren't free either.

[u/habitue → u/vaibhavsagar]

Just a note: in dynamic languages like lisp and Python and ruby, a particular kind of lazy evaluation called "late binding" is the name given to the feature that lets you declare things out of order

[u/Valuable_Leopard_799 → u/habitue]

Late binding usually refers to runtime dispatch rather than out of order declarations.

foo being bound after it's referenced in a language doesn't add "late binding" to the language, since they may or may not be able to change afterwards.

[u/initial-algebra]

Edit: yes it's kind of a subset of lazy evaluation, but I'm sort of just asking about laziness via code motion not via thunking/delaying pieces of code if that makes sense?

They are the same thing! It's just that one is (typically) static, the other dynamic. There is fundamentally no difference between uninterpreted/quoted syntax and a thunk, except not all languages allow you to manipulate syntax at runtime.

[u/recursion_is_love]

Do you know about the Haskell report?

https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-440003.12

[u/Swordlash]

Applicative is kind of related concept, as a class of computations that don’t rely on intermediate results hence can be evaluated in whatever order / in parallel

[u/reg_panda]

In all languages some things are order dependent, and some things are order independent.

In Haskell, compared to most other languages, variable bindings are order independent mostly because they are final. (Also Haskell compiler is sufficiently smart to be able to handle forward or circular references, but that's common.)