3 ms·

This is an interesting analysis, in many ways. Take it further down the stack and see that functional semantics are always executed by imperative machines. Su

by taeric 3y ago

This is an interesting analysis, in many ways. Take it further down the stack and see that functional semantics are always executed by imperative machines. Such that we have systems of imperative machines that we build functional abstractions on top of, so that we can have readable imperative code for the users. :D (An amusement being that both the machine and the people prefer imperative, it seems.)

mrkeen 3y ago
> Take it further down the stack and see that functional semantics are always executed by imperative machines And the other way around too. Even your C compiler can't reason about mutability, so it un-imperatives everything first: int foo(int i, int j) { while (i < 10) { j += i; i++; } return j; } That (j += i) line becomes: %9 = load i32, ptr %3, align 4, !dbg !23 // read i into %9 %10 = load i32, ptr %4, align 4, !dbg !25 // read j into %10 %11 = add nsw i32 %10, %9, !dbg !25 // sum %9 and %10 into %11 (i++;) becomes: %12 = load i32, ptr %3, align 4, !dbg !26 // read i into %12 %13 = add nsw i32 %12, 1, !dbg !26 // store i+1 into %13
- taeric 3y ago
  I would consider the compiler to be working in the functional realm, for most of its ideas. Such that I would think it is between the imperative of the machine and the imperative of what a person is thinking? That said, I confess I'm curious how on what the constraints are on this one. I thought there was an increment instruction, specifically. I'm guessing safety and general debugging concerns? And it occurs to me that you are showing an intermediate language in this? Static Single-Assignment (SSA) is definitely in the vein of moving imperative to functional for easy manipulation there. Definitely fun topics to explore here.
- amw-zero 3y ago
  I've come to the conclusion that executability and reasoning are separate axes. If we view everything in terms of languages with interpreters, of course functional semantics must be executed by imperative machines. But to reason about either kind of program, we need functional semantics, because functional programming is the language of pure reasoning. More on the subject: https://concerningquality.com/quality-and-paradigm/ https://concerningquality.com/quality-and-paradigm/
  - taeric 3y ago
    But folks have reasoned about imperative things for a long time, as well? It is certainly easier for many analytics to get into a functional form. But would be a stretch to say it is always easier. Fractals are often my go to example where imperative is easier for many constructs. I view it like coordinate systems. Polar versus Cartesian coordinates can clearly both do the same things. They each have domains where they have advantages. You could argue that time based logic systems are the end goal, maybe? Still feels like throwing babies in bathwater. Edit: for a fun example of reasoning without programming "functional" logic, look up juggling diagrams/notation. Not all logic is symbolic in the same way.
    - amw-zero 3y ago
      This doesn't feel in contrast to what I was saying. You can reason about imperative code, but you have to add things to it to reason about it, most importantly the notion of a memory store. This is because imperative code assumes an underlying CPU + RAM which holds state. It's not that it's easier, it's that imperative code has implicit state.
      - taeric 3y ago
        Fair that I don't intend my question there as a full rebuttal. I do question if functional semantics are fully needed any more so than other tools. In particular, I recall formal methods was more about prepositional logic than it was functional semantics. And yes, you have to add and remove things to any model to really be able to reason about it. Is why engineering dynamics is harder than engineering statics. Things that change are hard. Reducing this to state being the enemy, though, I think is wrong in a lot of functional advocacy. State can be reasoned about without having to boil the ocean, as it were.
- Kamq 3y ago
  I'll admit to not being super great at getting down into the nitty gritty with internals of compilers. Are you talking about some sort of IR? Because if we're talking about the output, mutation definitely happens. Checking on godbolt, there's definitely mutation at least sometimes. Using gcc 13.2, I get the following output. j += i; becomes: movl -4(%rbp), %eax // move i into %eax addl %eax, -8(%rbp) // add i to j With i++ becoming: addl $1, -4(%rbp). // add 1 to i If your example is IR, do you happen to know how it crunches everything "back down" to mutability? Does it just check that the previous value of i and j were never used and use the same registers as an optimization?

by taeric 3y ago

mrkeen 3y ago

> Take it further down the stack and see that functional semantics are always executed by imperative machines And the other way around too. Even your C compiler can't reason about mutability, so it un-imperatives everything first: int foo(int i, int j) { while (i < 10) { j += i; i++; } return j; } That (j += i) line becomes: %9 = load i32, ptr %3, align 4, !dbg !23 // read i into %9 %10 = load i32, ptr %4, align 4, !dbg !25 // read j into %10 %11 = add nsw i32 %10, %9, !dbg !25 // sum %9 and %10 into %11 (i++;) becomes: %12 = load i32, ptr %3, align 4, !dbg !26 // read i into %12 %13 = add nsw i32 %12, 1, !dbg !26 // store i+1 into %13

taeric 3y ago
I would consider the compiler to be working in the functional realm, for most of its ideas. Such that I would think it is between the imperative of the machine and the imperative of what a person is thinking? That said, I confess I'm curious how on what the constraints are on this one. I thought there was an increment instruction, specifically. I'm guessing safety and general debugging concerns? And it occurs to me that you are showing an intermediate language in this? Static Single-Assignment (SSA) is definitely in the vein of moving imperative to functional for easy manipulation there. Definitely fun topics to explore here.
amw-zero 3y ago
I've come to the conclusion that executability and reasoning are separate axes. If we view everything in terms of languages with interpreters, of course functional semantics must be executed by imperative machines. But to reason about either kind of program, we need functional semantics, because functional programming is the language of pure reasoning. More on the subject: https://concerningquality.com/quality-and-paradigm/ https://concerningquality.com/quality-and-paradigm/
- taeric 3y ago
  But folks have reasoned about imperative things for a long time, as well? It is certainly easier for many analytics to get into a functional form. But would be a stretch to say it is always easier. Fractals are often my go to example where imperative is easier for many constructs. I view it like coordinate systems. Polar versus Cartesian coordinates can clearly both do the same things. They each have domains where they have advantages. You could argue that time based logic systems are the end goal, maybe? Still feels like throwing babies in bathwater. Edit: for a fun example of reasoning without programming "functional" logic, look up juggling diagrams/notation. Not all logic is symbolic in the same way.
  - amw-zero 3y ago
    This doesn't feel in contrast to what I was saying. You can reason about imperative code, but you have to add things to it to reason about it, most importantly the notion of a memory store. This is because imperative code assumes an underlying CPU + RAM which holds state. It's not that it's easier, it's that imperative code has implicit state.
    - taeric 3y ago
      Fair that I don't intend my question there as a full rebuttal. I do question if functional semantics are fully needed any more so than other tools. In particular, I recall formal methods was more about prepositional logic than it was functional semantics. And yes, you have to add and remove things to any model to really be able to reason about it. Is why engineering dynamics is harder than engineering statics. Things that change are hard. Reducing this to state being the enemy, though, I think is wrong in a lot of functional advocacy. State can be reasoned about without having to boil the ocean, as it were.
Kamq 3y ago
I'll admit to not being super great at getting down into the nitty gritty with internals of compilers. Are you talking about some sort of IR? Because if we're talking about the output, mutation definitely happens. Checking on godbolt, there's definitely mutation at least sometimes. Using gcc 13.2, I get the following output. j += i; becomes: movl -4(%rbp), %eax // move i into %eax addl %eax, -8(%rbp) // add i to j With i++ becoming: addl $1, -4(%rbp). // add 1 to i If your example is IR, do you happen to know how it crunches everything "back down" to mutability? Does it just check that the previous value of i and j were never used and use the same registers as an optimization?