text:
# Strategic polymorphism requires just two combinators!

## 1 Introduction

In , we introduced the notion of *functional strategies* for which we assume the following matured definition throughout this paper:

###### Definition 1

Functional strategies are functions that

1. are generic,
2. can mix uniform and type-specific behaviour,
3. can traverse terms, and
4. are first-class citizens.

Functional strategies go beyond parametrically polymorphic functions because of the abilities to traverse terms and to dispatch to type-specific behaviour. We call this extra polymorphism simply ‘strategic polymorphism’. In the present paper, we will capture strategic polymorphism by just two fundamental function combinators. Most of our presentation will avoid commitment to a specific functional language, but we ultimately define a Haskell-based reference model.

Functional strategies were derived from the notion of (typed) term rewriting strategies . In fact, the notion of (traversal) strategies can be amalgamated with different programming paradigms. We use the term *strategic programming* for generic programming with strategies in whatever language. It is at the heart of strategic programming that traversal schemes are programmer-definable. The native application domain of strategic programming is language processing, in particular, the implementation of functionality for program transformations and analyses; see  for a few typical applications. With strategies, one can operate on large syntaxes or formats in a scalable and flexible manner. Scalability is implied by genericity, and flexibility by a combinator style that enables the definition of appropriate traversal schemes. In fact, the ability to traverse terms while mixing uniform and type-specific behaviour is beneficial in almost every non-trivial software application. This is demonstrated in , where an approach to *general purpose generic programming* is based on original expressiveness for ‘strategic polymorphism’.

Our efforts to amalgamate strategic and functional programming are scoped by the Strafunski project.111Strafunski home page: http://www.cs.vu.nl/Strafunski/ — Stra refers to strategies, fun refers to functional programming, and their harmonious composition is a homage to the music of Igor Stravinsky. Distributions of the Haskell-centred Strafunski bundle for generic programming and language processing include generative tool support that, given the programmer-supplied datatypes, generates the code needed for strategic programming. In previous work, we came up with different models of functional strategies . These models differ regarding the selection of primitive combinators and their types, but they all share Haskell as the base language.

In the present paper, we capture strategic polymorphism by just two combinators:

* $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ for type-based function dispatch, and
* $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ for folding over constructor applications.

The combinator couple $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ was identified in , and a very similar couple was employed in .222There are tiny technical differences. In , first-class polymorphism is employed as opposed to proper rank-2 function types in the present paper and in . Also, in , type cast is favoured as opposed to function dispatch in the present paper and in . Furthermore, in , a left-associative fold combinator is used as opposed to the right-associative combinator in the present paper and in . In the present paper, we use these two combinators for a very compact and matured reconstruction of functional strategies. Our goal here is to avoid an invasive commitment to Haskell. Also, we want to clearly maintain the link to strategic programming as it was initiated in the context of term rewriting. The above two combinators can be mapped to Def. 1 as follows. The combinator $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is crucial for mixing uniform and type-specific behaviour. It can be considered as a disciplined form of type case. The combinator $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ is the mother of all (one-layer, i.e., non-recursive) traversal. It folds over the immediate subterms of a constructor application — very much in the style of a list fold. This turns traversal schemes into programmable entities where ordinary recursive function definition suffices to complete folding into recursive traversal.

The paper is structured as follows. In Sec. 2, we approach to the essential expressiveness for strategic polymorphism via a motivating example. In Sec. 3, we define the two key combinators for strategic polymorphism. In Sec. 4, we discuss models of functional strategies. Sec. 3 and Sec. 4 are largely language-independent. In Sec. 5, we provide a reference model to extend Haskell with our two combinators. In Sec. 6, we demonstrate the power that results from our language extension by reconstructing representative parts of Strafunski’s library. In Sec. 7, the paper is concluded.

## 2 Strategic polymorphism — a motivating example

We choose a simple but challenging example that demonstrates all the characteristics of functional strategies. We will define a combinator $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ with an argument $`f`$, such that $`\mathrm{𝑞𝑢𝑒𝑟𝑦}f`$ performs a top-down, left-to-right traversal to find a subterm that can be processed by $`f`$ so that a value is extracted from the subterm. A suitable subterm has to meet two criteria. Firstly, its type must coincide with the domain of $`f`$. Secondly, $`f`$ applied to the subterm should not fail, that is, it should not return $`\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔}`$.

This is the Haskell type of the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator:

|  | $`\mathrm{𝑞𝑢𝑒𝑟𝑦}\mathit{::}\alpha \beta u.(\mathrm{𝑇𝑒𝑟𝑚}\alpha ,\mathrm{𝑇𝑒𝑟𝑚}\beta )`$ |
| --- | --- |
| $`(\alpha \mathrm{𝑀𝑎𝑦𝑏𝑒}u)`$ | – Recogniser / extractor |
| $`\beta `$ | – Input term |
| $`\mathrm{𝑀𝑎𝑦𝑏𝑒}u`$ | – Found entity (if any) |

There are three universally quantified type parameters:333For the purpose of a homogeneous notation, we always use *explicit* (top-level) universal quantification in all Haskell type signatures. Note: the type of $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ is just a plain rank-1 type, that is, all type variables are indeed quantified at the top-level. We will later also employ rank-2 types, and thereby go beyond Haskell 98. Rank-2 types make *explicit* quantification mandatory. So we decide to switch to explicit quantification all-over the place.

* $`\alpha `$ denotes the type of ‘relevant’ subterms from which a value is extracted.
* $`\beta `$ denotes the type of the term that is eventually passed to $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$.
* $`u`$ denotes the type of the extracted value.

The first argument of $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ is a function of type $`\alpha \mathrm{𝑀𝑎𝑦𝑏𝑒}u`$ that is meant to interrogate subterms of type $`\alpha `$ to extract a value of type $`u`$. The second argument is the input term of type $`\beta `$. The result type of $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ is the extracted value $`u`$ (if any), wrapped in the partiality monad $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$. There are two class constraints $`\mathrm{𝑇𝑒𝑟𝑚}\alpha `$ and $`\mathrm{𝑇𝑒𝑟𝑚}\beta `$ which point out that $`\alpha `$ and $`\beta `$ are place-holders for term types. The Haskell type class $`\mathrm{𝑇𝑒𝑟𝑚}`$ hosts expressiveness for ‘strategic polymorphism’, that is, basically the two combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ as we will say later.

Before we describe the actual definition of $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$, let us first point out that this sort of function is useful for all kinds of scenarios in program transformation and analysis:

* Query the type of an abstraction. For instance, from a Java class declaration one may want to retrieve the signature of a method with a given name.
* Query the definition of an abstraction. For instance, from an XML DTD, one may want to retrieve the content specification of a declared element type.
* Query the focused entity in the course of refactoring. For example, from a Cobol program, one may want to retrieve a focused group of data description entries.

One can easily think of numerous variations on $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ that are equally useful, e.g., implementing bottom-up search, or transforming terms rather than querying them, and so on.

Let’s turn to the Haskell definition of the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator:

|  |  | $`\mathrm{𝑞𝑢𝑒𝑟𝑦}fx`$ |
| --- | --- | --- |
| $`=\mathrm{𝐜𝐚𝐬𝐞}\overline{)\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}}(\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔})fx\mathrm{𝐨𝐟}`$ | – Attempt $`f`$ |
| $`\mathrm{𝐽𝑢𝑠𝑡}u\mathrm{𝐽𝑢𝑠𝑡}u`$ | – Done |
| $`\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔}\overline{)\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}}(\mathrm{𝑞𝑢𝑒𝑟𝑦}f)x`$ | – Recurse |

We boxed the two combinators that involve strategic polymorphism. ($`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}`$ is a type-specialised variant of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$, and $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ is defined in terms of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ as we will show later.) For clarity, their names end on “*MTU*” to remind us of the strategy type at hand: *M*onadic *T*ype-*U*nifying. Monadic style is in place here because of the partiality of querying. By ‘type unification’ we mean that querying returns a value of a specific type, regardless of the type of the input term. The combinator $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}`$ is used to attempt an application of $`f`$ to the input term $`x`$. The composed function behaves like the polymorphic function $`\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔}`$ passed as the first argument to $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}`$ except for the type $`\alpha `$ handled by the function $`f`$. If the attempt to apply $`f`$ results in a value $`u`$ (first branch of case), the search is done, and $`u`$ is returned. Otherwise (second branch of case), the combinator $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ is used to call $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ recursively on the children of $`x`$, i.e., its immediate subterms. The $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ combinator is meant to attempt application of its argument to each child in left-to-right order, and returns the result of the first application that succeeds. We will later see that $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ is just one example of many ‘one-layer’ traversal combinators — they can all be defined in terms of the fundamental combinator $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$.

