Generative Folding/Unfolding


Identity: FoldingGen
Category: MultiModule Naming
Classifiers: generative folding specialisation expression definition recursion
Internal cross references:
External cross references: XXX
Language: Haskell

Description:

Replace an instance of the right hand side of a definition by the corresponding left hand side, creating a new recursive definition.


format :: [a] -> [[a]] -> [[a]]
format sep xs
  = if len xs < 2 
       then xs
       else (head xs ++ sep) : format sep (tail xs)

{- fmt = format "\n", after unfolding -}

fmt xs
  = if len xs < 2 
       then xs
       else (head xs ++ "\n") : format "\n" (tail xs)

format :: [a] -> [[a]] -> [[a]]
format sep xs
  = if len xs < 2 
       then xs
       else (head xs ++ sep) : format sep (tail xs)

{- fmt = format "\n", after unfolding and 
   generative fold against the original definition. -}

fmt xs
  = if len xs < 2 
       then xs
       else (head xs ++ "\n") : fmt (tail xs)

General comment:

The refactoring here is different in nature to other structural refactorings. The transformation in the example uses the original definition of fmt, namely:

fmt = format "\n"
from right to left to create a new recursive definition of fmt. The fold takes place in the unfolded version of the definition, however. The two versions of the definition of fmt cannot coexist in the same Haskell module. The original definition therefore needs to be retained in some form.

Left to right comment:

In the example, the structure of the program is changed, and this can potentially modify the termination of the function. In an extreme case, consider folding the equation

fmt = format "\n"
against itself. This produces the equation
fmt = fmt
which whilst it is a true property of fmt fails to give the same definition of the fmt function; instead it makes it everywhere undefined.

Right to left comment:

This is indistinguishable from the inverse of simple folding.

Left to right conditions:

The conditions for simple folding also apply here.

It is also a requirement that the new definition has the same termination property as the original. This can be verified from the form of the definition in many cases.

Right to left conditions:

The conditions for simple unfolding also apply here.

Analysis required: Static analysis of bindings; call graph. If the folding is to be totally correct, termination analysis is required.