Homomorphic static analysis

There are two concerns:

1. Finding an abstraction that can capture the semantics that we want to express.
2. Being able to write it with nice syntax.

For point 1 I think normal ASTs like the Program data type in one of my previous comments fits the bill (perhaps with more type safety but that is a solved problem for simple types). If you want it to be overloadable you can make use the “Tagless-Final” style, but I don’t care much for that.

I think the only reason this is not a standard approach is because of point 2: GHC does not have a nice syntax for it. You can get far with RebindableSyntax, but you run into a wall when you have language constructs which bind variables: lambda, let, and case expressions. Those are all pointful and I assume that is the reason why they are not rebindable yet. With reckoning with variable binding, I mean that we should just choose a representation and make these things rebindable too. I don’t think it is very hard to do that, but I also don’t think there is a nice category theoretic abstraction to capture these variable-binding constructs.