To summarise, the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator illustrates all characteristics of strategies (recall 1.–4. in Def. 1):

1. The aspect that the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator is *generic*, i.e., applicable to *all* term types, is expressed by the universally quantified $`\beta `$ in its type.
2. The aspect that the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator *mixes uniform and type-specific behaviour* is reflected by the application of the combinator $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}`$.
3. The aspect that the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ combinator *traverses* the input term is reflected by the recursive definition of $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ in terms of the traversal combinator $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$.
4. The *first-class* status of functional strategies is illustrated by their featuring as combinator arguments (cf. the first argument of $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑀𝑇𝑈}`$ and $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$).

We refer the reader to  for many more examples of strategic polymorphism. The present example has been carefully chosen to cover all aspects of strategic polymorphism, and to be representative for strategic programming.

## 3 Just two combinators for strategic polymorphism

In the sequel, we define the two combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ for strategic polymorphism. The definition is language-independent. We use a semi-formal style for the semantics of the combinators, and we use rank-2 types to assign types to the combinators. The interested reader is referred to  for a formal definition of typed rewriting strategies in a basically first-order and many-sorted term-rewriting setting. The below definition makes heavy use of higher-orderness and polymorphism. This is the key to capturing strategic expressiveness in just two dedicated combinators as opposed to the several combinators in previous work.

### The $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ combinator for type-based function dispatch

We want to give a single definition of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$, which is valid for all different types of functional strategies (think of querying vs. transformation). So we assume the general type scheme $`\overline{}\alpha .\alpha c\alpha `$ for functional strategies. Here, $`c`$ is a type constructor that derives the co-domain of the function type from the domain $`\alpha `$. If we instantiate the co-domain constructor $`c`$ with the identity type constructor (i.e., $`I\alpha =\alpha `$), we obtain the type of type-preserving strategies. The constant type constructor (i.e., $`Cu\alpha =u`$) handles the type-unifying scheme (i.e., the result type is always $`u`$ regardless of the input type $`\alpha `$). We use an over-lined version $`\overline{}`$ of the universal quantifier $``$ to distinguish ‘strategic polymorphism’ from ordinary parametric polymorphism.

$`\begin{array}{c}\begin{array}{cccc}\mathrm{𝑎𝑑ℎ𝑜𝑐}\hfill & :& c.\hfill & \text{– Co-domain constructor}\hfill \\ & & \overline{}\beta .\hfill & \text{– Term type of specific functionality}\hfill \\ & & (\overline{}\alpha .\alpha c\alpha )\hfill & \text{– Generic default}\hfill \\ & & (\beta c\beta )\hfill & \text{– Type-specific ad-hoc case}\hfill \\ & & (\overline{}\gamma .\gamma c\gamma )\hfill & \text{– Constructed strategy}\hfill \end{array}\hfill \\ \\ \mathrm{𝑎𝑑ℎ𝑜𝑐}pmx=\{\begin{array}{cc}mx,\hfill & \text{if}\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}(x)=\mathrm{𝑑𝑜𝑚𝑂𝑓}(m)\hfill \\ px,\hfill & \text{otherwise}\hfill \end{array}\hfill \end{array}`$ \[i\]

