Hacker News new | past | comments | ask | show | jobs | submit login

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?




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. 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.


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.


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.


Abstract interpretation can do constant folding and branch elision. It changes the program instance. Type checking is about invariants over a specific program, not changing the program itself.


Most languages have type polymorphism that do change the program itself. But I agree, neither of those examples are instances of it.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: