6 ms·

the complaints about the Protobuf type system being not flexible enough are also really funny to read. fundamentally, the author refuses to contend with the fa

the complaints about the Protobuf type system being not flexible enough are also really funny to read. fundamentally, the author refuses to contend with the fact that the context in which Protobufs are used -- millions of messages strewn around random databases and files, read and written by software using different versions of libraries -- is NOT the same scenario where you get to design your types once and then EVERYTHING that ever touches those types is forced through a type checker. again, this betrays a certain degree of amateurishness on the author's part. Kenton has already provided a good explanation here: https://news.ycombinator.com/item?id=45140590 https://news.ycombinator.com/item?id=45140590

instig007 1y ago
> is NOT the same scenario where you get to design your types once and then EVERYTHING that ever touches those types is forced through a type checker. the author never claimed the types had to be designed only once, he claimed that schema evolution chosen by protobuf is inadequate for the purpose of lossless evolution. > Kenton has already provided a good explanation here: https://news.ycombinator.com/item?id=45140590 https://news.ycombinator.com/item?id=45140590 TLDR: yada-yada [...] protobuf is practical, type algebra either doesn't exist or impractical because only PL theorists know about it, not Kenton.
- kentonv 1y ago
  > type algebra either doesn't exist or impractical because only PL theorists know about it, not Kenton. Hi I'm Kenton. I, too, was enamored with advanced PL theory in college. Designed and implemented my own purely-functional programming language. Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks. In two decades building real-world complex systems, though, I've found that getting PL theory right is rarely the highest-leverage way to address the real problems of software engineering.
  - instig007 1y ago
    > Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks. Hi Kenton, I'm not sure what kind of PL theory you studied in college, but "array bounds-safety without runtime checks" don't require dependent types. They are being proven with several available SMT solvers as of right now, just ask LLVM folks with their "LLVM_ENABLE_Z3_SOLVER" compiler flag, the one that people build their real-world solutions on. By the way, you don't have to say "real-world" in every comment to appeal to your google years as a token of "real-world vs the rest of you". "But my team at google wouldn't use it", or something along that line, right? https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/book1.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...
    - kentonv 1y ago
      Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase. You need annotations that let you say "this array's size is is the same as that array" or "this integer is within the bounds of that array" -- that's dependent types.
      - instig007 1y ago
        > Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase. Please, Kenton, don't move your goalpost. Who said about "unaided"? Annotations, whether they come directly from a developer, or from IR meta, don't make a provided SAT-constraint suddenly a "dependent type" component of your type system, it needs a bit more than that. Let's not miss the "types" in "dependent types". You don't modify type systems of your languages to run SAT solvers in large codebases. Truly, if you believe that annotations for the purpose of static bounds checking "is not realistic in a large codebase" (or is it because you assume it's unaided?), I've got "google/pytype" and the entire Python community to justify before you.
        kentonv 1y ago

instig007 1y ago

> is NOT the same scenario where you get to design your types once and then EVERYTHING that ever touches those types is forced through a type checker. the author never claimed the types had to be designed only once, he claimed that schema evolution chosen by protobuf is inadequate for the purpose of lossless evolution. > Kenton has already provided a good explanation here: https://news.ycombinator.com/item?id=45140590 https://news.ycombinator.com/item?id=45140590 TLDR: yada-yada [...] protobuf is practical, type algebra either doesn't exist or impractical because only PL theorists know about it, not Kenton.

kentonv 1y ago
> type algebra either doesn't exist or impractical because only PL theorists know about it, not Kenton. Hi I'm Kenton. I, too, was enamored with advanced PL theory in college. Designed and implemented my own purely-functional programming language. Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks. In two decades building real-world complex systems, though, I've found that getting PL theory right is rarely the highest-leverage way to address the real problems of software engineering.
- instig007 1y ago
  > Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks. Hi Kenton, I'm not sure what kind of PL theory you studied in college, but "array bounds-safety without runtime checks" don't require dependent types. They are being proven with several available SMT solvers as of right now, just ask LLVM folks with their "LLVM_ENABLE_Z3_SOLVER" compiler flag, the one that people build their real-world solutions on. By the way, you don't have to say "real-world" in every comment to appeal to your google years as a token of "real-world vs the rest of you". "But my team at google wouldn't use it", or something along that line, right? https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/book1.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...
  - kentonv 1y ago
    Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase. You need annotations that let you say "this array's size is is the same as that array" or "this integer is within the bounds of that array" -- that's dependent types.
    - instig007 1y ago
      > Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase. Please, Kenton, don't move your goalpost. Who said about "unaided"? Annotations, whether they come directly from a developer, or from IR meta, don't make a provided SAT-constraint suddenly a "dependent type" component of your type system, it needs a bit more than that. Let's not miss the "types" in "dependent types". You don't modify type systems of your languages to run SAT solvers in large codebases. Truly, if you believe that annotations for the purpose of static bounds checking "is not realistic in a large codebase" (or is it because you assume it's unaided?), I've got "google/pytype" and the entire Python community to justify before you.
      - kentonv 1y ago