WingNews logo WingNews
top | item 41203929

(no title)

ozb | 1 year ago

I read this paper some 10 years ago, and have always wondered whether these ideas are implemented in industry. I know people use Denotational Semantics in academia, but eg I want an actual language that can encode the language-independent "meaning" of both a c++ template library and a Python program in a composable way, and also express and prove refinement relations between different specifications and implementations.

discuss

order

almostgotcaught|1 year ago

People will get mad at me for saying this but... this isn't that deep. As with most things in academic CS, this is just a formalization of stuff that is very common practical engineering.

> academia, but eg I want an actual language that can encode the language-independent "meaning" of both a c++ template library and a Python program

The name of the paper is "data types as lattices" so data not programs as such and denotational semantics is about programs. So I'll say:

1. A language independent representation of a data type is just a protobuf (or whatever your favorite serialization/deserialization framework is);

2. The language of lattices is very common in eg compilers (eg grep for lattice in LLVM) but again it's cart before the horse kind of stuff because there's not much there to be exploited in representing your unions and intersections as meet and join;

3. A language independent representation of operations is an IR and indeed you can inductively derive certain facts about some language level features (across multiple languages) by analyzing the IR. Again cf LLVM

I realize the paper is from 1976 so someone will pop up and say "the paper inspired these things" but it's just not true; people generally follow their nose when implementing and then someone comes along and says "let's name it a lattice".

This isn't a hot-take or something, it's just experience from being on both sides of the fence.

philzook|1 year ago

I think you are not doing this line of work justice.

Lattices like intervals or sets of values or zero/nonzero are typical and natural even without studying lots of theory.

I believe this paper is about how you can use the concept of a particular kind of lattice to give a rigorous mathematical semantics to possibly non terminating computations such as the untyped lambda calculus. This was not at all obvious before Scott. I don't feel qualified to comment much beyond that.

I suppose this is related to the simpler examples of lattices, but it's quite a feat.