this post was submitted on 28 Sep 2024
8 points (100.0% liked)

Programming Languages

1167 readers
5 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:

See /r/ProgrammingLanguages for specific examples

Related online communities

founded 1 year ago
MODERATORS
 

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

  1. It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and
  2. 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.

you are viewing a single comment's thread
view the rest of the comments
[–] [email protected] 2 points 1 month ago (6 children)

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

[–] [email protected] 1 points 1 month 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.

[–] [email protected] 0 points 1 month 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.

load more comments (4 replies)