3 ms·

At the risk of sounding like a stuck record, I think you'll make much more headway explaining why something you know well is good (say, the semantics of Eve, wh

by tome 9y ago

At the risk of sounding like a stuck record, I think you'll make much more headway explaining why something you know well is good (say, the semantics of Eve, which I don't think you've elaborated on at all in this thread -- a missed opportunity) than you will explaining why something that you don't know well is bad (say, the semantics and real world applications of Haskell, which you demonstrate again and again you don't understand, and it's really quite embarrassing).

pron 9y ago
1. I don't believe in good or bad when it comes to programming languages. There are neither theoretical nor empirical justifications for assigning such a value judgment. I was only pointing out some intentional tradeoffs in the design of different formalisms. I believe in a rather subjective more/less appealing/convenient. 2. I believe I understand the semantics of Haskell (or, at least that of strict FP languages) well enough, certainly for the purpose of this discussion. 3. The semantics of Eve is essentially that of Dedalus [1], which, in turn, is similar to the semantics of all synchronous languages (which have been very successfully used in industry for formally verified safety-critical real-time software and hardware), and are heavily inspired by linear temporal logic (in fact, the logic and the PLs were developed practically hand in hand). Dedalus is especially inspired by Lamport's TLA, a particularly simple and particularly powerful linear temporal logic. I've written about TLA (which forms the computational logic part of TLA+) here https://pron.github.io/posts/tlaplus_part3 https://pron.github.io/posts/tlaplus_part3 (the two previous installments are not strictly necessary, but if you're interested in program analysis and find that post interesting, you may want to read part 4 as well). [1]: Dedalus: Datalog in Time and Space https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-173.html https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-...
- tome 9y ago
  So what do you consider the "functional semantics" of let x = 1 + 1 in x * x and how does it differ from the "functional semantics" of let x = 1 + 1 y = 1 + 1 in x * y (under GHC, if you consider that relevant)?
  - pron 9y ago
    I don't know Haskell, but in Lisp, and IIRC also in ML, a "let" expression is shorthand for a lambda application, so: let x = 1 + 1 in x * x is equivalent to: (\x -> x * x) (1 + 1) As the denotational semantics of any lambda expression is represented by its normal form, for function application that would be the result of evaluating that function with substitution; the normal expression is 4, which denotes the integer 4. Similarly, let x = 1 + 1 y = 1 + 1 in x * y is equivalent to: (\x -> \y -> x * y) (1 + 1) (1 + 1) and, so, by the functional denotation, this also denotes the integer 4. As 4 = 4, the denotation of these two expressions is equal.
    - tome 9y ago
      It's very telling that you consider the denotational semantics to be the important thing here.
      - pron 9y ago
        1. Telling? That's what you asked for. 2. Functional semantics are convenient for sequential programs.
        tome 9y ago
        "Telling" in this context means "revealing". It's very revealing that you seem to think that the most important semantics of functional programs is the denotational one when in fact lots of other important and useful semantics exist.
        pron 9y ago
        I know what "telling" means. I just didn't understand what was telling, since you asked for the denotational semantics so I described them [1]. Why would I think that some semantics are more important than others? [1]: Perhaps there's been a misunderstanding. Functional semantics means that expressions denote things similar to functions. Usually, operational semantics are state-machine semantics, certainly not functional semantics. If you'd asked for the state machine semantics, I would have described those.
- tome 9y ago
  > 1. I don't believe in good or bad ... Then take my "good" and "bad" as shorthand for "more" and "less" appealing/convenient. > 3. The semantics of Eve is essentially that of Dedalus If expanded on that as much as you have expanded on the semantics of Haskell in this thread then we might actually learn something very interesting!
  - pron 9y ago
    > Then take my "good" and "bad" as shorthand for "more" and "less" appealing/convenient. So why are you upset when I say that I don't find pure FP to be appealing or convenient for concurrent/interactive/distributed programs? I think that the very notion of representing computation as functions in such circumstances is ill-advised, and results in a very inconvenient, very unnatural (at least for me), and very hard-to-reason-about formalism compare to alternatives. Nevertheless, my opinion is subjective, and I can accept that some may not share it. > If expanded on that as much as you have expanded on the semantics of Haskell in this thread then we might actually learn something very interesting! I did. Read my blog post (which is the general theory), and then read the Dedalus paper. Some time ago you asked me to write something about TLA(+). I have, my posts (especially parts 3 and 4) are aimed precisely to get people away from what Lamport calls the "Whorfian syndrome", which is confusing the analysis of a particular formalism with that of computation or programs in general. In addition, I strongly recommend reading the overview paper, Binary Relations for Abstraction and Refinement [1] by David A Schmidt (who also wrote the book Denotational Semantics: A Methodology for Language Development). While the last section of that paper discusses temporal logic, the paper really applies to all programs in all programming languages. [1]: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4564&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16....
    - tome 9y ago
      > So why are you upset when I say that I don't find pure FP to be appealing or convenient for concurrent/interactive/distributed programs? I'm not sure "upset" is the right word but what I object to is your repeated mischaracterisations and misunderstandings of Haskell, especially of how it is used by industry programmers.

