Programming Languages

1187 readers

1 users here now

Hello!

This is the current Lemmy equivalent of https://www.reddit.com/r/ProgrammingLanguages/.

The content and rules are the same here as they are over there. Taken directly from the /r/ProgrammingLanguages overview:

This community is dedicated to the theory, design and implementation of programming languages.

Be nice to each other. Flame wars and rants are not welcomed. Please also put some effort into your post.

This isn't the right place to ask questions such as "What language should I use for X", "what language should I learn", and "what's your favorite language". Such questions should be posted in /c/learn_programming or /c/programming.

This is the right place for posts like the following:

"Check out this new language I've been working on!"
"Here's a blog post on how I implemented static type checking into this compiler"
"I want to write a compiler, where do I start?"
"How does the Java compiler work? How does it handle forward declarations/imports/targeting multiple platforms/?"
"How should I test my compiler? How are other compilers and interpreters like gcc, Java, and python tested?"
"What are the pros/cons of ?"
"Compare and contrast vs. "
"Confused about the semantics of this language"
"Proceedings from PLDI / OOPSLA / ICFP / "

See /r/ProgrammingLanguages for specific examples

Related online communities

founded 2 years ago

MODERATORS

armchair_progamer

Total Denotational Semantics (blog) (fixpt.de)

submitted 2 months ago by armchair_progamer to c/programming_languages

7 comments fedilink hide all child comments

Background: What are denotational semantics, and what are they useful for?

Also: Operational and Denotational Semantics

Denotational semantics assign meaning to a program (e.g. in untyped lambda calculus) by mapping the program into a self-contained domain model in some meta language (e.g. Scott domains). Traditionally, what is complicated about denotational semantics is not so much the function that defines them; rather it is to find a sound mathematical definition of the semantic domain, and a general methodology of doing so that scales to recursive types and hence general recursion, global mutable state, exceptions and concurrency^1^^2^.

In this post, I discuss a related issue: I argue that traditional Scott/Strachey denotational semantics are partial (in a precise sense), which means that

It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and

Internal details of the semantic domain inhibit high-level, equational reasonining about programs

After exemplifying the problem, I will discuss total denotational semantics as a viable alternative, and how to define one using guarded recursion.

I do not claim that any of these considerations are novel or indisputable, but I hope that they are helpful to some people who

know how to read Haskell

like playing around with operational semantics and definitional interpreters

wonder how denotational semantics can be executed in a programming language

want to get excited about guarded recursion.

I hope that this topic becomes more accessible to people with this background due to a focus on computation.

I also hope that this post finds its way to a few semanticists who might provide a useful angle or have answers to the conjectures in the later parts of this post.

If you are in a rush and just want to see how a total denotational semantics can be defined in Agda, have a look at this gist.

top 7 comments

sorted by: hot top controversial new old

[–] [email protected] 2 points 2 months ago (2 children)

I thought I might learn something new about programming, instead I just learnt I'm not smart enough to understand this. :-(

[–] [email protected] 6 points 2 months ago (1 children)

You probably are. It's just an extremely specific domain and terminatory, and you are missing several underlying concepts required to understand it. It's literally a different language and you haven't learned the vocabulary; it looks like English, but the words have specific meanings in the context.

Not that it isn't complex, but I think it's a mistake to think that, just because you haven't learned Greek, that you're not smart enough to understand it. You're simply undereducated in the domain.

[–] [email protected] 3 points 2 months ago (2 children)

If was half a joke, but that mathematics might as well have been hieroglyphics.

Would you class this as computational theory? As a software developer is this field likely to be used in a day to day manner or is it more abstract than that?

[–] [email protected] 1 points 2 months ago

Oh, I don't follow the math at all, and much of the terminology is gibberish to me. I just didn't want you thinking you couldn't understand something you probably could, if you spent some time in the field.

I agree that understanding the math is always next level; you almost have to be working in the domain, or at least be a mathematician, to follow the maths in papers like this. I sort of gloss over it, now; despite being 4 credits short of a math minor, I've never use any of it outside of set theory and a little discrete math in my career and have forgotten nearly everything past algebra. It's frustrating, but although I enjoyed it, I didn't enjoy it enough to keep up in my free time and it's a perishable skill.

Anyway, while coming up with and proving the research requires real skill, I hate the idea of someone assuming they're incapable of understanding something, when it's often not a lack of potential, only a lack of education.

Lastly: I do think we have limits. I didn't take that last math course because I was already struggling with the number of levels of abstraction required to mentally retain the tools to do the work, and realized I'd never be a professional mathematician. There are levels of math I'm simply too stupid to understand, no matter how much time I spent studying. But the barrier in this paper IMHO seems to be that it's highly domain specific, and so demands a fair amount of understanding of domain terminology.

[–] Corbin 1 points 2 months ago

Semantics was originally studied as model theory, and today is phrased with category theory. You use this every day when you imagine what a program does in terms of machine effects.

[–] FizzyOrange 1 points 2 months ago (1 children)

Yeah this sort of stuff reads a lot like philosophy nonsense babble to me. I think maybe it isn't nonsense like the philosophy stuff but it sure would be nice if they gave a few concrete examples to demonstrate that.

The Background link does make sense... but it also seems kind of trivial. Giving the idea of mapping programming language semantics to an existing domain like mathematics a complex name like "denotational semantics" just serves to make it harder to understand and more impenetrable.

Generally I think naming things should make them easier to understand, e.g. naming "a number that represents the address of another object" a "pointer" is great, because it literally is something that points to another thing.

Denotational semantics is a terrible terrible name. I'm not even sure it should have a name. Can we call it "mathematical semantics" (if you map to maths)?

(I may be totally wrong here because I'm not a denotational semantics expert, but I have at least tried to follow it before getting whacked in the face with a load of philosophy.)

Reminds me a lot of REST. The core idea of REST is very simple, but it's also really hard to learn what that idea is because so much of it is hidden behind bullshit philosophy.

[–] Corbin 0 points 2 months ago

Nah, you're just not good with maths. Programming languages are mathematical objects and denotational semantics is merely treating languages as categories and looking for functors leading out of them.