Thoughts on Denotational Semantics

These are some thoughts that I had recently about denotational semantics, that I was going to send in an email to Dana but then I thought that there was no reason for them to be private! That being said, I’m not going to put too much effort into polishing them.

Logic Programming

I’m seeing that in denotational semantics people use power domains to model nondeterminism. Does anyone know about work that uses power domains to establish denotational semantics of prolog/logic programming languages? I’m sure if my googling was better I could find this

Functional reactive programming

Also, relatedly, I just learned that Conal Elliot’s original vision for functional reactive programming used denotational semantics/CPOs. Specifically, he talks about the fact that the reals are a CPO in order to resolve recursion in functional reactive programming!

@epatters and I have been thinking that once we have a good type theory with semantics in \mathsf{Cat} (i.e., categories where the objects are “values” and the morphisms are “diffs”) then the time is ripe to revisit functional reactive programming, where elements of \mathtt{Behavior}\: a are functors from the poset (\mathbb{R}, \leq) to \llbracket a \rrbracket (the denotation of a). We recover the traditional notion of time-varying value by letting \llbracket a \rrbracket be a codiscrete category, and we recover the traditional notion of events via letting \llbracket a \rrbracket be the single-object category corresponding to the free monoid on some set of events.

But then we are free to also have more interesting diffs, for instance \llbracket \mathtt{List}\: a \rrbracket can have a precise specification of inserts and deletes as its diffs, which means that you can, for instance, perform the precise edits to the DOM that you need in the context of a functional reactive programming web framework.

I seem to remember Adam Vandervorst telling me about an implementation of this he had in Scala, which he called “Delta Streams”; I will ping him and see if I can get him to leave a comment about the status of that project. Maybe @mromang08 would be interested in formalizing this notion of stream?

I think the time is ripe to work out theory of this type of functional reactive programming with denotational semantics, and see if we could replicate the theorems in Conal’s 1997 paper in this more general setting.

And then of course, we could consider different time domains as well, if we want to think about concurrency, e.g. non-linear posets.


I just realized that the single-object category for the free monoid on the set of events is the wrong model. I actually want the category where an object is an element of the monoid, and a map from m to n is some p such that mp = n. In the case of the free monoid, this is a preorder; it differs from the codiscrete category in that you can only add events, never change or remove events.