3 ms·

We're getting off track. I'm not especially interested in "semantic debates" (pun partially intended), i.e. I don't really care how you define operational or d

by tome 9y ago

We're getting off track. I'm not especially interested in "semantic debates" (pun partially intended), i.e. I don't really care how you define operational or denotational semantics. The point is that fac1 and fac2 do two completely different things when executed on a computer. I can't understand how you consider them operationally isomorphic. Even more puzzling to me is how you can consider unary addition to be isomorphic to binary addition. I am no bisimulation expert but unary addition involves a single state change whilst binary addition requires many. I will have to drop out of the debate, yet again, with the feeling we are living in completely different worlds.

pron 9y ago
> We're getting off track. Oh, I think that ship sailed long ago. This started as a discussion on Kotlin. :) > The point is that fac1 and fac2 do two completely different things when executed on a computer. But they don't. You must define some equivalence relation to determine whether executions are "completely different". You could go very concretely, all the way down to memory addresses or even to logic gates in the CPU, but then the very same Haskell program may be considered to be completely different from itself when compiled by different compiler versions. So, when working with powerful systems like TLA, you get to decide how fine-grained your equivalence is, but when talking about programs and languages, you go by the semantics of the language and use (bi)simulation, as it's the homo/isomorphism normally used in programming language theory (it was first proposed, I believe, by Robin Milner). Such an isomorphism exists between the things those programs do in the computer. > Even more puzzling to me is how you can consider unary addition to be isomorphic to binary addition. I am no bisimulation expert but unary addition involves a single state change whilst binary addition requires many. Because you are allowed to map a single state in one graph to multiple ones in the other. That's the difference between a function and a relation. > I will have to drop out of the debate, yet again, with the feeling we are living in completely different worlds. Well, all I can say is that this particular branch of the discussion began when I pointed out that the functional denotation is one particular choice, made to obtain certain tradeoffs, while others, with other tradeoffs, exist. If by your world you mean the world when you only consider the theory of functional programming, then indeed there's no point discussing it within the broader context of programming language theory/program analysis. Afer all, the theory of functional programming is a strict subset of programming language theory. I don't know how to compare FP to itself, nor do I know how to compare the mathematics of FP to some imprecise notion of imperative programming. I can try to compare the mathematics of FP to the mathematics of imperative.
- tome 9y ago
  You seem to think there's this thing called the "functional denotation" that functional programmers really care about. I've never heard that term before. Google seems to suggest it's something in natural language semantics and nothing to do with functional programming. Functional programmers care about all sorts of semantics, including operational and denotational semantics. I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs not least because functional programs can be trivially rewritten as imperative ones (see CBPV).
  - pron 9y ago
    > You seem to think there's this thing called the "functional denotation" that functional programmers really care about. I've never heard that term before. Oh, but that's because FP fans call it "referential transparency"; I'm sure you've come across that term. While the terminology is incorrect (for one, Java is also referentially transparent), when FP fans say "referential transparency", they mean "value semantics", i.e., that the meaning of a function application is its normal form, or, in other words, they simply mean "functional denotation". This is exactly what enables the equational reasoning FP fans like to talk about. > I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs They could (I know it's possible to write assertions in Haskell), but then they no longer operate on the denotation of the language. You can also use unsafePerformIO in Haskell, but if you do that, you may break the mental model the language aims to create. > not least because functional programs can be trivially rewritten as imperative ones (see CBPV). Again, they could, but not in a way that preserves the benefits for which the formalism was designed for. Similarly, pure functional programs could be written in Java, but that's not the idiomatic way. To take us back to where we started, we are talking about language design, and while many languages can imitate the style of others, they are optimized for certain pragmatic and aesthetic concerns. That is my whole point.
    - tome 9y ago
      > To take us back to where we started, we are talking about language design, and while many languages can imitate the style of others, they are optimized for certain pragmatic and aesthetic concerns. That is my whole point. If that were your whole point we could have avoided this thread. No one disputes that. In fact your point seems to be that Java/imperative languages are better than Haskell/functional languages, for a reason that you have tried to elaborate and that I have failed to understand.

by tome 9y ago

pron 9y ago

> We're getting off track. Oh, I think that ship sailed long ago. This started as a discussion on Kotlin. :) > The point is that fac1 and fac2 do two completely different things when executed on a computer. But they don't. You must define some equivalence relation to determine whether executions are "completely different". You could go very concretely, all the way down to memory addresses or even to logic gates in the CPU, but then the very same Haskell program may be considered to be completely different from itself when compiled by different compiler versions. So, when working with powerful systems like TLA, you get to decide how fine-grained your equivalence is, but when talking about programs and languages, you go by the semantics of the language and use (bi)simulation, as it's the homo/isomorphism normally used in programming language theory (it was first proposed, I believe, by Robin Milner). Such an isomorphism exists between the things those programs do in the computer. > Even more puzzling to me is how you can consider unary addition to be isomorphic to binary addition. I am no bisimulation expert but unary addition involves a single state change whilst binary addition requires many. Because you are allowed to map a single state in one graph to multiple ones in the other. That's the difference between a function and a relation. > I will have to drop out of the debate, yet again, with the feeling we are living in completely different worlds. Well, all I can say is that this particular branch of the discussion began when I pointed out that the functional denotation is one particular choice, made to obtain certain tradeoffs, while others, with other tradeoffs, exist. If by your world you mean the world when you only consider the theory of functional programming, then indeed there's no point discussing it within the broader context of programming language theory/program analysis. Afer all, the theory of functional programming is a strict subset of programming language theory. I don't know how to compare FP to itself, nor do I know how to compare the mathematics of FP to some imprecise notion of imperative programming. I can try to compare the mathematics of FP to the mathematics of imperative.

tome 9y ago
You seem to think there's this thing called the "functional denotation" that functional programmers really care about. I've never heard that term before. Google seems to suggest it's something in natural language semantics and nothing to do with functional programming. Functional programmers care about all sorts of semantics, including operational and denotational semantics. I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs not least because functional programs can be trivially rewritten as imperative ones (see CBPV).
- pron 9y ago
  > You seem to think there's this thing called the "functional denotation" that functional programmers really care about. I've never heard that term before. Oh, but that's because FP fans call it "referential transparency"; I'm sure you've come across that term. While the terminology is incorrect (for one, Java is also referentially transparent), when FP fans say "referential transparency", they mean "value semantics", i.e., that the meaning of a function application is its normal form, or, in other words, they simply mean "functional denotation". This is exactly what enables the equational reasoning FP fans like to talk about. > I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs They could (I know it's possible to write assertions in Haskell), but then they no longer operate on the denotation of the language. You can also use unsafePerformIO in Haskell, but if you do that, you may break the mental model the language aims to create. > not least because functional programs can be trivially rewritten as imperative ones (see CBPV). Again, they could, but not in a way that preserves the benefits for which the formalism was designed for. Similarly, pure functional programs could be written in Java, but that's not the idiomatic way. To take us back to where we started, we are talking about language design, and while many languages can imitate the style of others, they are optimized for certain pragmatic and aesthetic concerns. That is my whole point.
  - tome 9y ago
    > To take us back to where we started, we are talking about language design, and while many languages can imitate the style of others, they are optimized for certain pragmatic and aesthetic concerns. That is my whole point. If that were your whole point we could have avoided this thread. No one disputes that. In fact your point seems to be that Java/imperative languages are better than Haskell/functional languages, for a reason that you have tried to elaborate and that I have failed to understand.