🚀 go-pugleaf

Belated Reply To:

| >From: nelan@enuxha.eas.asu.edu (George Nelan)
| Ok, here's a summary of responses to my posting:

| I'm looking for references to work done on *transforming* higher-order
| functional programs to first-order.  Can anyone help?  E-mail: sufficient
| interest -> will post.  Thank you for your support.
|-------------------------------------------------------------------------------
| From: Paul Kelly <phjk%doc.imperial.ac.uk@NSFnet-Relay.AC.UK>
| 
| A research student here called Chin is just finishing a thesis which includes
| work on this, and has associated papers.  I suggest you email him, "wnc"

That's me! 

| Here is part of the abstract of a term paper I recently finished for a class in
| verification and transformation taught by one of my PhD advisors, Ed Ashcroft.
| The paper is titled "From Higher Order To First Order":
|
|       "Claim: an algorithm is presented that transforms most finitely typed
|	flattened higher order functional programs into equivalent first order
|	programs.  A finitely typed program is, in simple terms, a program that
|	passes (for instance) the type checking algorithm of Miranda or Haskell;
|	......
===============================================================================

My recent PhD thesis, entitled "Automated Methods for Program
Transformation", contains a chapter on higher-order removal. My
result appears to be quite similar (maybe you can confirm this)
to your above claim as it also removes 'most but not all higher-order 
features' and works with only 'well-typed' (or finitely typed) programs.

To structure the higher-order removal transformation, I have broken down 
the transformation into three algorithms. These transformation algorithms are
based on the define/unfold/fold rules of [Burstall&Darlington77] and serve 
the following purposes
	(1) remove 'general' applications
	(2) remove most of the instantiated (non-variable)
	    higher-order arguments
	(3) preserve laziness
Brief descriptions of these three algorithms (using examples)
follow. Note that the examples are based on an uncurried language (Hope-like).
I find 'uncurried' programs to be easier to deal with in unfold/fold
transformations because all parameter arguments are always present for
unfolding.

(1) Remove 'general' applications.
---------------------------------
This is similar (or identical) to what a number of people have
described as 'eta-abstraction'. Lester [Lester89] used this
transformation to simplify his stacklessness analysis.

For example, given:
	prg(u)	= inc(u)(4)
	inc(x)	= lambda y => y+4 end
The 'general' application, inc(u)(4), could be removed by transforming
(in this case just unfolds) to:
	prg(u)	= u+4

'General' applications (in an uncurried program) are terms of the form,
 fid (t1,..,tn)..(ty,..,tz), where fid is a function identifier and each
tx is an argument term. 'Function' applications are terms of the form
fid (t1,..,tn), while 'Variable' applications are terms of the form
v (t1,..,tn)..(ty,..,tz) where v is a variable. These are my terminologies
(apologies to anyone who have defined them differently), and I have shown
that all 'general' applications (in well-typed programs) could be 
eliminated (converted to function applications) by a simple transformation
algorithm. This may perhaps be what you mean by 'flattenning'.

(2) Remove 'instantiated' higher-order arguments
------------------------------------------------
Given a higher-order program:
	f(x)		= alt_map(x,lambda a=>a*a end,lambda a=>a*a*a end)
	alt_map([],F,G)	= []
	alt_map(x:xs,F,G)= F(x):alt_map(xs,G,F)
The second transformation algorithm will remove the 'instantiated'
higher-order function call in f by transforming it to:
	f([])	= []
	f(x:xs)	= x*x:f'(xs)
	f'([])	= []
	f'(x:xs)= x*x*x:f(xs)
This transformation is a form of function specialisation (or partial
evaluation) which specialises function calls with instantiated 
higher-order arguments. We have to be careful which of the higher-order
arguments we are allowed to specialise for recursive functions. If we are not
careful, we may get a non-terminating transformation algorithm. The parameter
criterion I used to determine if an argument can be specialised or not
is called, the 'variable-only' criterion. For example, the above
alt_map function contains two higher-order parameters, F and G, which are
both 'variable-only'. This is so because the corresponding recursive call, 
alt_map(xs,G,F), in the 2nd defining equation of alt_map contains variables 
(constants allowed as well) in those parameter positions.

In contrast, another higher-order function:
	acc_map([],F)	= []
	acc_map(x:xs,F) = F(x):acc_map(xs,lambda a=>a+F(x) end)