by tome 9y ago

pron 9y ago

1. I don't believe in good or bad when it comes to programming languages. There are neither theoretical nor empirical justifications for assigning such a value judgment. I was only pointing out some intentional tradeoffs in the design of different formalisms. I believe in a rather subjective more/less appealing/convenient. 2. I believe I understand the semantics of Haskell (or, at least that of strict FP languages) well enough, certainly for the purpose of this discussion. 3. The semantics of Eve is essentially that of Dedalus [1], which, in turn, is similar to the semantics of all synchronous languages (which have been very successfully used in industry for formally verified safety-critical real-time software and hardware), and are heavily inspired by linear temporal logic (in fact, the logic and the PLs were developed practically hand in hand). Dedalus is especially inspired by Lamport's TLA, a particularly simple and particularly powerful linear temporal logic. I've written about TLA (which forms the computational logic part of TLA+) here https://pron.github.io/posts/tlaplus_part3 https://pron.github.io/posts/tlaplus_part3 (the two previous installments are not strictly necessary, but if you're interested in program analysis and find that post interesting, you may want to read part 4 as well). [1]: Dedalus: Datalog in Time and Space https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-173.html https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-...

tome 9y ago
So what do you consider the "functional semantics" of let x = 1 + 1 in x * x and how does it differ from the "functional semantics" of let x = 1 + 1 y = 1 + 1 in x * y (under GHC, if you consider that relevant)?
- pron 9y ago
  I don't know Haskell, but in Lisp, and IIRC also in ML, a "let" expression is shorthand for a lambda application, so: let x = 1 + 1 in x * x is equivalent to: (\x -> x * x) (1 + 1) As the denotational semantics of any lambda expression is represented by its normal form, for function application that would be the result of evaluating that function with substitution; the normal expression is 4, which denotes the integer 4. Similarly, let x = 1 + 1 y = 1 + 1 in x * y is equivalent to: (\x -> \y -> x * y) (1 + 1) (1 + 1) and, so, by the functional denotation, this also denotes the integer 4. As 4 = 4, the denotation of these two expressions is equal.
  - tome 9y ago
    It's very telling that you consider the denotational semantics to be the important thing here.
    - pron 9y ago
      1. Telling? That's what you asked for. 2. Functional semantics are convenient for sequential programs.
      - tome 9y ago
        "Telling" in this context means "revealing". It's very revealing that you seem to think that the most important semantics of functional programs is the denotational one when in fact lots of other important and useful semantics exist.
        pron 9y ago
        I know what "telling" means. I just didn't understand what was telling, since you asked for the denotational semantics so I described them [1]. Why would I think that some semantics are more important than others? [1]: Perhaps there's been a misunderstanding. Functional semantics means that expressions denote things similar to functions. Usually, operational semantics are state-machine semantics, certainly not functional semantics. If you'd asked for the state machine semantics, I would have described those.
tome 9y ago
> 1. I don't believe in good or bad ... Then take my "good" and "bad" as shorthand for "more" and "less" appealing/convenient. > 3. The semantics of Eve is essentially that of Dedalus If expanded on that as much as you have expanded on the semantics of Haskell in this thread then we might actually learn something very interesting!
- pron 9y ago
  > Then take my "good" and "bad" as shorthand for "more" and "less" appealing/convenient. So why are you upset when I say that I don't find pure FP to be appealing or convenient for concurrent/interactive/distributed programs? I think that the very notion of representing computation as functions in such circumstances is ill-advised, and results in a very inconvenient, very unnatural (at least for me), and very hard-to-reason-about formalism compare to alternatives. Nevertheless, my opinion is subjective, and I can accept that some may not share it. > If expanded on that as much as you have expanded on the semantics of Haskell in this thread then we might actually learn something very interesting! I did. Read my blog post (which is the general theory), and then read the Dedalus paper. Some time ago you asked me to write something about TLA(+). I have, my posts (especially parts 3 and 4) are aimed precisely to get people away from what Lamport calls the "Whorfian syndrome", which is confusing the analysis of a particular formalism with that of computation or programs in general. In addition, I strongly recommend reading the overview paper, Binary Relations for Abstraction and Refinement [1] by David A Schmidt (who also wrote the book Denotational Semantics: A Methodology for Language Development). While the last section of that paper discusses temporal logic, the paper really applies to all programs in all programming languages. [1]: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4564&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16....
  - tome 9y ago
    > So why are you upset when I say that I don't find pure FP to be appealing or convenient for concurrent/interactive/distributed programs? I'm not sure "upset" is the right word but what I object to is your repeated mischaracterisations and misunderstandings of Haskell, especially of how it is used by industry programmers.