Ongoing work on Supercompilation of Java code (or supercompilation in general)?

I was intrigued by this description of a technology for "supercompiling" Java code.

But I notice that a lot of the information on that website appears to be "stale", and hasn't been updated for a few years.

Is anyone aware of the current state of research on supercompilers, especially as it relates to Java?

Regards,

Ian.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Slightly off-tangent

Not too Java specific except that the compiler is written for a JVM language: A Small Positive Supercompiler in Scala. The language it compiles is a simple first order functional language - so no Java relationship there. Clicking through leads to some references including one online PDF.

A Higher-Order Supercompiler in Scala

Now there is also a next project
A Higher-Order Supercompiler in Scala.

Online supercompiler

The best part is the interactive web environment.

Supero

There's an actively developed supercompiler for Haskell named Supero by Neil Mitchell

Can it educate people?

It would be interesting to learn from the supercompiler what the patterns of inefficiencies are and what the suggested solutions are, so when writing code in the first place one could maybe do things in the more efficient style. Unless, of course, those inefficiencies are required to keep things architected/designed/implemented such that humans can maintain and extend the system.

You ask that like it's a good thing

Super-compilers are the masters of copy-and-paste, special purpose code. So you probably don't really want most coders trying to learn from them. A sad proportion of developers learns this style of coding just fine without help, thank you very much.

I see

oh well. the way some of the stuff i looked at read, it sounded like maybe it reconfigured things to be more succinct or something, rather than just being a big inliner :-) for sure wish to avoid more crappy coding by humans!

Not just inlining, I believe

Not just inlining, I believe supercompilation incorporates fusion, partial evaluation, and a host of other techniques.

including

Yes, including inlining, partial evaluation, fusion, and deforestation as special cases. And this is only if you restrict to supercompilation as described by M.H. Sørensen, R. Glück, N.D. Jones in A Positive Supercompiler. At least some of the examples in Hutton's The worker/wrapper transformation can be arrived at directly by supercompilation of the change of representation.

I think Turchin's idea is more general. I think he may have been talking about decidable fragments of Generalised Partial Computation.

Supercompilation can also be used as a proof method with a little bit of auxiliary logic which performs a sort of abstract interpretation on the resultant functions. A simple example is

 
foo Z = True
foo S x = foo x

This function is terminating and only returns True, so it's application to any integer can be replaced with True. These sorts of functions can result from supercompilation of expressions.

This paper: Poitín: Distilling Theorems From Conjectures has descriptions of how supercompilation can be used as an automated proof technique.

I was unable to find a free

I was unable to find a free version of the Poitín paper referenced above.

However, this paper seems to include most of the transformations used for the theorem proving though, but may be missing some comentary:
Extending Poitin to Handle Explicit Quantifiers

Supercompilation as proof assistance

Here's an interesting blog post where the author uses manual supercompilation to prove that that an implementation of a monad has some of the correct algebraic properties. Verifying the Monad Laws with Supercompilation.