[HN Gopher] Data types as Lattices - Dana Scott [pdf]
       ___________________________________________________________________
        
       Data types as Lattices - Dana Scott [pdf]
        
       Author : ozb
       Score  : 7 points
       Date   : 2024-08-09 17:48 UTC (5 hours ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | ozb wrote:
       | 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.
        
         | almostgotcaught wrote:
         | 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 wrote:
           | 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.
        
       ___________________________________________________________________
       (page generated 2024-08-09 23:01 UTC)