does not have any 'variable-only' higher-order parameter. This is because 
its corresponding recursive function call, acc_map(xs,lambda a=>a+F(x) end),
contains an accumulating term, lambda a=>a+F(x) end, in its ho-parameter
position. Such parameters are more difficult to specialise/remove and
may require laws to do so. I have not offered any solutions towards 
the removal of ho-arguments without the variable-only criterion.

3) Preserving Full Laziness
---------------------------

Higher-order parameters which are non-linear may, at times, result in 
loss of efficiency when they are specialised. For example, the map function
below:
	map([],F) 	= []
	map(x:xs,F)	= F(x):map(xs,F)
contains a non-linear higher-order parameter, F (occurred twice in the RHS
of the second equation). As a result, if we were to directly specialise the 
map function call in:
	g(xs,y)		= map(xs,lambda a=>sqr(y)+a end)
we get a less efficient program (note the re-computed sub-term
sqr(y)):
	g([],y)		= []
	g(x:xs,y)	= (sqr(y)+x):g(xs,y)
This issue is related to Wadworth's
full laziness graph reduction technique and Hughes's fully lazy lambda
lifting technique. To avoid this loss of laziness. I formulated a
transformation algorithm which would extract out 'ground-type' maximal
free expressions (MFEs - see [Hughes82]). A ground-type MFE for the 
above example is sqr(y). This could be extracted out to give:
	g(xs,y)		= g'(xs,sqr(y))
	g'(xs,Y)	= map(xs,lambda a=>Y+a end)
before g' is specialised to:
	g'([],Y)	= []
	g'(x:xs,Y)	= (Y+x):g'(xs,Y)
We are interested in extracting only ground-type MFEs and not function-type 
MFE. This is because the extraction of function-type MFEs, e.g. + sqr(y),
actually introduces (rather than remove) ho-functions - contradicting 
with the goal of ho-removal transformation. 

The laziness preserving transformation is quite complex because we may need to
extract out deeply 'buried' ground-type free expressions. I shall not go into
details here. The transformation algorithm can be found in my thesis and 
in a paper I am currently revising (e-mail me for details).

Additional Issues
-----------------

The transformation algorithms described are correct because they are based
on unfold/fold and satisfies Scherlis/Kott's total correctness criterion.
In addition, I have also proved the termination of these transformation
algorithms. The proof relied on the fact that programs are well-typed. An 
informal explanation for this well-typed requirement (to ensure termination)
is that the essence of the ho-removal algorithms is to reduce
the 'order' of programs. As well-typed programs have finite 'order', they
could always be transformed/removed within a finite number of iteration steps 
by the algorithm.

Lastly, the above algorithms does not directly eliminate list/trees of
function elements. However, when they are combined with an extended form
of Wadler's deforestation algorithm [Wadler88], we have a more 
powerful technique which is able to eliminate list/trees of functions. 
This is interesting because (in the opposite direction) we are using 
the higher-order removal technique to  help extend Wadler's first-order 
deforestation algorithm to higher-order programs. 

Related Works
-------------

[Goguen88] and [Wadler88] both proposed a macro expansion (unfolding) technique
to remove a restricted class of higher-order functions. More
specifically, their technqiue could be applied to higher-order functions 
whose function-type parameters are 'fixed' (e.g. map function above 
but not alt_map nor acc_map).

[Nielson&Nielson89] proposed the higher-order function removal 
transformation as a special form of partial evaluation 
with the help of BTA (Binding-time analysis).
I think their proposed technique is presently only able to handle
the removal of function-type arguments without free variables.

References
----------
[Burstall&Darlington77] A Transformation System for Developing 
		recursive programs, JACM 1977
[Goguen88] Higher-Order Functions considered Unnecessary for Higher-order
		Programming, SRI-CSL-88-1
[Lester89] Stacklessness: Compiling Recursion for a Distributed Architecture
		FPCA '89
[Hughes82] Supercombinators: A new implementation technique for Applicative
		Languages ACM LFP 1982
[Nielson&Nielson89] Transformation on Higher-order Functions FPCA'89.
[Wadler88] Deforestation - Transforming Programs to Eliminate Trees,
		ESOP '88
==========================================================================

..WN Chin
Dept of Computing, Imperial College

PS I have not yet implemented the described transformation techniques.