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 (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-...
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!
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....
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.
And I object to false claims that pure FP is somehow "better designed" than other approaches (which is how this entire discussion started). Design is a matter of aesthetics (completely subjective) and pragmatics (also subjective, but can be measured empirically) -- not theory -- and aesthetics and pragmatics are the sources of value -- again, not theory.
let x = 1 + 1
in x * x
let x = 1 + 1
y = 1 + 1
in x * y
let x = 1 + 1
in x * x
(\x -> x * x) (1 + 1)
Similarly,
let x = 1 + 1
y = 1 + 1
in x * y
(\x -> \y -> x * y) (1 + 1) (1 + 1)
As 4 = 4, the denotation of these two expressions is equal.
2. Functional semantics are convenient for sequential programs.
[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.
I'm all in favour of you promoting technologies and approches that you think are beneficial. What I would ask you to stop doing (again) is critiquing Haskell without really understanding it.
Heh, well, in a way I guess you could say I made that "term" up, but it's not an atomic term. The formal semantics of a syntactic term is some object (in the semantic domain of the formalism) mapped to that term. If that object is a function (or something close to it), what you have is functional semantics. Similarly, you have relational semantics, behavior semantics, and any other kind that you may find useful; even evidence semantics, which assigns evidence objects to terms.
I've heard some academics refer to it as "value semantics", which, I guess, hints to the fact that the denotation of a lambda application is the value that the lambda term reduces to, but I find that terminology to be unclear. I've heard Haskell programmers (in the pseudo-mathematical atmosphere that seems to be common in that community) refer to it as "referential transparency", which is downright misleading because referential transparency does actually have sort-of a well-defined meaning, and it's not quite that. I've heard Conal Elliot refer to it simply as "denotational" (as in "functional programming is denotational programming"), which is also misleading because not all denotations are functions. So, I find "functional semantics" to be both precise and clear.
> You also seem to believe that it's the only semantics that functional programmers care about and this is why I say you have a big misunderstanding about Haskell.
Where did you get that? What I may have said or alluded to, in so many words, is that denotational semantics are important for writing and analyzing programs, and I find that functional semantics don't make a great fit for non-sequential programs. After all, it only pays to think "denotationally" if the denotation is simple and a natural fit for the domain.
https://news.ycombinator.com/item?id=11907547
I'm afraid I still can't understand your position.