4 ms·

What? There is no "the" instance of abstract interpretation, because different uses of it will have different abstract domains they are interpreting over and di

by chc4 2y ago

What? There is no "the" instance of abstract interpretation, because different uses of it will have different abstract domains they are interpreting over and different transfer functions. There's no reason to choose types as being a more privileged implementant than odd/even, and choosing odd/even as being a "case" of a type doesn't make more sense than choosing types as being a "case" of odd/even.

tekknolagi 2y ago
In particular PyPy's abstract values have multiple domains at once: type, known bits, known range, etc. They do it all in one pass
- almostgotcaught 2y ago
  no shade at you (i like you and your work and blog) but > type, known bits, known range these are all the same thing. i was thinking about this question in the shower (before responding) and i'm pretty sure type inference (for whatever purpose, like deducing the type, or refining the type, etc) is the only use-case of abstract interpretation. if you look at couset's webpage (i haven't read the original papers) you see lots of cute pics of program trajectory but no one actually uses abstract interpretation for control-flow tracking - the lattice is only ever updated at a type boundary. prove me wrong (like i could be wrong) but i'm reflecting on implementations in llvm/mlir/pytype ie mature/real use-cases (i have not poked around in pypy's impl).
  - tekknolagi 2y ago
    I'm not sure what you mean that they're the same thing. They're different domains with different transfer functions. There's even a recent ish paper exploring how they can be used to inform one another. Can you say more?
    - almostgotcaught 2y ago
      > type, known bits, known range >I'm not sure what you mean that they're the same thing they're all components of the type; i have no idea what pypy does with "known bits" but deducing "range" of a value is firmly/unanimously as "type refinement" (see https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type) i.e. still a part/aspect/dimension of the type not of the value.
      - x0xrx 2y ago
        I think with a suitably expansive definition of “type” you can get pretty far in this direction. I have personally used AI for control flow analysis of a toy OO language.
  - funcDropShadow 2y ago
    I'll leave this link here for you: https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm If you are not convinced think about the name of the company during your next shower.
  - archi42 2y ago
    They're related, but they're not the same thing: E.g. when analysing a JS-like language and you see "x = a + b" with raw memory content a = {0x1,0x2}, b = {0x3} you get x = {0x4,0x5,0x13,0x23} - because you can't tell if that + is a string concatenation or numerical addition. Of course when analysing program code, you might want to carry type information with you. The math behind AI allows to combine basically any domain to a single domain without losing all the nice properties of the Galois connection. But usually you get away with tracking multiple domains simultaneously, since that's also a lot easier from an engineering perspective (someone has to understand and maintain that code for a few decades). Edit: I recommend following funcDropShadow's advice.
marcosdumay 2y ago
Let me repeat what I think the question is in other words: Is there any kind of abstract interpretation that can not be modeled as a type system?
- almostgotcaught 2y ago
  that's not what the other question/poster/person is implying - every can already be modeled as a type system because type systems (at least some of them) are turing complete. the other question asking whether there's any other application of abstract interpretation other than type checking/type inference. to which i say no or at least none that i've ever seen ie no one ever does anything with it something about eg control flow. it's always only about types. edit: i was about to say "for example no one ever uses abstract interpretation for escape analysis" and then i wanted to double check and lo and behold https://dl.acm.org/doi/abs/10.1145/945885.945886 https://dl.acm.org/doi/abs/10.1145/945885.945886. so i guess i'm wrong (and the other original question can be answered in the negative) but i would still argue that it's true in practice. the reason is obvious - the space/lattice of possible types of a program is huge, the space of states is .......... busy beaver scale.
  - ant6n 2y ago
    There’s forward and backward propagation. Backward propagation is generally less about the type of a variable, but it’s still a form of abstract interpretation. For example, is-live (or dead) or used analysis, or reachable analyses are not really type information, as they tend to depend on the control flow after a point. There’s some other analysis that’s not type-like as such, for example available expressions.
  - derdi 2y ago
    You might as well express escape analysis as inferring an "escaping reference" or "non-escaping reference" type for each allocation site. Then you're back to "abstract interpretation is type inference". But wanting to make this statement true also makes it meaningless. Tautological-by-definition statements aren't interesting.
- JonChesterfield 2y ago

by chc4 2y ago

tekknolagi 2y ago

In particular PyPy's abstract values have multiple domains at once: type, known bits, known range, etc. They do it all in one pass

almostgotcaught 2y ago
no shade at you (i like you and your work and blog) but > type, known bits, known range these are all the same thing. i was thinking about this question in the shower (before responding) and i'm pretty sure type inference (for whatever purpose, like deducing the type, or refining the type, etc) is the only use-case of abstract interpretation. if you look at couset's webpage (i haven't read the original papers) you see lots of cute pics of program trajectory but no one actually uses abstract interpretation for control-flow tracking - the lattice is only ever updated at a type boundary. prove me wrong (like i could be wrong) but i'm reflecting on implementations in llvm/mlir/pytype ie mature/real use-cases (i have not poked around in pypy's impl).
- tekknolagi 2y ago
  I'm not sure what you mean that they're the same thing. They're different domains with different transfer functions. There's even a recent ish paper exploring how they can be used to inform one another. Can you say more?
  - almostgotcaught 2y ago
    > type, known bits, known range >I'm not sure what you mean that they're the same thing they're all components of the type; i have no idea what pypy does with "known bits" but deducing "range" of a value is firmly/unanimously as "type refinement" (see https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type) i.e. still a part/aspect/dimension of the type not of the value.
    - x0xrx 2y ago
      I think with a suitably expansive definition of “type” you can get pretty far in this direction. I have personally used AI for control flow analysis of a toy OO language.
- funcDropShadow 2y ago
  I'll leave this link here for you: https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm If you are not convinced think about the name of the company during your next shower.
- archi42 2y ago
  They're related, but they're not the same thing: E.g. when analysing a JS-like language and you see "x = a + b" with raw memory content a = {0x1,0x2}, b = {0x3} you get x = {0x4,0x5,0x13,0x23} - because you can't tell if that + is a string concatenation or numerical addition. Of course when analysing program code, you might want to carry type information with you. The math behind AI allows to combine basically any domain to a single domain without losing all the nice properties of the Galois connection. But usually you get away with tracking multiple domains simultaneously, since that's also a lot easier from an engineering perspective (someone has to understand and maintain that code for a few decades). Edit: I recommend following funcDropShadow's advice.

marcosdumay 2y ago

Let me repeat what I think the question is in other words: Is there any kind of abstract interpretation that can not be modeled as a type system?

almostgotcaught 2y ago
that's not what the other question/poster/person is implying - every can already be modeled as a type system because type systems (at least some of them) are turing complete. the other question asking whether there's any other application of abstract interpretation other than type checking/type inference. to which i say no or at least none that i've ever seen ie no one ever does anything with it something about eg control flow. it's always only about types. edit: i was about to say "for example no one ever uses abstract interpretation for escape analysis" and then i wanted to double check and lo and behold https://dl.acm.org/doi/abs/10.1145/945885.945886 https://dl.acm.org/doi/abs/10.1145/945885.945886. so i guess i'm wrong (and the other original question can be answered in the negative) but i would still argue that it's true in practice. the reason is obvious - the space/lattice of possible types of a program is huge, the space of states is .......... busy beaver scale.
- ant6n 2y ago
  There’s forward and backward propagation. Backward propagation is generally less about the type of a variable, but it’s still a form of abstract interpretation. For example, is-live (or dead) or used analysis, or reachable analyses are not really type information, as they tend to depend on the control flow after a point. There’s some other analysis that’s not type-like as such, for example available expressions.
- derdi 2y ago
  You might as well express escape analysis as inferring an "escaping reference" or "non-escaping reference" type for each allocation site. Then you're back to "abstract interpretation is type inference". But wanting to make this statement true also makes it meaningless. Tautological-by-definition statements aren't interesting.
JonChesterfield 2y ago