Data types as Lattices – Dana Scott [pdf](github.com) |
Data types as Lattices – Dana Scott [pdf](github.com) |
> 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.
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.
[1]: https://cuelang.org/docs/concept/the-logic-of-cue/#the-value...