In thinking about the defunctionalization paper from the prior post, I've come to the conclusion that polymorphism is a big problem for current control flow static analyses. Polymorphic functions introduce a lot of joining of abstract values. See Polymorphic splitting an effective polyvariant flow analysis
In reality the main thing that CFA is trying to address is where to values flow. In order to make the problem tractable, we need to abstract, and make adjustments to ensure termination. The main adjustment that is needed is to make recursion bounded. However, everything other adjustment seems to be a tradeoff between precision and theoretical complexity. The paradox of static analysis is that the more precise you can be the fewer spurious flow paths you explore, and the quicker the analysis in practice. However, the more precise you are the more complex the analysis is in theory. However, it seems to me that the theoretical complexity is more tied to the nature that with a constant m or k limit, you end up following more and more recursion. What if recursion was the only thing bounded by m or k? Essentially just have a parameter that controls the unrolling of recursive / mutually recursive functions. I wonder how precise such an analysis could be. I feel like Kimball has talked about some sort of analysis that uses regular expressions on traces to find or bound recursion. I'll have to see if I can find that paper, and see how it differs from my ideas.
Two thoughts about this:
- I wonder if I can augment my approach for Trace Preserving mCFA (unpublished) to account for these sorts of patterns
- I wonder if I can use the defunctionalization approach to do a set / union type system that handles polymorphism well
There is a lot of literature that I haven't read on this topic. I know I've seen at least one or two CFA papers about handling polymorphism specifically (such as let bound lambdas). Additionally, I have very little experience or background with set based type systems and defunctionalization. It would require a lot deeper dive into the literature to see what has already been done.
However, I think a union type inference (maybe augmented with both structural and nominal types) along with defunctionalization could get rid of a ton of spurious control flow for a CFA, and potentially be able to handle any untyped language. Using inference to type untyped languages seems like a hard problem, I wonder what the state of the art is. Here is one paper about Programming with union, intersection, and negation types which is probably a good introduction to set based type systems.
Additionally, I had some thoughts about how to proceed a full program analysis for algebraic effects and modern abstractions
- I'm thinking that it might be easiest (as far as just getting some results for the lab for a paper later this summer), to just use a small lambda calculus language based on scheme, with just a couple things added.
(perform action ...args)for performing an effect, and(handle action (lambda (resume, ...args) handler) (lambda () body))for the handling of the action. I'll focus on deep effect handlers, which reinstall the handler for the resumption. Additionally, I need to think more about threading state through, which is a common thing for languages with deep effect handlers to do, and makes it much easier to implement mutable state as an effect. Maybe something like:(handle action initial-state (lambda (state, resume, ...args) handler) (lambda (state) body))with perform changing to(perform action ...args (lambda (result, state) body)) - I could also remove mutation from the language since I can just use the state effect
- Should I support user datatypes (currently in my prior analyses I just support linked lists and primitives), I think at the very least I should try supporting structural objects (which could all be represented the same way). Nominal objects could just be an extension of structural objects with a special tag field.