Refactoring in Tunes

[Francois-Rene Rideau]

I'd like to intervene in this thread about "Refactoring".
As I understand it, refactoring is just a very particular case of
metaprogramming, with lots of hype around, and meant to be done manually only
(because hypists follow the C++/Java/OO buzzwagon, where automated
metaprogramming is rendered practically impossible in the presence
of ugly misdesigned dominating languages). I don't mean that works on
"refactoring" are worthless; on the contrary, they might be a huge progress
as compared to no metaprogramming at all (or at least, no formalization
thereof), and they might popularize a few meta-level ideas among programmers.
But this is still all too far away from what we'd expect a development system
to (help us) do.

For any "refactoring" trick, you can find a decomposition of it into
nice and general metaprogramming rules. Massimo already talked about
lambda-abstraction and beta-expansion: concepts indeed difficult to
express if at all in languages such as C, C++, Java, but trivial in
functional programming languages such as LISP, FORTH, ML, Haskell, etc.
The fact that such operations be done before runtime leads us in the realms
of "partial-" or staged evaluation. Combining them leads us to substitution,
and finding the right substitution is unification (which can get pretty
difficult for higher-order terms). If you allow for more meta-level
functionality (who talked about differentiating functions to compute
normal vectors for 3D shapes?), then you can "refactor" the code in even
simpler ways; etc.

About "refactoring", I'd like to stress out that what's simple according
to one's point of view isn't as simple according to another one's. And the
"one's" in question might be people trying to understand the program,
people trying to prove it correct, people trying to execute it efficiently
on a given hardware, etc, etc. In as much as "refactorers" keep just one
version of the code at a time, they are not being helpful in having people
with divergent point of views agree on a same program; for that, you have
to be able to manipulate not just the code, but the meta-code, too, so as
to be able to _consistently_ go back and forth between different versions
of your program. Etc, etc.

   Brian> *automating* refactoring.
If you replace "refactoring" by the more general "metaprogramming",
well, you get precisely the whole idea about Tunes.


NB: in another message, Brian says:
> My idea here of a type system is one specified in the manner of predicate
> logic (though not with standard predicate logic only). Subclassing in tunes
> would not be "overridding methods" and "adding variables" but specifying a
> type that obeys more specifications.
According to some class formalisms, adding variables and methods _is_
adding more specifications. Overriding existing methods is still a
non-monotonous operation, though, unless you provide a proof of refinement
(but then it's no more really an evil OO class hierarchy, but a good old
refinement calculus).

[ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!   http://www.tunes.org/  ]
[ FR: François-René Rideau | TUNES is a Useful, Nevertheless Expedient System ]
[ Reflection&Cybernethics  | Project for  a Free Reflective  Computing System ]
You don't test the validity of a theory by seeing that it says correct
things, but by seeing that it doesn't say incorrect things. What you test
by seeing that it does say correct _and previously unpredicted_ things,
is the interest of a theory you've tested to be valid.