The placing of the various $`\overline{}`$ quantifiers in the (rank-2) type of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ emphasises that the combinator constructs a polymorphic function from a polymorphic function argument $`p`$ and a monomorphic function argument $`m`$.444Reminder: $``$/$`\overline{}`$ quantifiers expand to the right as far as possible. Lifting the $`\overline{}\gamma `$ to the top of the function type would be acceptable, because $`\overline{}\gamma `$ is placed on the right of the outermost $``$, and hence, lifting leads to an equivalent type. By contrast, moving the inner $`\overline{}\alpha `$ to the top would lead to a too liberal function that also accepted monomorphic arguments for $`p`$. Dually, pushing the $`\overline{}\beta `$ to the second argument (where it is used) would lead to a too restrictive function that insisted on polymorphic ad-hoc cases for $`m`$ instead of type-specific functionality. In the definition, the expressions $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}(x)`$ and $`\mathrm{𝑑𝑜𝑚𝑂𝑓}(m)`$ denote the *specific* type of $`x`$ and the *specific* domain of $`m`$, i.e., the respective types to which $`\gamma `$ and $`\beta `$ are instantiated *at run-time*. So, following this definition, $`\mathrm{𝑎𝑑ℎ𝑜𝑐}pmx`$ dispatches to the monomorphic $`m`$ if $`m`$ is applicable to the $`x`$ at hand, but otherwise it resorts to the polymorphic, generally applicable $`p`$.

In strategic programming, the common usage of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is to derive *generic* ‘rewrite steps’ from *type-specific* ones . The monomorphic ingredient $`m`$ is then a function which rewrites terms of a specific type, potentially based on pattern matching, whereas the polymorphic ingredient $`p`$ provides a trivial generic default. As a simple example, consider the following polymorphic function $`\mathrm{𝑛𝑒𝑔𝑏𝑜𝑜𝑙}`$ which behaves like the identity function by default but applies Boolean negation “$`\neg `$” when faced with a Boolean:

$$\begin{array}{c}\mathrm{𝑛𝑒𝑔𝑏𝑜𝑜𝑙}=\mathrm{𝑎𝑑ℎ𝑜𝑐}\mathrm{𝑖𝑑}(\neg )\hfill \end{array}$$

For this type-preserving strategy, the co-domain type constructor $`c`$ is instantiated to the identity type constructor $`I`$. In our $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ sample, $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ was used to construct a type-unifying generic rewrite step “$`\mathrm{𝑎𝑑ℎ𝑜𝑐}(\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔})f`$”. Here, the co-domain constructor $`c`$ is instantiated to the constant type constructor $`C`$. The generic default $`\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑁𝑜𝑡ℎ𝑖𝑛𝑔}`$ models the failure of the $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$. The function $`f`$ interrogates terms of a certain type to extract a $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ value.

### The $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ combinator for folding over constructor applications

Let us recall the basic idiom of list traversal. Without loss of generality, we consider *right-associative* list traversal. Folding a list $`[x_1,x_2,\mathrm{},x_n]`$ according to ingredients $`f`$ and $`z`$ for the non-empty and the empty list form is defined as usual:

$$\begin{array}{c}\mathrm{𝑓𝑜𝑙𝑑𝑟}fz[x_1,x_2,\mathrm{},x_n]=fx_1(fx_2(\mathrm{}(fx_nz)\mathrm{}))\hfill \end{array}$$

Folding over constructor applications is similar: instead of folding over the elements of a homogeneous list, we fold over the children of a term, i.e., its immediate subterms. Since the children of a term are potentially of different types, we need a *heterogeneous* fold. So we use the name $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$. Without loss of generality, we assume *curried* constructor applications. Folding a term $`Cx_n\mathrm{}x_2x_1`$ is now defined as follows:

$`\begin{array}{c}\begin{array}{cccc}\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}\hfill & :& c.\hfill & \text{– Co-domain constructor}\hfill \\ & & (\overline{}\alpha \beta .\alpha c(\alpha \beta )c\beta )\hfill & \text{– ‘cons’ case}\hfill \\ & & (\gamma .\gamma c\gamma )\hfill & \text{– ‘nil’ case}\hfill \\ & & (\overline{}\delta .\delta c\delta )\hfill & \text{– Constructed strategy}\hfill \end{array}\hfill \\ \\ \mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}fz(Cx_n\mathrm{}x_2x_1)=fx_1(fx_2(\mathrm{}(fx_n(zC))\mathrm{}))\hfill \\ \hfill \end{array}`$ \[ii\]

The indices in $`Cx_n\mathrm{}x_2x_1`$ clarify that we treat the children in the curried expression as a ‘snoc list’ with the rightmost child as ‘head’. Also note that the empty constructor application $`C`$ is passed to $`z`$ so that the constructor can contribute to the result of folding. The type of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ is somewhat involved, especially regarding the argument $`f`$. Here, $`\alpha `$ denotes the type of the current head $`x_i`$, i.e., the next subterm, and $`\beta `$ denotes the type of a fragment of $`Cx_n\mathrm{}x_i`$. The type $`c(\alpha \beta )`$ denotes the recursively processed tail, and it reflects that this tail lacks the $`i^{\mathrm{𝑡ℎ}}`$ child of type $`\alpha `$. The type of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$’s argument $`z`$ of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ is less of a headache. Since $`z`$ is meant to process constructors, the $`\gamma `$ in its type denotes the type of the constructor $`C`$, applied to no children.

This folding operation is now sufficient to define arbitrary *one-layer* traversal combinators which in turn can be completed into recursive traversal schemes in different ways. In the sample section, we assumed a one-layer traversal combinator $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ which can now be defined concisely as follows:

$`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}s`$ $`=`$ $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}(\lambda htt\mathrm{`}\mathrm{𝑚𝑝𝑙𝑢𝑠}\mathrm{`}sh)(\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑚𝑧𝑒𝑟𝑜})`$
Here we assume an extended monad with operations $`\mathrm{𝑚𝑝𝑙𝑢𝑠}`$ for a kind of choice, and $`\mathrm{𝑚𝑧𝑒𝑟𝑜}`$ for failure. The $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ monad is a typical representative of this class of monads. The definition states that the argument strategy $`s`$ is applied to the head $`h`$ of the constructor application, and $`\mathrm{𝑚𝑝𝑙𝑢𝑠}`$ is used to combine the recursively processed tail $`t`$ and the processed head. Folding starts from $`\mathrm{𝑚𝑧𝑒𝑟𝑜}`$. In Sec. 6, we will provide definitions of more one-layer traversal combinators, and we derive several typical recursive traversal combinators — just in the same way as $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ was derive from $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ by means of ordinary recursive function definition.

## 4 Implementational models — a detailed analysis

The two combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$, which capture strategic polymorphism, can be modelled in several ways. In this section, we will analyse the dimensions of this design space for implementation. This also allow us to refer to the large body of related work on generic programming. The exploration will avoid commitment to a specific functional language. This will clarify that different typed functional languages can be made fit for strategic programming, e.g., Clean, Haskell, and SML.

#### Models at a glance

As with any generic functionality, there are three ways to enable functional strategies in a given language:

The combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ are implemented as language primitives.

They are defined in terms of already available expressiveness.

They are defined using a term interface which is implemented per datatype.

Let us make some important side remarks regarding these overall approaches. The built-in option is the preferred one but it requires changing the language and its implementations. The defined option may fail to be faithful or may require inconvenient encodings, depending on the given expressiveness (as demonstrated below). To be practical and scalable, the per-type option needs generative tool support to implement the term interface per datatype. If the generative component becomes an integral part of the language implementation (as is the case for other generic functionality, e.g., equality predicates in SML and Haskell 98 ), the per-type option evolves into the built-in option.

Whichever option is chosen, another seven dimensions span a design space:

How to query type information and how to perform coercion?

How to generically destruct and construct terms?

How to *apply* a strategy to an actual term?

How to separate strategic and parametric polymorphism?

How to rank the types of strategy combinators?

How to deal with eager vs. lazy reduction and with effects?

How to maintain separate compilation?

#### The type-reflection dimension

Type-based function dispatch ($`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$) assumes some *type information* at run-time. In addition, *coercion* of type-specific cases is needed to apply them to terms encountered at run-time. Dynamic typing  provides expressiveness to define $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$. Then, the terms that are processed by strategies had to be of type Dynamic, and $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is implemented by ‘dynamic type case’ for type matching and coercion. (There are few language implementations with built-in support for dynamic typing but Yale Haskell used to support it, and it was recently added to Clean. Per-type support for dynamic typing has been suggested in various ways.) In fact, dynamic typing is more powerful than needed for $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ because it involves the special type Dynamic. A lightweight dynamic-typing approach is to maintain a universe in which all datatypes are embedded . This approach is particularly suited for per-type generative support. Embedding can be performed in two ways: either via a constructor per type , or on the basis of a universal term representation that includes a type *representation* . As an alternative to dynamic typing, one may also consider intensional polymorphism  as a means to define $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$. This is a major language extension. (It is not available in widespread language implementations.) More seriously, this approach is not applicable because all work in the area of intensional type analysis favours *structural* type analysis while our kind of dispatching requires *nominal* type analysis as argued in . This closes the case to define $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ in terms of other expressiveness. As for a built-in $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$, the following approaches are at our disposal. Access to run-time type information can be based on a term representation with type tags . We should note that such tags are in conflict with type erasure. Also, they slightly enlarge the run-time representation of terms, and in turn slow down term manipulation. Alternatively, term constructors can be used to retrieve type information via a mapping from constructors to type tags. Yet another approach is to rely on carrying dictionaries in the sense of type classes  instead of carrying types in the terms themselves. Yet another approach is to rely on run-time type information complemented by unsafe type coercion as discussed in .

#### The term-reflection dimension

The poor man’s way to observe term structure is based on a universal term representation. Here, explosion and implosion functions mediate between the programmer-supplied datatypes and the universal term representation. This expressiveness is usually provided per-type . Folding over constructor applications boils then down to ordinary folding over homogeneous lists of term representations. Note that it is imperative to effectively hide the representation type in order to guarantee ‘implosion safety’ . Then, this approach shines because of its simplicity. Note that implosion and explosion are likely to lead to a performance degradation but the choice of a suitable representation type can limit the depth of term conversion to a traversal’s extent. A built-in definition of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ would entirely avoid this rather indirect style of operating on terms. In fact, built-in support is straightforward: Def. \[ii\] can be defined on any run-time term representation as is. As our Haskell-specific reference model of the upcoming section will demonstrate, term reflection can also be supported elegantly per-type. That is, $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ directly operates on terms on the basis of a per-type implementation of Def. \[ii\]. The most prominent expressiveness to attempt a definition of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ is presumably polytypism  as implemented in PolyP and Generic Haskell. The combinator $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ can indeed be expressed by structural induction on the type for its traversed argument. However, nominal run-time type case as needed for $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is beyond the scope of polytypism. The various constructs to customise polytypic definitions555Cf. ad-hoc definitions for Generic Haskell as of , type-specific instances for derivable type classes  just as for ordinary Haskell type or constructor classes , copy lines and constructor cases  added to Generic Haskell as of . are compile-time means as opposed to a combinator for run-time type-based dispatch. One may also consider recent proposals for generalised pattern-match constructs  to define $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$. Pattern matching is then not restricted to a single type, and a pattern-match case does not insist on a specific constructor. Again, these approaches do not offer type case.

#### The application dimension

Ideally, strategies are plain functions on the programmer’s term types. In fact, this characterises a challenging corner in our multi-dimensional design space. There are the following reasons why strategy application might deviate from function application. (a) Strategies might operate on Dynamic or a representation type in the interest of type and/or term reflection. (b) Strategies might be wrapped inside datatype constructors for reasons of opaqueness , or for reasons of rank-2 polymorphism . (c) Strategies might operate on datatypes constructed from term types for reasons of a uniform definition : recall the co-domain constructor $`c`$ in Def. \[i\] and Def. \[ii\]. This constructor will be normally a proper datatype because type-level lambdas are hardly supported in functional programming. Strategy application differs for (a)–(c). As for (a), to deal with Dynamic or a representation type, the ordinary terms need to be converted before and after strategy application. For convenience, this can be encapsulated via an overloaded application operator . Then the programmer does not need to provide type tags. As for (b), a corresponding application operator is trivially defined by unwrapping. Basic strategy combinators also need to perform wrapping and unwrapping all-over the place. As for (c), we are saved by the fact that usually only a small number of co-domain constructors are used. Hence, one can specialise the types of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ for these few cases instead of postponing the type adjustment until strategy application. The built-in approach can hide this problem via a closed-world assumption regarding co-domain constructors.

#### The quantification dimension

It is clear that strategies go beyond parametrically polymorphic functions. To reflect this fact, we used $`\overline{}`$ instead of $``$ in Def. \[i\] and Def. \[ii\]. In an actual language design, we can extend the interpretation of the universal quantifier, i.e., we equate our $`\overline{}`$ with $``$. This is common practice for intensional polymorphism. We introduced $`\overline{}`$ for the sake of a clear separation of parametric and strategic polymorphism. Having in mind a per-type approach, we can also introduce explicit type constraints in the sense of ad-hoc polymorphism , as supported by Haskell and Clean, i.e., we equate $`\overline{}\alpha .\mathrm{}`$ with $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{}`$. Thus, the class constraint $`\mathrm{𝑇𝑒𝑟𝑚}\alpha `$ points out where we go beyond parametric polymorphism. A built-in approach does not rely on type classes or class constraints.

#### The ranking dimension

To enable the combinator style of strategic programming, it is indispensable that strategy combinators consume polymorphic arguments. The most basic example is the $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ combinator which must insist on a polymorphic first argument because it is applied to children of potentially different term types. Normally, the need for polymorphic function arguments necessitates second-order polymorphism  as opposed to ‘simple’ polymorphism with top-level quantification. One can attempt to organise generic traversal in terms of rank-1 expressiveness  but this will rule out the key idioms of strategic programming — in particular one-layer traversal. As an aside, second-order polymorphism is generally avoidable if strategies are weakly typed as functions on a representation type. Some form of rank-2 types (or even higher ranks) are supported in several functional language implementations. A well-understood form is first-class polymorphism  as employed for modelling functional strategies in . First-class polymorphism means to wrap up polymorphic functions as constructor components. This necessitates unwrapping prior to function application. In , we employ rank-2 types (as supported in the current GHC implementation of Haskell) for generic traversal combinators. Regarding the earlier discussion of expressiveness to define our combinators, we should now add that ‘second order’ is also indispensable if existing forms of polymorphism were considered. In particular, polytypism in Generic Haskell  is not second order because polytypic functions cannot involve polytypic function arguments.

#### The reduction dimension

Functional strategy combinators were inspired by term rewriting strategies  which are eager. As for ordinary function application, the eager functional programmer can effectively postpone strategy application by the lazy “$`\mathrm{𝑖𝑓}`$” in the definition of new strategy combinators. When adding the $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ combinator in an eager framework, Def. \[ii\] must be implemented with some care to prevent premature evaluation of applications to subterms. This is not a problem in a straightforward inductive implementation (as opposed to the maybe too eager reading of Def. \[ii\]). There is also no problem with using impure effects such as in SML rather than monadic effects. This is again demonstrated by strategic term rewriting à la Stratego because Stratego supports some effects, e.g., for hygenic name generation or I/O.

#### The modularisation dimension

Strategic programs do not require compile-time specialisation of generic functionality as opposed to polytypic programs. This is because strategic programs operate on the programmer-supplied datatypes only via $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$. These combinators, in turn, either operate on suitable run-time term representations as built-ins, or they are overloaded per-type. Hence, separate compilation is maintainable. Some techniques for type or term reflection might however imply a closed-world assumption. Firstly, the definition of a universe with embedding constructors per type is not extensible unless we assume extensible datatypes. In , we deal with the same problem: type case is encoded in a way that relies on a class member per term type. Separate compilation is also sacrificed when one provides per-type functionality by a ‘monster switch’, that is, by a central authority which would be meant to cover all types as opposed to proper overloading with support for separate compilation.

## 5 A reference model for Haskell

We will now define a Haskell-based reference model for the implementation of the combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$. In view of the previous section, we can provide the following characterisation:

* The reference model relies on per-type functionality.
* Strategies directly operate on the terms of the programmer-supplied datatypes.
* Strategy application is plain function application.

To start with, we define the type scheme for generic functions that model strategies:

|  |  |  | $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha c`$ | $`=`$ | $`\alpha c\alpha `$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}c`$ | $`=`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha c`$ |

These two type synonyms make a distinction between unconstrained, i.e., parametrically polymorphic functions and constrained, i.e., strategically polymorphic functions. The class constraint points out where we go beyond parametric polymorphism. Roughly, the $`\mathrm{𝑇𝑒𝑟𝑚}`$ class hosts our two combinators, but the details follow below. Let us first list the Haskell types of our two combinators:

|  |  |  | $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ | $`\mathit{::}`$ | $`c\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}c\mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha c\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}c`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ | $`\mathit{::}`$ | $`c.\mathrm{𝐻𝐶𝑜𝑛𝑠}c\mathrm{𝐻𝑁𝑖𝑙}c\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}c`$ |

|  |  |  | $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝐻𝐶𝑜𝑛𝑠}c`$ | $`=`$ | $`\alpha \beta .\mathrm{𝑇𝑒𝑟𝑚}\alpha \alpha c(\alpha \beta )c\beta `$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝐻𝑁𝑖𝑙}c`$ | $`=`$ | $`\gamma .\gamma c\gamma `$ |

The two type synonyms above are defined for convenience to make the type of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ more comprehensible. In the types of the combinators, we make use of rank-2 polymorphism as provided by the GHC implementation of Haskell. It remains to define the combinators, to provide the complete declaration of the $`\mathrm{𝑇𝑒𝑟𝑚}`$ class, and to describe the derivation of the $`\mathrm{𝑇𝑒𝑟𝑚}`$ instances. We start with the implementation of Def. \[i\] for $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$. To this end, we assume an operation $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}`$ which maps ‘typeable’ values of any term type to a type representation. Note that this is the kind of mapping that we proposed earlier in order to avoid carrying type information in the terms themselves. The operation $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}`$ is placed in a $`\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}`$ class as follows:

|  | $`\mathrm{𝐜𝐥𝐚𝐬𝐬}\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}\alpha \mathrm{𝐰𝐡𝐞𝐫𝐞}`$ |
| --- | --- |
| $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}\mathit{::}\alpha \mathrm{𝑇𝑦𝑝𝑒𝑅𝑒𝑝}`$ |

