Homomorphic static analysis

maralorn:

Can you make a bit more explicit what you mean with me aiming for “pointfree” style?

The problem with monads for the purpose of static analysis is (from a certain perspective) that the monadic bind function >>= is not point-free. Its second argument could be a lambda that binds a variable. Switching to (Kleisli) categories means you only allow function composition and identity functions (both pointfree). Strong and Choice are similarly pointfree. The Arrow class allows lifting pointful functions to your category, but they are confined to the arr method (and even this confinement is not enough for all analyses as you write in your comment).

The arrow syntax does find a nice subset of syntax where the compiler can translate pointful programs to the pointfree arrow style, but this introduces a non-trivial translation which in my opinion complicates everything. For example, it is impossible to (exactly) pretty print programs written in arrow notation to their original syntax.

Instead, I think we should just reckon with overloaded variable binding once and for all and avoid the complicating pointfree translation.