Data types as Lattices – Dana Scott [pdf]
github.comI 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.
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.
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.
I didn't recognize the name but then I went to the paper and realized this is one of the papers that establishes a model (as in model theory) for untyped lambda calculus. I knew about the result but not the author's name (nor the name of the paper). Ok I retract some of my cynicism. Still not very overwhelmed though by the gravity of the result. I'm not one of those people that worships Church ie I'm aware of all of the stuff people manage to prove with lambda calculi but I've yet to see any practical value (so we arrive at an actually negative answer to op's question).
CUE lang [1] is one instance where the idea of data types as lattices is implemented in industry
[1]: https://cuelang.org/docs/concept/the-logic-of-cue/#the-value...