The type $`\mathrm{𝑇𝑦𝑝𝑒𝑅𝑒𝑝}`$ models type representations. Furthermore, we assume an operation $`\mathrm{𝑢𝑛𝑠𝑎𝑓𝑒𝐶𝑜𝑒𝑟𝑐𝑒}`$ to cast a value of any type to another type. Then, Def. \[i\] can be rephrased in Haskell as follows:

|  | $`\mathrm{𝑎𝑑ℎ𝑜𝑐}pmx=\mathrm{𝐢𝐟}(\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}x)(\mathrm{𝑑𝑜𝑚𝑂𝑓}m)\mathrm{𝐭𝐡𝐞𝐧}(\mathrm{𝑢𝑛𝑠𝑎𝑓𝑒𝐶𝑜𝑒𝑟𝑐𝑒}m)x\mathrm{𝐞𝐥𝐬𝐞}px`$ |
| --- | --- |
| $`\mathrm{𝑑𝑜𝑚𝑂𝑓}(f\mathit{::}ab)=\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}(\mathit{::}a)`$ |

It is important to notice that the argument of $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}`$ is only used to carry type information via overloading. The assumed two features are readily available in Haskell implementations. Of course, a proper language extension, which offers $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ as a built-in, does not need to expose either $`\mathrm{𝑡𝑦𝑝𝑒𝑂𝑓}`$ or $`\mathrm{𝑢𝑛𝑠𝑎𝑓𝑒𝐶𝑜𝑒𝑟𝑐𝑒}`$. These two operations are folklore in the Haskell community because they form the foundation of the $`\mathrm{𝐷𝑦𝑛𝑎𝑚𝑖𝑐}`$ library, which has been a standard part of Haskell distributions for several years. The folk’s wisdom to derive $`\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}`$ and to perform type-safe cast on top of it with the help of $`\mathrm{𝑢𝑛𝑠𝑎𝑓𝑒𝐶𝑜𝑒𝑟𝑐𝑒}`$ is found in . One can also use other, maybe safer, but also more involved approaches to dynamic typing. Regardless of the specific approach, the important thing to remember is that our implementational model of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ only involves term types but no universe such as Dynamic. This means that $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is very simple in nature, and $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is not inherently dynamically typed.

From the above development it is clear that $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ is indeed defined in terms of per-type functionality for accessing run-time type representations based on overloading. Then, the class $`\mathrm{𝑇𝑒𝑟𝑚}`$ that captures strategic polymorphism has to be constrained by the $`\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}`$ class so that every term type is also known to be typeable. Thus, we have:

|  | $`\mathrm{𝐜𝐥𝐚𝐬𝐬}\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}\alpha \mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝐰𝐡𝐞𝐫𝐞}`$ |
| --- | --- |
| – Completed below |

Def. \[ii\] for the $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ combinator immediately necessitates per-type support because Haskell does not offer any expressiveness to generically observe the structure of terms. We place $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ itself as a member in the $`\mathrm{𝑇𝑒𝑟𝑚}`$ class. In fact, the very comprehensible type of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ from above is not immediately suited for an overloaded class member. So we place a primed member in the class with an equivalent type:

|  | $`\mathrm{𝐜𝐥𝐚𝐬𝐬}\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}\alpha \mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝐰𝐡𝐞𝐫𝐞}`$ |
| --- | --- |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}^{}\mathit{::}c.\mathrm{𝐻𝐶𝑜𝑛𝑠}c\mathrm{𝐻𝑁𝑖𝑙}c\mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha c`$ |

We define $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ simply in terms of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}^{}`$:

|  | $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}\mathit{::}c.\mathrm{𝐻𝐶𝑜𝑛𝑠}c\mathrm{𝐻𝑁𝑖𝑙}c\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}c`$ |
| --- | --- |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}fz=\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}^{}fz`$ |

The type of the primed member uses *implicit* quantification over the class parameter $`\alpha `$. The non-primed version uses *explicit* quantification hidden in $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}`$. The $`\mathrm{𝑇𝑒𝑟𝑚}`$ class exhibits an intriguing feature: it is defined recursively in the sense that the $`\mathrm{𝑇𝑒𝑟𝑚}`$ class itself is used to constrain the signature of its member $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}^{}`$ hidden in $`\mathrm{𝐻𝐶𝑜𝑛𝑠}`$. This can be viewed as a sign of the first-class status of strategies.

The classes $`\mathrm{𝑇𝑒𝑟𝑚}`$ and $`\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}`$ can be now added to the Haskell 98  language definition in the same way as the standard classes $`\mathrm{𝐸𝑞}`$, $`\mathrm{𝑂𝑟𝑑}`$, $`\mathrm{𝑆ℎ𝑜𝑤}`$, and $`\mathrm{𝑅𝑒𝑎𝑑}`$. Just as the Haskell language definition contains a specification of derived instances for these built-in classes, so do we need to complete our extension by specifying the derived $`\mathrm{𝑇𝑒𝑟𝑚}`$ instances. The derivation of the member $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}^{}`$ is completely straightforward. We need to provide one equation per constructor based on the scheme for heterogeneous, right-associative fold according to Def. \[ii\]. That is, given a constructor $`C`$ of type $`\tau `$ with $`n`$ arguments, we need a pattern-match case defined as follows:

$$\begin{array}{c}\mathrm{𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞}\mathrm{𝑇𝑒𝑟𝑚}\tau \mathrm{𝐰𝐡𝐞𝐫𝐞}\hfill \\ \mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}fz(Cx_n\mathrm{}x_2x_1)=fx_1(fx_2(\mathrm{}(fx_n(zC))\mathrm{}))\hfill \\ \text{Continue for the other constructors}\hfill \end{array}$$

This simple scheme is applicable to mutually recursive, parameterised (perhaps over higher-kinded type variables) datatypes. Not even non-uniform recursion is a problem. For all basic datatypes such as $`\mathrm{𝐼𝑛𝑡}`$, we assume instances that apply the nil case. This is also a sensible choice for function types as there is no way to traverse them but it should be safe to encounter them in the course of traversal.

For completeness, we have investigated the option to define our combinators by means of *derivable type classes* as they were proposed for Haskell and Clean . Derivable type classes are precisely meant for the definition of classes for which the instances follow a common scheme. To this end, polytypic patterns for sums and products  are included in the pattern-match syntax for class member definition. The $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ combinator (and hence, the $`\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}`$ class) does not take advantage of derivable type classes because it necessitates a nominal approach rather than structural induction. However, the $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ combinator (and hence, the $`\mathrm{𝑇𝑒𝑟𝑚}`$ class) can be defined as follows:

|  |  |  | $`\mathrm{𝐜𝐥𝐚𝐬𝐬}\mathrm{𝑇𝑦𝑝𝑒𝑎𝑏𝑙𝑒}\alpha \mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝐰𝐡𝐞𝐫𝐞}`$ |
| --- | --- | --- | --- |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}\mathit{::}\mathrm{𝐻𝐶𝑜𝑛𝑠}I\mathrm{𝐻𝑁𝑖𝑙}I\mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha I`$ |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}\{|\mathrm{𝑈𝑛𝑖𝑡}|\}fz\mathrm{𝑈𝑛𝑖𝑡}`$ | $`=`$ | $`z\mathrm{𝑈𝑛𝑖𝑡}`$ |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}\{|\alpha \mathit{:+:}\beta |\}fz(\mathrm{𝐼𝑛𝑙}x)`$ | $`=`$ | $`\mathrm{𝐼𝑛𝑙}(\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}fzx)`$ |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}\{|\alpha \mathit{:+:}\beta |\}fz(\mathrm{𝐼𝑛𝑟}x)`$ | $`=`$ | $`\mathrm{𝐼𝑛𝑟}(\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}fzx)`$ |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}\{|\alpha \mathit{:\ast :}\beta |\}fz(x\mathit{:\ast :}y)`$ | $`=`$ | $`fx(\lambda x^{}x^{}\mathit{:\ast :}\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}fzy)`$ |

There are equations for $`\mathrm{𝑈𝑛𝑖𝑡}`$, $`\alpha :+:\beta `$ (i.e., sums), and $`\alpha ::\beta `$ (i.e., right-associative products). In fact, we only show the special case for the type-preserving scheme where the co-domain constructor is instantiated to the identity type constructor $`I`$.

## 6 Reconstruction of Strafunski

The two simple combinators $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ are sufficient to obtain the full power of strategic programming. We will demonstrate this by the reconstruction of essential parts of the strategic programming library of Strafunski. In fact, all previously published examples of functional strategy combinators  can be reconstructed with the identified primitives.

Normally we distinguish two broad categories of strategies, namely *type-preserving* vs. *type-unifying* ones. In case of the former, input and output term are of the same type. In case of the latter, the output type is fixed regardless of the input type. Another dimension of categorisation arises from the issue of possibly ‘effectful’ traversal. In previous work, all our strategy combinators adhered to monadic style to be prepared for effects such as partiality, environment propagation, and I/O. If no such effect is present, the trivial identity monad can be used to ‘recover’ from monadic style. In the present paper, we explicitly distinguish *monadic* and *non-monadic* strategies. This allows a strategic programmer to resort to the simpler non-monadic types whenever this is sufficient. The variation in the two aforementioned dimensions — type-preservation vs. type-unification, and non-monadic vs. monadic strategies — can be captured by the following Haskell type synonyms:

|  |  |  | $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑇𝑃}`$ | $`=`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \alpha \alpha `$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑇𝑈}u`$ | $`=`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \alpha u`$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝑇𝑃}m`$ | $`=`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \alpha m\alpha `$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝑇𝑈}um`$ | $`=`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \alpha mu`$ |

Note that these strategy types are just instances of the more abstract type $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}`$ which we defined in the previous section. This can be demonstrated as follows:

|  |  |  | $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑇𝑃}`$ | $`=`$ | $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}I`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑇𝑈}u`$ | $`=`$ | $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}(Cu)`$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝑇𝑃}m`$ | $`=`$ | $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}(\mathrm{𝑀𝐼}m)`$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝑇𝑈}um`$ | $`=`$ | $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}(\mathrm{𝑀𝐶}um)`$ |

|  |  |  | $`\mathrm{𝐭𝐲𝐩𝐞}I\alpha `$ | $`=`$ | $`\alpha `$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝐭𝐲𝐩𝐞}Cu\alpha `$ | $`=`$ | $`u`$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝐼}m\alpha `$ | $`=`$ | $`m\alpha `$ |
| $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑀𝐶}um\alpha `$ | $`=`$ | $`mu`$ |

The synonyms $`I`$, $`C`$, $`\mathrm{𝑀𝐼}`$, and $`\mathrm{𝑀𝐶}`$ are Haskell implementations of non-monadic and monadic versions of the identity and constant type constructors. The four broad categories of strategy types are reconstructed by passing one of these type constructors to $`\mathrm{𝑆𝑡𝑟𝑎𝑡𝑒𝑔𝑖𝑐}`$. We assume specialised versions of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ for each of these categories. We postfix the combinators by the corresponding category. These specialised combinators shall be used in strategic code if a specific category is intended.666So we should have used $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑀𝑇𝑈}`$ instead of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ in the definition of $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ in Sec. 3. The specialised combinators for the category $`\mathrm{𝑇𝑃}`$, for example, are declared as follows:

|  |  |  | $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑇𝑃}`$ | $`\mathit{::}`$ | $`\alpha .\mathrm{𝑇𝑒𝑟𝑚}\alpha \mathrm{𝑇𝑃}\mathrm{𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑟𝑖𝑐}\alpha I\mathrm{𝑇𝑃}`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}`$ | $`\mathit{::}`$ | $`\mathrm{𝐻𝐶𝑜𝑛𝑠}I\mathrm{𝐻𝑁𝑖𝑙}I\mathrm{𝑇𝑃}`$ |

These specialisations allow us to maintain “strategy application = function application” in absence of type-level lambdas in Haskell. Recall that the types of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ involve a parameter $`c`$ for co-domain construction. Any instantiation of the combinator types had to use *datatypes* or *newtypes* for $`c`$ as opposed to type synonyms. This is no problem for the category $`\mathrm{𝑀𝑇𝑃}`$ where a monad instantiates $`c`$ but the other categories were defined above via type synonyms for identity and constant type construction. We can easily match up the types of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ with the simple types favoured by the programmer. The trick is to wrap and unwrap extra ‘coaching’ constructors inside the definitions of the specialisations. We illustrate this technique for $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑇𝑃}`$:

|  |  |  | $`\mathrm{𝐧𝐞𝐰𝐭𝐲𝐩𝐞}I^{}\alpha `$ | $`=I^{}\alpha `$ | – The newtype variation on $`I`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑢𝑛𝐼}^{}(I^{}x)`$ | $`=x`$ | – Unwrapping function |
| $`\mathrm{𝑎𝑑ℎ𝑜𝑐𝑇𝑃}fg`$ | $`=\mathrm{𝑢𝑛𝐼}^{}\mathrm{𝑎𝑑ℎ𝑜𝑐}(I^{}f)(I^{}g)`$ | – Specialisation of $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ for $`\mathrm{𝑇𝑃}`$ |

At this point, we have defined all helper types and specialised combinators so that strategic programming can commence. We can define numerous one-layer traversal combinators in terms of $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$, e.g.:

Attempt to process one child; try from left-to-right

|  |  |  | $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ | $`\mathit{::}`$ | $`um.\mathrm{𝑀𝑜𝑛𝑎𝑑𝑃𝑙𝑢𝑠}m\mathrm{𝑀𝑇𝑈}um\mathrm{𝑀𝑇𝑈}um`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}s`$ | $`=`$ | $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑀𝑇𝑈}(\lambda htt\mathrm{`}\mathrm{𝑚𝑝𝑙𝑢𝑠}\mathrm{`}sh)(\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑚𝑧𝑒𝑟𝑜})`$ |

Reduce all children via a monoid

|  | $`\mathrm{𝑎𝑙𝑙𝑇𝑈}\mathit{::}u.\mathrm{𝑀𝑜𝑛𝑜𝑖𝑑}u\mathrm{𝑇𝑈}u\mathrm{𝑇𝑈}u`$ |
| --- | --- |
| $`\mathrm{𝑎𝑙𝑙𝑇𝑈}s=\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑈}(\lambda htt\mathrm{`}\mathrm{𝑚𝑎𝑝𝑝𝑒𝑛𝑑}\mathrm{`}sh)(\mathrm{𝑐𝑜𝑛𝑠𝑡}\mathrm{𝑚𝑒𝑚𝑝𝑡𝑦})`$ |

Map over the children

|  | $`\mathrm{𝑎𝑙𝑙𝑇𝑃}\mathit{::}\mathrm{𝑇𝑃}\mathrm{𝑇𝑃}`$ |
| --- | --- |
| $`\mathrm{𝑎𝑙𝑙𝑇𝑃}s=\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑇𝑃}(\lambda htt(sh))\mathrm{𝑖𝑑}`$ |

Map over the children; monadic variation

|  | $`\mathrm{𝑎𝑙𝑙𝑀𝑇𝑃}\mathit{::}m.\mathrm{𝑀𝑜𝑛𝑎𝑑}m\mathrm{𝑀𝑇𝑃}m\mathrm{𝑀𝑇𝑃}m`$ |
| --- | --- |
| $`\mathrm{𝑎𝑙𝑙𝑀𝑇𝑃}s=\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑀𝑇𝑃}(\lambda htt>>=\lambda t^{}sh>>=\mathrm{𝑟𝑒𝑡𝑢𝑟𝑛}t^{})\mathrm{𝑟𝑒𝑡𝑢𝑟𝑛}`$ |

These examples reconstruct combinators as introduced in . The first combinator, $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$, was already defined in Sec. 3; here, we also provide its type, and we use the specialised combinator $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟𝑀𝑇𝑈}`$ to reflect the kind of strategy at hand. There is a class constraint $`\mathrm{𝑀𝑜𝑛𝑎𝑑𝑃𝑙𝑢𝑠}m`$ because $`\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}`$ finds the suitable child via try and failure. The second combinator, $`\mathrm{𝑎𝑙𝑙𝑇𝑈}`$, uses monoid operations to combine the results of applying the type-unifying argument strategy to all children. The third combinator, $`\mathrm{𝑎𝑙𝑙𝑇𝑃}`$, is a variation on the folklore list $`\mathrm{𝑚𝑎𝑝}`$. The type-preserving argument strategy $`s`$ is mapped over the children of a term. In the case of a non-empty constructor application, $`s`$ is applied to the head $`h`$, and then the result is passed to the recursively processed tail. The empty constructor application is simply preserved via the identity function $`\mathrm{𝑖𝑑}`$. The last combinator, $`\mathrm{𝑎𝑙𝑙𝑀𝑇𝑃}`$, is a monadic variation on $`\mathrm{𝑎𝑙𝑙𝑇𝑃}`$. It uses monadic bind ($`>>=`$) to sequence the applications of the type-preserving argument strategy to all children, and reconstructs the term with the processed children.

Recursive traversal combinators can now be fabricated. The following portfolio provides *traversal schemes* that are parameterised by strategies for node-processing:

Full traversal of all nodes in top-down manner

|  |  |  | $`\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑇𝑃}`$ | $`\mathit{::}`$ | $`\mathrm{𝑇𝑃}\mathrm{𝑇𝑃}`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑇𝑃}sx`$ | $`=`$ | $`\mathrm{𝑎𝑙𝑙𝑇𝑃}(\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑇𝑃}s)(sx)`$ |

Full traversal of all nodes in bottom-up manner

|  |  |  | $`\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑏𝑢𝑇𝑃}`$ | $`\mathit{::}`$ | $`\mathrm{𝑇𝑃}\mathrm{𝑇𝑃}`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑏𝑢𝑇𝑃}sx`$ | $`=`$ | $`s(\mathrm{𝑎𝑙𝑙𝑇𝑃}(\mathrm{𝑓𝑢𝑙𝑙}\mathrm{\dot{}}\mathrm{𝑏𝑢𝑇𝑃}s)x)`$ |

Top-down traversal with cut after success

|  |  |  | $`\mathrm{𝑠𝑡𝑜𝑝}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑀𝑇𝑃}`$ | $`\mathit{::}`$ | $`m.\mathrm{𝑀𝑜𝑛𝑎𝑑𝑃𝑙𝑢𝑠}m\mathrm{𝑀𝑇𝑃}m\mathrm{𝑀𝑇𝑃}m`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑠𝑡𝑜𝑝}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑀𝑇𝑃}sx`$ | $`=`$ | $`sx\mathrm{`}\mathrm{𝑚𝑝𝑙𝑢𝑠}\mathrm{`}\mathrm{𝑎𝑙𝑙𝑀𝑇𝑃}(\mathrm{𝑠𝑡𝑜𝑝}\mathrm{\dot{}}\mathrm{𝑡𝑑𝑀𝑇𝑃}s)x`$ |

Accumulating a list query all-over the place

|  |  |  | $`\mathrm{𝑐𝑜𝑙𝑙𝑒𝑐𝑡}`$ | $`\mathit{::}`$ | $`u.\mathrm{𝑇𝑈}[u]\mathrm{𝑇𝑈}[u]`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑐𝑜𝑙𝑙𝑒𝑐𝑡}sx`$ | $`=`$ | $`sx++\mathrm{𝑎𝑙𝑙𝑇𝑈}(\mathrm{𝑐𝑜𝑙𝑙𝑒𝑐𝑡}s)x`$ |

Selection from the first node that admits success

|  |  |  | $`\mathrm{𝑠𝑒𝑙𝑒𝑐𝑡}`$ | $`\mathit{::}`$ | $`um.\mathrm{𝑀𝑜𝑛𝑎𝑑𝑃𝑙𝑢𝑠}m\mathrm{𝑀𝑇𝑈}um\mathrm{𝑀𝑇𝑈}um`$ |
| --- | --- | --- | --- | --- | --- |
| $`\mathrm{𝑠𝑒𝑙𝑒𝑐𝑡}sx`$ | $`=`$ | $`sx\mathrm{`}\mathrm{𝑚𝑝𝑙𝑢𝑠}\mathrm{`}\mathrm{𝑜𝑛𝑒𝑀𝑇𝑈}(\mathrm{𝑠𝑒𝑙𝑒𝑐𝑡}s)x`$ |

The first two combinators model non-monadic, type-preserving, and full traversal, i.e., they visit every node in the input term and the result type coincides precisely with the type of the input type. The monadic, type-preserving combinator $`\mathrm{𝑠𝑡𝑜𝑝}\mathrm{\_}\mathrm{𝑡𝑑𝑀𝑇𝑃}`$ performs a *partial* traversal, since it does not descend below nodes where its argument strategy is applied successfully. The type-unifying combinator $`\mathrm{𝑐𝑜𝑙𝑙𝑒𝑐𝑡}`$ performs a full traversal while intermediate list results are concatenated. The monadic, type-unifying combinator $`\mathrm{𝑠𝑒𝑙𝑒𝑐𝑡}`$ performs a partial traversal following the same scheme as $`\mathrm{𝑞𝑢𝑒𝑟𝑦}`$ from the sample section. However, the argument for recognition and extraction is not a function on a certain term type, but a strategy. This generality is appropriate whenever ‘relevant’ subterms can be of different types. All these combinators are reconstructions of combinators that are available in the strategy library distributed with Strafunski.

## 7 Concluding remarks

We have realized a compact amalgamation of term rewriting strategies and functional programming with emphasis on traversal strategies. Functional strategic programming features first-class generic functions that traverse terms of any type while mixing uniform and type-specific behaviour. Our reconstruction of functional strategies is based on just two combinators. Our first combinator is $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ for type-based function dispatch. Our second combinator is $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ for folding over constructor applications. We have given concise definitions of the these two basic combinators. We have demonstrated how they are used to define one-layer traversal combinators and recursive traversal combinators as used in strategic programming. The abilities to traverse terms and to mix uniform and type-specific behaviour provide, in our experience, the key to practical application of functional programming to program analysis and transformation problems.

We have discussed implementational models of functional strategies without commitment to a specific functional language. We have, for example, argued that adding built-in support for $`\mathrm{𝑎𝑑ℎ𝑜𝑐}`$ and $`\mathrm{ℎ𝑓𝑜𝑙𝑑𝑟}`$ to functional language implementations requires only modest modifications, if second-order polymorphism is available. More specifically, using a reference model which requires generative support per-type, we have shown how the Haskell language needs to be extended to include our two combinators. Fully operational support for functional strategic programming is available in the form of the Strafunski bundle for generic programming and language processing in Haskell. The bundle can be configured to use one out of several alternative models. Generative support is based on the DrIFT preprocessing technology for Haskell. Strafunski has been applied for Java refactoring, Cobol reverse engineering, grammar engineering, Haskell program analysis and transformation, XML document transformation, and others.

Thus, our approach is lightweight, highly expressive, well-founded, and has already proven its value in important application domains. Language users take advantage of the generality and simplicity provided by our combinator style of generic programming. Language implementors take advantage of the fact that strategic programming does not require any new language constructs, but only two simple combinators which are easily defined per-type or as built-ins. There is no need for compile-time specialisation, and separate compilation is easily maintained.

##### Acknowledgement

We are grateful for discussions with David Basin, Robert Ennals, Kevin Hammond, Ralf Hinze, Barry Jay, Johan Jeuring, Claude Kirchner, Paul Klint, Jan Kort, Andres Löh, Simon Peyton Jones, Claus Reinke, Simon Thompson, Phil Trinder, Jurgen Vinju, and Stephanie Weirich.


format: text

text:
# References

On the Penrose Inequality

Edward Malec1, Marc Mars2 and Walter Simon3

1 Uniwersytet Jagielloński, Kraków, Poland

2Universidad de Salamanca, Spain
3Universität Wien, Austria

> We summarize results on the Penrose inequality bounding the ADM-mass or the Bondi mass in terms of the area of an outermost apparent horizon for asymptotically flat initial data of Einstein’s equations. We first recall the proof, due to Geroch and to Jang and Wald, of monotonicity of the Geroch-Hawking mass under a smooth inverse mean curvature flow for data with non-negative Ricci scalar, which leads to a Penrose inequality if the apparent horizon is a minimal surface. We then sketch a proof of the Penrose inequality of Malec, Mars and Simon which holds for general horizons and for data satisfying the dominant energy condition, but imposes (in addition to smooth inverse mean curvature flow) suitable restrictions on the data on a spacelike surface. These conditions can, however, at least locally be fulfilled by a suitable choice of the initial surface in a given spacetime. Remarkably, they are also (formally) identical to ones employed earlier by Hayward in order to define a 2+1 foliation on null surfaces, with respect to which the Hawking mass is again monotonic.

In an attempt for getting evidence on the ”cosmic censorship conjecture” in asymptotically flat spactimes, Penrose considered collapsing shells of particles with zero rest mass and gave a heuristic argument in favour of the inequality

$$M_{ADM}\sqrt{\frac{A}{16\pi }}$$
(1)
between the ADM mass $`M_{ADM}`$ measured at spatial infinity and the area $`A`$ of an apparent horizon . Another conjecture with the Bondi mass $`M_B`$ measured at null infinity instead of $`M_{ADM}`$ can also be formulated.

To establish this ”Penrose inequality” (PI) for a selected apparent horizon in a given spacetime $`(,{}_{}{}^{4}g_{\mu \nu }^{})`$ we have to connect this horizon with infinity by a hypersurface $`𝒩`$. To describe this procedure in some detail we recall some facts about initial data sets $`(𝒩,g_{ij},k_{ij})`$, with apparent horizons as boundaries.

The induced metric $`g_{ij}`$ on $`𝒩`$ and the second fundamental form $`k_{ij}`$ are required to satisfy the constraints

$`D_i\left(k_l^ik\delta _l^i\right)`$ $`=`$ $`8\pi j_l,`$ (2)
$`Rk_{ij}k^{ij}+k^2`$ $`=`$ $`16\pi \rho .`$ (3)
where $`D_i`$ is the covariant derivative and $`R`$ the Ricci scalar on $`𝒩`$, $`k=g^{ij}k_{ij}`$, and $`\rho `$ and $`j_i`$ are the energy density and the matter current, respectively. We take the data to be asymptotically flat and to satisfy the dominant energy condition (which implies that $`\rho |j|`$).

For any 2-surface $`𝒮`$, we denote the tangents to the outgoing future and past null geodesics orthogonal to $`𝒮`$ by $`\stackrel{}{L}^\pm `$, with inner product $`\phi =\stackrel{}{L}^+,\stackrel{}{L}^{}`$. We introduce the ”expansions” of $`L^\pm `$ by

$$\mathrm{\Theta }^\pm =(g^{\mu \nu }2\phi ^1L^{+(\mu }L^{\nu )})_{(\mu }L_{\nu )}^\pm $$
(4)
which clearly depend on the normalization of the null vectors.

A “future apparent horizon” $``$ (called a “horizon” from now on) is a 2-surface defined by the property that all outgoing future directed null geodesics in $``$ orthogonal to $``$ have vanishing divergence, i.e. $`\mathrm{\Theta }^+=0`$, and that the divergence of the outgoing past null geodesics is non-negative, i.e. $`\mathrm{\Theta }^{}0`$. (The term ”outgoing” is defined with respect to the asymptotically flat end. Past apparent horizons are defined analogously). If $`\mathrm{\Theta }^+=\mathrm{\Theta }^{}=0`$ on $``$, the horizon is an extremal surface (in $`(,g_{\mu \nu })`$ as well as in any submanifold $`𝒩`$) and the outermost extremal surface in an asymptotically flat space must be minimal.

It is now useful to distinguish the following three cases.

This common (but somewhat unhappy) terminology denotes the case where $`𝒩`$ is bounded by a minimal surface (instead of a general trapped one) and where (instead of assuming the constraints) the Ricci scalar on $`𝒩`$ is required to be non-negative. Such 3-manifolds arise as spacelike slices of a spacetime with a horizon only in very special situations such as in the time-symmetric case.

Here one joins a chosen apparent horizon via a spacelike surface either with spatial infinity or with a cross section of null infinity.

One joins a chosen (future) apparent horizon with a cross section of (past) null infinity by a null surface.

Mathematical proofs of the PI with ”realistic” smoothness assumptions have so far only been obtained in the Riemannian case. The strongest result to date is due to Bray  who proves (1), admitting also disconnected minimal surfaces with (total) area $`A`$. However, we rather wish to expose here in some detail other (older) approaches which produce weaker results in the Riemannian case but are more promising, and also have produced some partial results, in the other cases. These approaches are based on defining flows and corresponding 2 + 1 decompositions of the chosen hypersurfaces. In particular the following steps can be identified in this strategy:

1. Choose a suitable 3-surface $`𝒩`$ joining the apparent horizon with infinity.
2. Choose (or if possible, show existence !) of a (weak) flow on $`𝒩`$ starting at the horizon and going to infinity. Consider the corresponding foliation $`S(r)`$ by level surfaces of the flow (if it exists !).
3. Define a ”quasilocal mass” $`M_{QL}(r)`$ as a surface integral, in particular over the level sets of the flow.
4. Show that $`lim_r\mathrm{}M_{QL}M_{ADM}`$ or that $`lim_r\mathrm{}M_{QL}M_B`$ (where the ”end” of $`𝒩`$ is at $`r\mathrm{})`$.
5. Show that $`M_{QL}(r_{})\sqrt{A/16\pi }`$ (where $`r_{}`$ denotes the horizon).
6. Show monotonicity of the mass along the flow, i.e. $`(d/dr)M_{QL}(r)0`$.

It is obvious that the PI, equ. (1), follows if these steps can be carried out. In practice, it is useful to restrict oneself first to smooth flows, and to try to generalize afterwards. We are now going to describe the 3 cases identified before.
The Riemannian case.

We first assume that there is a smooth “inverse mean curvature flow” (IMCF) starting from a minimal surface. This means that one can write the metric $`g_{ij}`$ as

$$ds^2=\varphi ^2dr^2+q_{AB}dx^Adx^B$$
(5)
(where $`A,B=2,3`$), with smooth fields $`\varphi `$ (the ”lapse”) and $`q_{AB}`$, and with $`p\varphi =g(r)`$ where $`p`$ is the mean curvature of the surfaces $`r=\text{const.}`$ and $`g(r)`$ is a smooth function. In other words, $`p\varphi `$ is constant on the level sets of the flow. Note that $`\varphi `$ diverges at the minimal surface, but the integral curves of the flow can be extended. Assuming also that the level sets have spherical topology, Geroch showed that the mass functional

$$M_G(𝒮)=\frac{\sqrt{A}}{64\pi ^{\frac{3}{2}}}\left(16\pi _𝒮p^2𝑑S\right)$$
(6)
(taken over level sets of the IMCF) is monotonic , while Jang and Wald observed that this leads to the proof of the PI along the lines sketched above . Later Huisken and Ilmanen succeeded in removing the restrictive and ”unphysical” assumption of smoothness of the flow . These authors established the existence of weak solutions of the degenerate elliptic equation for the level sets of the IMCF. The resulting generalized flow appears to ”jump” at (countably) many places to so-called minimizing hulls. Most importantly, the Geroch mass increases at each jump, and so monotonicity is preserved. In this setup it is also possible to handle disconnected horizons but the presence of jumps prevents obtaining the PI with the total area of the horizon. Unlike Bray’s result, the PI proved by this method only contains the area of any connected component selected to start the IMCF. (In particular, the largest component can be chosen for this purpose).
The general spacelike case.

Let $`(𝒩,g_{ij},k_{ij})`$ be a data set with $`𝒩`$ spacelike, and assume as before that there is a smooth IMCF with level sets of spherical topology. Let $`\stackrel{}{M}=d/dr`$, or equivalently $`M^iD_ir=1`$, denote the tangent vector field to the flow. We normalize the null vectors $`\stackrel{}{L}^\pm `$ emanating orthogonally from the level sets by requiring that

$$\stackrel{}{L}^++\stackrel{}{L}^{}=\sqrt{2}\stackrel{}{M}.$$
(7)
Here we describe (and rewrite sligthly) a result of Malec, Mars and Simon  who show monotonicity of the Hawking quasilocal mass

$$M_H(𝒮)=\frac{\sqrt{A}}{64\pi ^{\frac{3}{2}}}\left(16\pi _𝒮\phi ^1\mathrm{\Theta }^+\mathrm{\Theta }^{}𝑑S\right)$$
(8)
(defined in terms of the expansions (4)) under the following restrictions of the data (in addition to smooth IMCF):

$`\mathrm{\Theta }^{}`$ $``$ $`0\text{on the level sets of the IMCF on}𝒩,`$ (9)
$`{\displaystyle \frac{\mathrm{\Theta }^+}{\mathrm{\Theta }^{}}}`$ $`=`$ $`f(r)\text{for some smooth function}f(r).`$ (10)
Equ. (10) means that $`\mathrm{\Theta }^+/\mathrm{\Theta }^{}`$ is constant on the level sets of the IMCF. Note that $`M_H`$ does not depend on the normalization of the null vectors $`L^\pm `$, whereas condition (10) is to be understood in terms of the normalization introduced above. We next remark that, again using this normalization, we have $`\sqrt{2}p\varphi =\mathrm{\Theta }^++\mathrm{\Theta }^{}`$. Hence the condition of IMCF, together with (10), is equivalent to requiring the existence of a foliation on which both expansions $`\mathrm{\Theta }^+`$ and $`\mathrm{\Theta }^{}`$ are constant. We will refer to this observation when describing the null case below. Moreover, equ.(10) together with IMCF is also equivalent with 3.(a) in the theorem of  (where a different normalization was used).

We finally note that (10) can locally be fulfilled by a suitable choice of the hypersurface in a given spacetime. In fact, consider an arbitrary (smooth) function $`F(r)`$ with $`F(0)=1`$ and $`|F(r)|<1`$ for $`r>0`$. Rescaling the null vectors $`\stackrel{}{L}^{}`$ and $`\stackrel{}{L}^+`$ emanating from $`𝒮`$ like $`\stackrel{}{L}^+\lambda \stackrel{}{L}^+`$ and $`\stackrel{}{L}^{}\lambda ^1\stackrel{}{L}^{}`$, with $`\lambda ^2=\mathrm{\Theta }^{}(\mathrm{\Theta }^+)^1(1+F(r))(1F(r))^1`$ the relation (7) then determines the tangent to the hypersurface on which the IMCF satisfies (9) as well as (10). In view of the large freedom for choosing $`F(r)`$ it is also plausible that a suitable choice would make the surface $`𝒩`$ reach spacelike infinity.

The null case.

Ludvigsen and Vickers have shown that the ”Nester-Witten” quasilocal mass is monotonic along a suitable flow on a surface generated by null geodesics emanating orthogonally from the apparent horizon . More recently Bergqvist has substantially simplified the proof of this result by removing all the spinors from the arguments . The problems with applying these results to a proof of the PI are, firstly, that the null surfaces constructed in this way do not exist globally in general and secondly, that the quasilocal masses are not known to be bounded by the Bondi mass at infinity in the sense of condition 4 above.

In contrast, Hayward shows monotonicity of the Hawking mass on null surfaces along a flow defined by the condition that the expansions $`\mathrm{\Theta }^+`$ and $`\mathrm{\Theta }^{}`$ are constant on the level sets . More precisely, for the surfaces spanned, say, by past directed null geodesics emanating from the future apparent horizon, it is the condition that $`\mathrm{\Theta }^{}`$ is constant on the level sets which defines the foliation while the constancy of $`\mathrm{\Theta }^+`$ just defines a scaling of $`\stackrel{}{L}^+`$ convenient for the computation. Since an analogous monotonicity statement holds along the other null congruence as well it seems that, by taking linear combination of the null vectors one can also obtain monotonicity along the corresponding spacelike directions. While this is not true in general (the statements on this issue in  are not correct), it is nevertheless true in special cases, in particular when $`\stackrel{}{M}`$ is just the sum of the null vectors as in (7). Therefore the analogy between Haywards result and the result of Malec, Mars and Simon in the spacelike case (as reformulated above) is not an incidence. It should be possible to write these results in a unified manner in a suitable formalism.
Acknowledgement
W.S. was supported by Austrian FWF project Nr. P14621-Mat.