Electronic Notes in Theoretical Computer Science 70 No. 6 (2017)
URL: http://www.elsevier.nl/locate/entcs/volume70.html 21 pages

The Sketch of a Polymorphic Symphony

arXiv:cs/0204013v2 [] 1 Nov 2002

Ralf Lämmel
Email: ralf@cs.vu.nl
CWI, Kruislaan 413, NL-1098 SJ Amsterdam
Vrije Universiteit, De Boelelaan 1081a, NL-1081 HV Amsterdam

Abstract
In previous work, we have introduced functional strategies, that is, first-class generic functions that can traverse into terms of any type while mixing uniform and type-specific behaviour. In the present paper, we give a detailed description of one particular Haskell-based
model of functional strategies. This model is characterised as follows. Firstly, we employ
first-class polymorphism as a form of second-order polymorphism as for the mere types of
functional strategies. Secondly, we use an encoding scheme of run-time type case for mixing uniform and type-specific behaviour. Thirdly, we base all traversal on a fundamental
combinator for folding over constructor applications.
Using this model, we capture common strategic traversal schemes in a highly parameterised style. We study two original forms of parameterisation. Firstly, we design parameters for the specific control-flow, data-flow and traversal characteristics of more concrete
traversal schemes. Secondly, we use overloading to postpone commitment to a specific
type scheme of traversal. The resulting portfolio of traversal schemes can be regarded as a
challenging benchmark for setups for typed generic programming.
The way we develop the model and the suite of traversal schemes, it becomes clear that
parameterised + typed strategic programming is best viewed as a potent combination of
certain bits of parametric, intensional, polytypic, and ad-hoc polymorphism.

Arrangement
The running example Given is a tree, say a term. We want to operate on a certain
subterm. We search for the subterm t in some traversal order, be it top-down and
left-to-right. We want to further constrain t in the sense that it should occur on a
certain path, namely below k nodes the fitness of which is determined by predicates.
Once we found t below certain nodes n1 , . . . , nk , we either want to select t as is, or
we want to compute some value from t, or we want to transform t in its context in
the complete tree. This traversal scenario is illustrated in Fig. 1 for k = 2. This sort
of problem is very common in programming over tree and graph structures, e.g., in
adaptive object-oriented programming [16]. One might consider additional forms
of conditions, e.g., certain kinds of nodes that should not be passed, or further forms
of computation, e.g., cumulative computation along the path.
c 2017 Published by Elsevier Science B. V.

Lämmel

1
0
1
0
1
0
0
1

n
1

n2

Find the subtree t below n2 in turn below n1 . We
assume two predicates p1 and p2 to identify n1 and
n2 . We further assume a generic function f to identify
and then to process t.

t

Figure 1. Processing a subtree that is reachable via a path

Sample code In the present paper, we refrain from discussing real-world application snippets but we sketch an illustrative instance of the running example in
Fig. 2. As one can see, we assume a combinator belowlist that captures the described scheme of path traversal. In the figure, we define a function test42 to traverse into a sample term term1 in terms of belowlist. The traversal looks for a
subterm of type SortB to extract its integer component if it occurs on a path with
two SortB subterms with the integer components 1 and 3. There are a few blind
spots in the figure (cf. “. . . ”) which we will resolve in the course of the concert. As
the following Hugs session shows, the traversal yields 42:
Main> test42
Just 42
Main>
A traversal scheme for the introductory problem
f ‘belowlist ‘ ps = ...
A sample system of two datatypes
data SortA = SortA1 SortB | SortA2
data SortB = SortB Int SortA
A test term for traversal
term1 = SortA1 (SortB 0 (SortA1 (SortB 1 (SortA1 (SortB 2 (
SortA1 (SortB 3 (SortA1 (SortB 42 SortA2 )))))))))
Extract the integer from a SortB term; fail for other sorts
sortb2int = ...
Insist on a SortB term with a specific integer
sortbEqInt i = ...
An actual traversal
test42 :: Maybe Int
test42 = (f ‘belowlist ‘ [p1 , p2 ]) term1
where f = sortb2int
p1 = sortbEqInt 1
p2 = sortbEqInt 3
Figure 2. Illustrative Haskell code for the running example

2

Lämmel

Side conditions The above traversal scenario should be complemented by a few
useful side conditions. We assume that (i) we deal with many sorts, say usersupplied systems of named, mutually recursive datatypes such as syntaxes and formats. So a traversal will encounter terms of different types. We further require that
(ii) traversal schemes are statically type-safe, that is, a traversal always delivers a
type-correct result (if any) without even attempting the construction of any ill-typed
term. Furthermore, we insist on (iii) a parameterised solution where the overall
traversal scheme is strictly separated from problem-specific ingredients. Also, the
kind of processor (recall selection vs. computation vs. transformation) should not
be anticipated. Recall that the actual traversal in Fig. 2 is indeed synthesised by
passing predicates and a processor to a presumably overloaded traversal scheme
belowlist. Last but not least, we require that (iv) a proper combinator approach
is adopted where one can easily compose traversals and schemes thereof. As for
the assumed belowlist combinator, its definition should be a concise and suggestive
one-liner based on more fundamental traversal combinators. With combinators,
we can easily toggle variation points of traversal, e.g., top-down vs. bottom-up,
left-to-right vs. right-to-left, first match vs. all matches, and so on.
Conducted by Strafunski If any of the above side conditions is given up, the
treatment of the scenario becomes less satisfying. If you do not insist on static
type safety, then you can resort to Prolog, or preferably to Stratego [23] which
supports at least limited type checks. Types are however desirable to discipline
the instantiation of traversal schemes. If you even want to do away with parameterisation and combinator style, then XSLT is your language of choice. If types
appeal to you, then you might feel tempted to consider polytypic functional programming [9]. However, corresponding language designs do not provide support
for generic programming in a combinator style because polytypic values are not
first-class citizens. If you are as demanding and simplistic as we are, then you
use the Strafunski-style of generic programming in Haskell as introduced by the
present author and Joost Visser in [14]. 1 The style is centred around the notion of
functional strategies — first-class generic functions that can traverse into terms of
any type while mixing uniform and type-specific behaviour.
The movements No previous knowledge of strategic programming is required
to enjoy this symphony. We develop a model of functional strategies based on
Haskell 98 [19] extended with first-class polymorphism [11]. The symphony consists of four movements. In Sec. 1, the type Strategic of functional strategies is
initiated and inhabited with parametrically polymorphic [21,24] combinators. In
Sec. 2, we integrate a combinator adhoc to update functional strategies for a specific type. This combinator relies on run-time type case — a notion that was studied
in the context of intensional polymorphism [8,28]. In Sec. 3, we integrate a fundamental combinator hfoldr to perform primitive portions of traversal by folding
1

URL http://www.cs.vu.nl/Strafunski where Stra refers to strategies as in strategic
term rewriting [3,23], fun refers to functional programming, and their harmonious composition is
a homage to the music of Igor Stravinsky.

3

Lämmel

over the immediate subterms of a term without anticipation of recursion. This kind
of folding can be regarded as a variation on polytypism [9]. In Sec. 4, we use
overloading, say ad-hoc polymorphism [26,10], to treat different types of traversal (recall selection vs. computation vs. transformation) in a uniform manner. At
this level of genericity, we succeed in defining a portfolio of highly parameterised
traversal schemes, including the scheme belowlist that is needed in the running
example. This portfolio demonstrates the expressiveness and conciseness of functional strategies. 2

1 Moderato
In this section, we initiate the type of generic functions that model functional strategies. For the sake of a systematic development, we will first focus on the most simple, i.e., the parametrically polymorphic [21,24] dimension of the corresponding
type scheme. In the subsequent two movements, we go beyond this boundary by
adding expressiveness for run-time type case and generic term traversal.
First-class polymorphic functions In Fig. 3, we use a type synonym Parametric with two parameters α and κ to capture the general type scheme α → κ α of
functional strategies. As one can see, the parameter α corresponds to the domain
of the function type, and κ is used to construct the co-domain from α. Common
options for the co-domain type constructor κ are the identity type constructor I
and the constant type constructor C as defined in the figure, too. Based on the
type scheme Parametric, we define the ultimate datatype Strategic that captures the
polymorphic function type for functional strategies. Polymorphism is expressed
via the universal quantifier “∀”, and the fact that we ultimately need to go beyond
parametric polymorphism is anticipated via a class constraint “Term α” for ‘strategic polymorphism’. Note that the “∀” occurs in the scope of the component of the
constructor G. This form of second-order polymorphism, where polymorphic entities are wrapped by datatype constructors, is called first-class polymorphism [11],
and it is a common language extension of Haskell 98. (Implicit) top-level universal
quantification would be eventually insufficient to construct strategy combinators.
Strategic type schemes In Fig 3. we also define the identity type constructor I,
the constant type constructor C, and the constructor S for sequential composition
of type constructors. Based on these, we derive three classes MG, TP, and TU of
generic functions from Strategic. The synonym MG captures monadic strategies.
Monadic style [25] is favoured here because that way we can deal with effects during traversal, e.g., success and failure, state, or nondeterminism. We could also
consider extra variants for non-monadic strategies but we instead assume that the
2

The code shown in the paper is fully operational in Haskell (tested with Hugs 98; Dec. 2001
version). A paper-specific Strafunski distribution with illustrative examples can be downloaded
from the paper’s web-site http://www.cwi.nl/˜ralf/polymorphic-symphony/. This
distribution also comes with a strategic Haskell program that provides generative tool support for
strategic programming against user-supplied datatypes.

4

Lämmel

The generic function type for functional strategies
type Parametric α κ = α → κ α
newtype Strategic κ = G (∀ α. Term α ⇒ Parametric α κ)
unG (G s) = s
The identity type constructor
newtype I α = I α
unI (I x ) = x
The constant type constructor
newtype C u α = C u
unC (C x ) = x
Sequential type constructor composition
newtype S t t ′ α = S (t ′ (t α))
unS (S x ) = x
Type-preserving and type-unifying strategies
type MG κ m = Strategic (S κ m)
type TP m = MG I m
type TU u m = MG (C u) m

-- ‘Monadic Generic’ functions
-- Corresponds to ∀α. α → m α
-- Corresponds to ∀α. α → m u

Strategy application by unwrapping
apply :: (Term α, Monad m) ⇒ MG κ m → α → m (κ α)
apply s x = unS (unG s x )
More convenient application for TP
applyTP :: (Monad m, Term α) ⇒ TP m → α → m α
applyTP s x = apply s x >>= return ◦ unI
More convenient application for TU
applyTU :: (Monad m, Term α) ⇒ TU u m → α → m u
applyTU s x = apply s x >>= return ◦ unC
Figure 3. Functional strategies as first-class polymorphic functions

trivial identity monad is used for that purpose. The synonym TP instantiates MG
via I so that Type-Preserving strategies are identified. The synonym TU instantiates MG via C so that Type-Unifying strategies are identified, that is, polymorphic
functions with a fixed result type. At the bottom of Fig. 3, we provide trivial definitions of ‘application’ combinators. The combinator apply complements ordinary
function application by some unwrapping that accounts for first-class polymorphism (cf. unG), and for type-constructor composition (cf. unS). The combinators
applyTP and applyTU specialise apply for TP and TU to hide the employment of
the datatypes I and C for co-domain construction. Their result types point out the
basic type schemes for TP and TU without any noise. 3
3

We should revise our sample code from Fig. 2 to use applyTU in the synthesis of the traversal:
test42 :: Maybe Int
test42 = applyTU (f ‘belowlist ‘ [p1 , p2 ]) term1
where...

5

Lämmel

Parametrically polymorphic embedding
para :: (∀ α. Parametric α κ → Strategic κ)
para s = G s
Identity strategy
idTP :: Monad m ⇒ TP m
idTP = para (S ◦ return ◦ I )
Constant strategy
constTU :: Monad m ⇒ u → TU u m
constTU u = para (S ◦ return ◦ C ◦ const u)
Failure strategy
fail :: MonadPlus m ⇒ MG κ m
fail = para (S ◦ const mzero)
Figure 4. Parametrically polymorphic strategies
Left-to-right monadic sequential strategy composition
seq :: Monad m ⇒ TP m → MG κ m → MG κ m
seq f g = G (λx → S (applyTP f x >>= apply g))
Value-passing with shared term argument
pass :: Monad m ⇒ TU u m → (u → MG κ m) → MG κ m
pass f g = G (λx → S (applyTU f x >>= λu → apply (g u) x ))
Composition of alternative strategies
choice :: MonadPlus m ⇒ MG κ m → MG κ m → MG κ m
choice f g = G (λx → S (apply f x ‘mplus‘ apply g x ))
Figure 5. Composition combinators for functional strategies

Nullary combinators Let us start to inhabit the strategy types while restricting
ourselves to parametrically polymorphic inhabitants. In Sec. 2 and Sec. 3, we will
inhabit the type Strategic in other ways by employing designated combinators for
‘strategic polymorphism’. If we neglect the monadic facet of functional strategies
for a second, then there are few parametrically polymorphic inhabitants: the identity function for the type-preserving scheme, and constant functions for the typeunifying scheme. This is generalised for the monadic setup in Fig. 4. For clarity,
we define the function para that approves a parametrically polymorphic function
as a member of Strategic. While its definition coincides with the constructor G, its
type insists on a parametrically polymorphic argument (no mentioning of the Term
class). Using para, we can define the identity strategy idTP and a combinator constTU for constant strategies. Relying on the extended monad class MonadPlus, we
can also define the always failing strategy fail in terms of the member mzero denoting failure, e.g., Nothing in the case of the Maybe instance of the MonadPlus class.
The inhabitant fail is meant to illustrate that functional strategies might exhibit success and failure behaviour, or they even might be non-deterministic depending on
the actual choice of the MonadPlus instance.
6

Lämmel

Binary combinators In Fig. 5, we define three prime combinators to compose
functional strategies. The combinator seq lifts monadic sequencing of function
applications to the strategy level (cf. “>
>=”). The combinator pass composes two
strategies which share a term argument and where the result of the first strategy
is passed as additional input to the second strategy. The combinator choice composes alternative function applications. The actual kind of choice depends on the
(extended) monad which is employed in the definition (cf. class MonadPlus and its
member mplus), e.g., the Maybe monad for partiality or the List monad for multiple results. In the definitions of the binary combinators, we use apply to deploy
the polymorphic function arguments, and we use G to re-wrap the composition as
a polymorphic function of type Strategic. In composing functional strategies, we
cannot use the disciplined para as a substitute for G because, eventually, we want
to compose functions that go beyond parametric polymorphism.
Rank-2 types A crucial observation is that the composition combinators seq,
pass and choice really enforce us to use some form of second-order polymorphism [7,20]. Other function combinators like “◦” or “>
>=” have rank-1 types,
that is, they are quantified at the top-level. This implies that they (also) accept
monomorphic function arguments. By contrast, the types of seq, pass and choice
have rank-2 types, that is, they are quantified argument-wise. These types model insistence on polymorphic function arguments as required for generic programming
in a combinator style. Rank-2 types are not just needed for the binary composition
combinators, but also for the upcoming traversal primitive, and for non-recursive
and recursive traversal combinators. Actually, generic traversal in a combinator
style necessitates rank-2 types. This is because, in general, a traversal scheme takes
universally quantified arguments. Nested quantification reflects that ingredients of
traversals must be applicable to subterms of any type.

2 Larghetto
At this point in our polymorphic concert, we still lack the original expressiveness
of functional strategies: the ability to perform traversal into terms while mixing
uniform and type-specific behaviour. This section and the subsequent one are concerned with this ‘strategic polymorphism’. In the present section, we provide a
combinator adhoc for type-specific customisation of functional strategies. In the
next section, generic traversal into terms will be enabled.
Informal explanation The type of the adhoc combinator is given at the top of
Fig. 6. The combinator allows us to update an existing strategy for a specific type
via a monomorphic function. We call this idiom type-based function dispatch. We
also use the term strategy update because of the affinity to point-wise modification
of ordinary functions. In this sense, strategy update is about “type-wise” modification of a polymorphic function. Here are two samples of strategy update:
negate bool
negate bool

:: TP Identity
= adhocTP idTP (return ◦ ¬)
7

Lämmel

The adhoc combinator
adhoc :: Term α ⇒ Strategic κ → Parametric α κ → Strategic κ
adhoc poly mono = ... -- Implemented via Term class; see below.
A convenient specialisation for TP
adhocTP :: (Monad m, Term α) ⇒ TP m → (α → m α) → TP m
adhocTP poly mono = adhoc poly (λx → S (mono x >>= return ◦ I ))
A convenient specialisation for TU
adhocTU :: (Monad m, Term α) ⇒ TU u m → (α → m u) → TU u m
adhocTU poly mono = adhoc poly (λx → S (mono x >>= return ◦ C ))
Figure 6. Updating functional strategies by type-specific cases
Attempt to extract the integer from a SortB term
sortb2int :: TU Int Maybe
sortb2int = adhocTU fail (λ(SortB i ) → Just i )
Insist on a SortB term with a specific integer
sortbEqInt :: Int → TU () Maybe
sortbEqInt i = sortb2int ‘pass‘ (λi ′ → if i ′ ≡ i then constTU () else fail )
Figure 7. Use of strategy update in the running example

return int
return int

:: TU Int Maybe
= adhocTU fail return

The strategy negate bool behaves like idTP most of the time but it performs negation when faced with a Boolean (cf. “¬”). We use the Identity monad. The strategy
return int is meant to recognise integers, that is, it simply fails if it does not find
an integer. So we use the Maybe monad to deal with failure. Note that we use
type-specialised variants adhocTP and adhocTU as defined in Fig. 6. They allow
the strategic programmer to forget about wrapping and unwrapping I, C, and S.
In Fig. 7, we use strategy update to resolve two blind spots in Fig. 2 — the sample
code for our running example. The strategy sortb2int extracts an integer from a
term of type SortB. The strategy sortbEqInt insists on a specific extracted integer.
This is a predicate-like strategy which either returns Just () or Nothing.
Definition of strategy update Given a strategy poly of type Strategic κ, and a
function mono of type Parametric α κ, the updated function adhoc poly mono
branches according to the type α′ of an eventual input value v: if α = α′ , then
mono is applied to v, otherwise poly. That is:
(
mono v, if type of v = domain of mono
adhoc poly mono v =
poly v, otherwise
Strategy update can be considered as a simple and very disciplined form of type
case at run-time. Such type case was studied in the context of intensional polymorphism [8,28]. One might feel tempted to compare strategy update to dynamic typ8

Lämmel

ing [1,2] but note that first-class polymorphic strategies, as designed in the present
paper, operate on terms of algebraic datatypes as opposed to ‘dynamics’. Dynamic
typing can be employed, however, in other models of functional strategies, e.g., in
the way described in [14].
Encoding scheme A strategic programmer considers the adhoc combinator as a
primitive. In Haskell, we cannot define the adhoc combinator once and for all, but
it can be supported per datatype. This is precisely what the Term class is needed
for in the definition of Strategic (recall Fig. 3). So we basically place the adhoc
combinator in the Term class with the provision to add another member for generic
traversal later. There are several ways to encode strategy update. We will explain
here a scheme that is inspired by type-safe cast as of [27]. In fact, we revise this
scheme to model a single-branching type case (as opposed to a plain type cast)
while assuming nominal type analysis (as opposed to a structural one).
The scheme is illustrated in Fig. 8. In the Term class, we place a primed member
adhoc ′ with an implicitly quantified type. This is necessary because we need to
Initiation of the Term class for ‘strategic polymorphism’
class Term α where
adhoc ′ :: Term a′ ⇒ Strategic κ → Parametric α κ → Parametric a′ κ
Migration from an overloaded to a first-class polymorphic type
adhoc poly mono = G (adhoc ′ poly mono)
Helpers for ‘recording’ types of updates
class Term α where -- to be added
int :: Strategic κ → Parametric Int κ → Parametric α κ
sorta :: Strategic κ → Parametric SortA κ → Parametric α κ
sortb :: Strategic κ → Parametric SortB κ → Parametric α κ
Initialisation of the ‘decision matrix’ via default declarations
class Term α where
int poly = unG poly
sorta poly = unG poly
sortb poly = unG poly
The relevant slices of the Term instances
instance Term Int where
adhoc ′ = int
int mono = mono
instance Term SortA where
adhoc ′ = sorta
sorta mono = mono
instance Term SortB where
adhoc ′ = sortb
sortb mono = mono
Figure 8. Per-datatype support for strategy update

9

Lämmel

link the type parameter α of the class declaration to the type of adhoc ′ . In the type
of adhoc ′ , the parameter α acts as a place-holder for the term type of the updating
monomorphic function, and there is an extra parameter α′ for the term type of the
input term. The first-class polymorphic adhoc is easily derived from adhoc ′ via
wrapping with G as shown in the figure. The overall idea for the implementation
of adhoc ′ is to compare the term type α of the update with the term type α′ of the
ultimate input term. To this end, we need to encode a kind of decision matrix to
check for α = α′ for all possible combinations of term types. The dimension for α
is taken care of by overloading adhoc ′ in α. The dimension for α′ is taken care of by
extra helper members — one for each type. These helper members model strategy
update for a specific type of update while they are overloaded in the input term type.
This is exemplified in the figure with the helpers int, sorta, and sortb for the sample
term types in our running example (cf. Fig. 2). It makes sense to initialise the
definitions of the helper members to resort to poly by default. In any given instance
of the Term class, we need to define adhoc ′ , and we override the default definition
for the specific helper member that handles the instance’s type. The definition of
adhoc ′ simply dispatches to the helper member. The helper member is redefined to
dispatch to mono instead of poly. This is again illustrated for the sample term types
in our running example. Note that we are faced with a closed-world assumption
because we need one member per term type in our strategic program (see [14] for
another model).
Mixture of specificity and genericity The contribution of strategy update is the
following. It allows us to lift type-specific behaviour in a type-safe and transparent
way to the strategy level. Note that parametric polymorphism only works the other
way around: a polymorphic function can be applied to a value of a specific type, and
in fact, the actual behaviour will be entirely uniform, independent of the specific
type [21,24]. In generic programming with traversals, type-specific customisation
is indispensable because a traversal is typically concerned with problem-specific
datatypes and constructors. At a more general level, one can say that the adhoc
combinator implements the following admittedly very much related requirements
regarding the tension between genericity and specificity:
(i) Separability of generic and type-specific behaviour
(ii) Composability of generic and type-specific behaviour
(iii) First-class status of updatable generic functions
In functional programming, the common approach to the definition of polymorphic
functions with type-specific behaviour is to use ad-hoc polymorphism, say type and
constructor classes [26,10] as supported in Haskell. This approach does not meet
the above requirements because a class and its instances form a declaration unit.
Any new combination of generic and type-specific behaviour has to be anticipated
by a dedicated class. Hence, strategy update is complementary.

10

Lämmel

3 Allegretto
Ultimately, functional strategies are meant to perform term traversal. Hence, we
need to add another bit of polymorphism. In fact, the kind of term traversal that
we envisage can be regarded as a variation on polytypism [9]. That is, recursion
into terms is performed on the basis of the structure of the underlying algebraic
datatypes. First we will briefly categorise traversal approaches in previous work.
Then we will generalise one of the approaches to contribute a very flexible means
of traversal to the ongoing reconstruction of functional strategies.
Traversal approaches We identify the following categories:
(i) Recursive traversal schemes [18,5,22,15,4]
(ii) One-layer traversal combinators [23,12,14]
(iii) Traversal by type induction [9]
(iv) Traversal at a representation-type level [3]
(i) Recursive traversal schemes, e.g., generalised folds or iterators over data structures, follow a fixed scheme of recursion into terms, and the style of composition
of intermediate results is also intertwined with the recursion scheme. (ii) Onelayer traversal combinators add flexibility because they do not recurse into terms
by themselves but they rather capture single steps of traversals. Hence, different
recursion schemes and different means to compose intermediate results can still be
established by plain (recursive) function definition. The value of one-layer traversal combinators was identified in the context of strategic term rewriting [23] in the
application domain of program transformation. (iii) Polytypic programming suggests that a traversal can also be viewed as a function that is defined by induction
on the argument type. So one can capture term traversal schemes by polytypic
definitions. However, these definitions could not be used in a combinator style
because existing language designs do not cover ‘rank-2 polytypism’, that is, one
cannot pass one polytypic function to another one. (iv) Finally, a programmer can
resort to a universal representation type to perform traversal. Here we assume that
the programmer is provided with implosion and explosion functionality to mediate
between programmer-supplied term types and the representation type. While unrestricted access to a representation type corresponds to a less safe way of generic
programming due to the potential of implosion problems, implementations of (i)–
(iii) might very well be based on a representation type. To give an example, in [14],
traversal combinators are implemented using a representation type without any exposure to the generic programmer. Hence, implosion safety can be certified.
Right-associative, heterogeneous fold In this symphony, we basically follow the
one-layer traversal-combinator approach, but we generalise it in the following manner. Rather than making a somewhat arbitrary selection of traversal combinators as
in previous work [23,12,14], we identify the fundamental principle underlying all
one-layer traversal. To this end, we define a primitive combinator for folding over
constructor applications. This kind of folding views the immediate subterms of a
11

Lämmel

Completion of the Term class for ‘strategic polymorphism’
class Term α where
hfoldr ′ :: HFoldrAlg κ → α → κ α
Migration from an overloaded to a first-class polymorphic type
hfoldr :: HFoldrAlg κ → Strategic κ
hfoldr alg = G (hfoldr ′ alg )
Fold algebras
data HFoldrAlg κ = A
-- First-class polymorphic wrapper
(∀ α β. Term α ⇒ α → κ (α → β) → κ β) -- Cons-like case
(∀ γ. γ → κ γ)
-- Nil-like case
Figure 9. Folding over constructor applications
instance Term Int where
hfoldr ′ (A z ) i = z i
instance Term SortA where
hfoldr ′ (A f z ) (SortA1 b) = f b (z SortA1 )
hfoldr ′ (A z ) SortA2 = z SortA2
instance Term SortB where
hfoldr ′ (A f z ) (SortB i α) = f α (f i (z SortB ))
Figure 10. Per-datatype support for hfoldr — sample instances

term (say, its children) as a heterogeneous list of terms. Without loss of generality,
we favour a right-associative fold in the sequel. We call the resulting fold operation hfoldr for right-associative, heterogeneous fold. Let us recall how the ordinary
foldr folds over a homogeneous list. Given the fold ingredients f and z for the
non-empty and the empty list form, the application of foldr to a list is defined as
follows:
foldr f z [x1 , x2 , . . . , xn ] = f x1 (f x2 (· · · (f xn z) · · ·))
The combinator hfoldr folds over a constructor application in nearly the same way:
hfoldr f z (C xn · · · x2 x1 ) = f x1 (f x2 (· · · (f xn (z C)) · · ·))
Note the order of the children in a constructor application. Due to curried style,
we have a kind of snoc-list, that is, the leftmost child is the head of the list, and so
on. Also note that the empty constructor application C is passed to z so that the
constructor can contribute to the result of folding.
Encoding scheme A strategic programmer considers hfoldr as a primitive. In
Haskell, we cannot define the hfoldr combinator once and for all, but it can be supported per datatype — as in the case of strategy update. In Fig. 9, we complete
the Term class accordingly. We add a primed helper member hfoldr ′ to the class,
and we define the actual combinator hfoldr via wrapping with G. Due to the employment of first-class polymorphism, we need to pack the ingredients f and z for
hfoldr in a datatype HFoldrAlg. This is a deviation from the curried style that is
12

Lämmel

used for the rank-1 foldr for lists. The datatype constructor A is used for packaging.
The types of the two components deserve some explanation. The first component,
i.e., the one that corresponds to f , is universally quantified in α and β corresponding to the type of the heading child (i.e., the outermost argument in the constructor
application), and the type of the constructor application at hand, respectively. The
type of the recursively processed tail is κ (α → β) because it ‘lacks’ a child of type
α. Given a constructor application C xn · · · x2 x1 , the type variable α would be
bound to the respective types of the xi in the several folding steps while the type
β variable would be bound to the corresponding remainders of C’s type. The second component of A, i.e., the one that corresponds to the base case z, is simply a
parametrically polymorphic function for processing the empty constructor application. The per-datatype definition of hfoldr is illustrated in Fig. 10 with the sample
datatypes from our running example. We basically need one equation for hfoldr ′
of the above form for each specific datatype constructor.
One-layer traversal combinators Based on hfoldr, one can define all kinds of
one-layer traversal combinators. We indicate an open-ended list of candidates by
reconstructing combinators that were presented elsewhere [23,13,14,12]:
allTP Process all children; preserve the constructor.
oneTP Try to process the children until one succeeds; preserve the constructor.
allTU Process all children; reduce the intermediate results.
oneTU Try to process the children until one succeeds; return the processed child.
One can think of further combinators, e.g., combinators dealing with different orders of processing children, monadic effects, and different constraints regarding
success and failure behaviour.
The definition of the combinators is shown in Fig. 11. Let us explain the first
one, that is, allTP. We construct a (type-preserving) fold algebra A f z and pass
it to hfoldr. The ingredient z for the empty constructor application simply returns,
i.e., preserves the constructor. Additional wrapping of S and I is needed to deal
with our ‘datatypes-as-type-constructors’ encoding. The ingredient f sequences
three computations. Firstly, the tail t is computed. Secondly, the head h (i.e.,
the child at hand) is processed via s. Thirdly, the processed head h′ is passed to
the computed tail t′ (modulo wrapping and unwrapping). The definition of the
other combinators is similar. A challenging complication shows up when we want
to define oneTP because it turns out that this fold over children is paramorphic in
nature [17] while our combinator hfoldr is catamorphic. We use a pairing technique
adopted from [17] to encode the paramorphic fold with hfoldr (cf. the new type
constructor D). This complication also illustrates the potential for further generic
function types, namely MG (D Maybe) m in this case.

13

Lämmel

Process all children; preserve the outermost constructor
allTP :: Monad m ⇒ TP m → TP m
allTP s = hfoldr (A f z )
where
f h t = S (do t ′ ← unS t
h ′ ← applyTP s h
return (I ((unI t ′ ) h ′ )))
z = S ◦ return ◦ I
Try to process the children until one succeeds; preserve the outermost constructor
oneTP :: MonadPlus m ⇒ TP m → TP m
oneTP s = G (λx → S (apply (poneTP s) x >>=
maybe mzero (return ◦ I ) ◦ fst ◦ unD))
The Duplicate type constructor for encoding type-preserving paramorphisms
newtype D t α = D (t α, t α)
unD (D x ) = x
Paramorphic helper for oneTP
poneTP :: MonadPlus m ⇒ TP m → MG (D Maybe) m
poneTP s = hfoldr (A f z )
where
f h t = S (do {t ′ ← unS t;
tp ← maybe mzero return (snd (unD t ′ ));
(do tc ← maybe mzero return (fst (unD t ′ ))
return (D (Just (tc h), Just (tp h)))
) ‘mplus‘ (
do h ′ ← applyTP s h
return (D (Just (tp h ′ ), Just (tp h)))
) ‘mplus‘ return (D (Nothing , Just (tp h)))})
z x = S (return (D (Nothing , Just x )))
Process all children; reduce the intermediate results
allTU :: Monad m ⇒ (u → u → u) → u → TU u m → TU u m
allTU op2 unit s = hfoldr (A f z )
where
f h t = S (do a ← unS t
b ← applyTU s h
return (C (unC a ‘op2 ‘ b)))
z = S ◦ return ◦ C ◦ const unit
Try to process the children until one succeeds; return the processed child
oneTU :: MonadPlus m ⇒ TU u m → TU u m
oneTU s = hfoldr (A f z )
where
f h t = S (cast (unS t) ‘mplus‘ cast (apply s h))
z = S ◦ const mzero
cast c = c >>= return ◦ C ◦ unC
Figure 11. Examples of one-layer traversal combinators

14

Lämmel

Sums of products vs. curried constructor applications The combinator hfoldr
roughly covers the sum and product cases in a polytypic definition [9] but without resorting to a constructor-free representation type. While a polytypic definition
deals with the many children in a term via nested binary products, hfoldr processes
all children in a curried constructor application as is. While the different constructors of a datatype amount to nested binary sums in a polytypic definition, the
base case of hfoldr handles the empty constructor application. Also note that polytypic definitions employ a designated declaration form for type induction while
functional strategies are defined as ordinary recursive functions. Finally, polytypic
definitions are normally implemented by compile-time specialisation. Functional
strategies only require a Term interface for datatypes to enable hfoldr and adhoc.

4 Largo
We are now in the position to define all kinds of traversal schemes in terms of the
strategy combinators and recursion. Before we present a portfolio of such schemes,
we impose some extra structure on our combinator suite in order to allow for a
uniform treatment of type-preserving and type-unifying traversal.
Overloading TP and TU The strategy combinators are usually typed in a manner that they can be used to derive strategies of both type TP and type TU. Hence,
one would expect that traversal schemes can be composed in a manner to work
for both type schemes as well. There are two asymmetries which we need to address. Firstly, there is no obvious way to write fold algebras that cover both TP
and TU. This is the reason why we have a oneTP vs. a oneTU, and an allTP vs.
an allTU. These combinators should be overloaded. Secondly, there is no uniform
way to combine the execution of two strategies of the same type. We can only compose alternative branches via choice. For the sake of sequential composition being
generic, the seq combinator insists on a type-preserving first argument. For the sake
of value passing to deliver an extra input to the second operand, the pass combinator insists on a type-unifying first argument. We suggest an overloaded composition
combinator comb as follows. In the TP instance, sequential composition via seq is
appropriate: the term as returned by the first type-preserving application is passed
to the second. In the TU instance, both strategies are evaluated via pass, and then,
the two resulting values are combined via the binary operation of a monoid. Note
that the Monoid class is also appropriate to harmonise the types of the one-layer
traversal combinators allTP and allTU for overloading. That is, the additional parameters for allTU are assumed to correspond to the monoid operations.
In Fig. 12, the overloaded combinators for traversal (cf. one and all) and combination of strategies (cf. comb) are defined. For completeness, we also overload idTP
and constTU in a way that an always succeeding strategy is defined (cf. skip). The
overloaded combinators are placed in two Haskell type classes StrategicMonadPlus and StrategicMonoid in order to deal with the different class constraints for
the overloaded combinators.
15

Lämmel

Overloading operator(s) involving MonadPlus
class StrategicMonadPlus s where
one :: s → s
instance MonadPlus m ⇒ StrategicMonadPlus (TP m) where
one = oneTP
instance MonadPlus m ⇒ StrategicMonadPlus (TU u m) where
one = oneTU
Overloading operators potentially involving Monoid
class StrategicMonoid s where
skip :: s
all :: s → s
comb :: s → s → s
instance Monad m ⇒ StrategicMonoid (TP m) where
skip = idTP
all = allTP
comb = seq
instance (Monad m, Monoid u) ⇒ StrategicMonoid (TU u m) where
skip = constTU mempty
all = allTU mappend mempty
comb = λf g → f ‘pass‘ λa → g ‘pass‘ λb → constTU (a ‘mappend ‘ b)
Figure 12. Classes of generic function combinators

Full traversal control In Fig. 13, we define traversal schemes in three groups. The
highly parameterised function traverse captures a rich class of traversal schemes as
illustrated by the given instantiations. Some of the type-preserving instantiations
of traverse were identified in [23]. In [13,12,14], some type-unifying instantiations
were added. In the definition of traverse, we separate out the distinguishing parameters of such more specific traversal schemes. The argument op is the function
combinator to compose term processing and recursive descent. The argument t defines how to descend into children. Finally, f is the strategy for term processing.
Here is the normative type for this ‘mother of traversal’:
traverse :: Monad m
⇒ (MG κ m → MG κ m → MG κ m)
→ (MG κ m → MG κ m)
→ MG κ m
→ MG κ m

-- Composition
-- Descent
-- Processor

We call this a normative type because the inferable type is much more general,
namely traverse :: (a → b → c) → (c → b) → a → c. Not even the normative
type captures all our intentions, e.g., the one that t actually specifies descent into
children. It is a topic for future work to capture such constraints in suitable types.
The scheme traverse is illustrated by several instances in the figure. The first two
instances all rec and one rec refine traverse to opt either for descent with all or
16

Lämmel

Traversal with parameters for different kinds of traversal control
traverse op t f
= f ‘op‘ t (traverse op t f )
all rec op
= traverse op all
= traverse op one
one rec op
full td
= all rec comb
= all rec (flip comb)
full bu
once td
= one rec choice
= one rec (flip choice)
once bu
stop td
= all rec choice
= all rec (flip choice)
stop bu
Traversal with propagation of an environment
propagate op t f u e = (f e) ‘op‘ (u e ‘pass‘ (λe ′ → t (propagate op t f u e ′ )))
= propagate comb all
full pe
once pe
= propagate choice one
= propagate choice all
stop pe
Traversal based on a notion of path
f ‘beloweq ‘ p
= once td (p ‘pass‘ λ() → once td f )
f ‘below ‘ p
= (one f ) ‘beloweq ‘ p
f ‘aboveeq ‘ p
= once bu (once td p ‘pass‘ λ() → f )
f ‘above‘ p
= f ‘aboveeq ‘ (one p)
belowlist f
= foldl below f ◦ reverse
abovelist f
= above f ◦ foldr above (constTU ())
′
(ps ‘prepost ‘ ps ) f = (f ‘abovelist ‘ ps ′ ) ‘belowlist ‘ ps
Figure 13. Traversal schemes

one, respectively. The postfixes “...td” or “...bu” stand for top-down or bottomup, respectively. The prefixes “full...”, “once...”, or “stop...” hint on the style of
traversal control: full traversal where all nodes are processed vs. single hit traversal
where the argument strategy has to succeed once vs. cut-off traversal where descent
stops when a subterm was processed successfully. All the more concrete schemes
are still overloaded as for the choice of TP vs. TU. To give an example, the scheme
full td models full traversal of a term where all nodes are processed in top-down
manner. In this example, the argument t for descent is instantiated with all (via
all rec). The argument op for the composition of term processing and recursive
descent is instantiated with comb.
Traversal with propagation The second group in Fig. 13 illustrates a class of
traversal schemes that go beyond simple node-wise processing. In addition to
traversal, propagation of an environment (abbreviated by the postfix “...pe”) is performed. The scheme propagate takes the same arguments op, t, and f as traverse.
In addition, the scheme carries a generic function argument u to update the environment before descent into the children, and an argument e for the initial environment.
Here is the normative type for propagate:

17

Lämmel

propagate :: Monad m
⇒ (MG κ m → MG κ m → MG κ m)
→ (MG κ m → MG κ m)
→ (e → MG κ m)
→ (e → TU e m)
→e
→ MG κ m

-- Composition
-- Descent
-- Processor
-- Environment update
-- Initial environment

The shown instances of propagate favour top-down traversal because bottom-up
traversal seems to be less obvious when combined with propagation. In is interesting to notice that the scheme propagate provides an alternative to using the environment monad [25] in a strategic program.
Path schemes The last group in Fig. 13 deals with traversal constrained by the path
leading to or starting from a node (say, a subterm). For this reason, we do not just
use a processor strategy f , but we also use predicates p for constraints. The scheme
beloweq attempts to process a subterm via f (not necessarily strictly) below a node
for which p succeeds; dually for aboveeq. The below and above variants enforce
the root of the processed subterm not to coincide with the constrained node. In the
definition of the path schemes, we use the simpler traversal schemes once td and
once bu from above. The types of the path schemes are as follows:
beloweq, below,
aboveeq, above :: (MonadPlus m, StrategicMonadPlus (MG κ m))
⇒ MG κ m
-- Processor
→ TU () m
-- Predicate
→ MG κ m
These types illustrate that predicates are encoded as type-unifying functions of type
TU () m where m is normally the Maybe monad or another instance of the MonadPlus class. So success and failure behaviour encodes the truth value.
The final three schemes in the group elaborate the more basic path schemes to deal
with lists of predicates. The schemes belowlist and abovelist constrain the prefix or
postfix of a node rooting a subtree of interest, respectively. The last scheme prepost
combines belowlist and abovelist. Note that the path scheme belowlist resolves the
remaining blind spot in the sample code for our running example in Fig. 2.
[End Of Symphony]

18

Lämmel

Appraisal
The four movements of this symphony combine certain bits of parametric polymorphism, type case (i.e., intensional polymorphism), polytypism, and overloading to
provide a concise and expressive model for functional strategies [14]. The development culminates in the last movement when typed highly parameterised traversal
schemes are defined. This paper makes the following overall contributions when
compared to previous work on strategic programming. Firstly, the developed model
is more concise and expressive than in our previous work [13,12,14]. Secondly, the
defined traversal schemes reach new limits of parameterisation. We shall elaborate
on these two claims accordingly.
The overall model “functional strategies = first-class polymorphic functions” was
already sketched in [14]. In addition to working out this model, we improved it
in two important ways. Firstly, the type schemes for type-preserving and typeunifying strategies are viewed as instances of one common type scheme Strategic.
This allows us to define combinators like choice and adhoc without commitment
to any specific type scheme. Secondly, we eliminated the need for an open-ended
list of primitive one-layer traversal combinators. To this end, we designed a generic
fold combinator for processing the immediate subterms of constructor applications.
A related language construct is described in [6]: pattern matching is generalised in
a way that generic access is granted to subterms of constructor applications. A
limited form of folds over constructor applications was first proposed in [12] in a
term-rewriting setting, but there it was by far less potent and it was difficult to type
due to the limitations of the underlying type system.
The key idea to define traversal schemes in terms of one-layer traversal combinators
carries over from the seminal work on term rewriting strategies [23]. The present
paper reaches a new level of genericity for the following two reasons. Firstly, we
effectively overload the two prime type schemes of generic traversal. This allows
us to capture meaningful traversal schemes without anticipating their use for transformation vs. analysis. Secondly, we identify a few highly parameterised traversal
schemes with parameters for various forms of control. These ‘skeleton’ or ‘meta’
schemes capture more concrete traversal schemes favoured in previous work.
Acknowledgement The following people contributed beats to this polymorphic
symphony: Jan Kort, Andres Löh, Simon Peyton-Jones, Joost Visser, and Stephanie
Weirich. I am grateful for the remarks and suggestions by the anonymous WRS’02
referees. I devote my first symphony to Berenike and Bernadette.

References
[1] M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic Typing in a Statically Typed
Language. ACM Transactions on Programming Languages and Systems, 13(2):237–
268, Apr. 1991.

19

Lämmel

[2] M. Abadi, L. Cardelli, B. Pierce, and D. Rémy. Dynamic Typing in Polymorphic
Languages. In Proceedings of the 1992 ACM Workshop on ML and its Applications,
pages 92–103, San Francisco, June 1992. Association for Computing Machinery.
[3] P. Borovanský, C. Kirchner, H. Kirchner, and C. Ringeissen. Rewriting with strategies
in ELAN: a functional semantics. International Journal of Foundations of Computer
Science, 12(1):69–95, 2001.
[4] M. Brand, P. Klint, and J. Vinju. Term rewriting with traversal functions. Technical
Report SEN-R0121, CWI, July 2001.
[5] J. Cockett and D. Spencer. Strong categorical datatypes I. In R. Seely, editor,
Proceedings Int. Summer Category Theory Meeting, Montréal, Québec, 23–30 June
1991, volume 13 of Canadian Mathematical Society Conf. Proceedings, pages 141–
169. American Mathematical Society, Providence, RI, 1992.
[6] E. Dolstra and E. Visser. First-class rules and generic traversal. Technical report,
Universiteit Utrecht, UU-CS-2001-38, 2001. Technical report.
[7] J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l’arithétique
d’ordre supérieur. PhD thesis, Université Paris VII, 1972.
[8] R. Harper and G. Morrisett. Compiling polymorphism using intentional type
analysis. In Conference Record of POPL ’95: 22nd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, San Francisco, Calif., pages
130–141. ACM, Jan. 1995.
[9] J. Jeuring and P. Jansson. Polytypic programming. In J. Launchbury, E. Meijer, and
T. Sheard, editors, 2nd Int. School on Advanced Functional Programming, Olympia,
WA, USA, 26–30 Aug 1996, volume 1129 of LNCS, pages 68–114. Springer-Verlag,
Berlin, 1996.
[10] M. Jones.
Functional Programming with Overloading and Higher-Order
Polymorphism.
In J. Jeuring and E. Meijer, editors, Advanced Functional
Programming, volume 925 of LNCS, pages 97–136. Springer-Verlag, 1995.
[11] M. Jones. First-class polymorphism with type inference. In Conference Record
of POPL ’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 483–496, Paris, France, 15–17 Jan. 1997.
[12] R. Lämmel. Typed Generic Traversal With Term Rewriting Strategies. Journal of
Logic and Algebraic Programming, 54, September 2002.
[13] R. Lämmel and J. Visser. Type-safe Functional Strategies. In Draft proc. of SFP’00,
St Andrews, July 2000.
[14] R. Lämmel and J. Visser.
Typed Combinators for Generic Traversal.
In
S. Krishnamurthi and C. Ramakrishnan, editors, Proc. of PADL’02, volume 2257 of
LNCS, pages 137–154. Springer-Verlag, Jan. 2002.
[15] R. Lämmel, J. Visser, and J. Kort. Dealing with Large Bananas. In J. Jeuring, editor,
Proc. of WGP’2000, Technical Report, Universiteit Utrecht, pages 46–59, July 2000.

20

Lämmel

[16] K. Lieberherr. Adaptive Object-Oriented Software: The Demeter Method with
Propagation Patterns. PWS Publishing Company, Boston, 1996.
[17] L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–424, 1992.
[18] E. Meijer, M. Fokkinga, and R. Paterson. Functional Programming with Bananas,
Lenses, Envelopes, and Barbed Wire. In J. Hughes, editor, Functional Programming
Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA,
August 26-30, 1991, Proceedings, volume 523 of LNCS, pages 124–144. SpringerVerlag, 1991.
[19] S. Peyton Jones and J. Hughes (eds.). Haskell 98: A non-strict, purely functional
language. http://www.haskell.org/onlinereport/, 1999.
[20] J. Reynolds. Towards a Theory of Type Structures. In Programming Symposium
(Colloque sur la Programmation, Paris), volume 19 of LNCS, pages 408–425.
Springer-Verlag, 1974.
[21] J. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason,
editor, Proc. of 9th IFIP World Computer Congress, Information Processing ’83, Paris,
France, 19–23 Sept 1983, pages 513–523. North-Holland, Amsterdam, 1983.
[22] S. Thompson. Higher-order + Polymorphic = Reusable. Unpublishled; http://
www.cs.ukc.ac.uk/pubs/1997/224, May 1997.
[23] E. Visser, Z.-e.-A. Benaissa, and A. Tolmach. Building Program Optimizers with
Rewriting Strategies. In Proceedings of the third ACM SIGPLAN International
Conference on Functional Programming (ICFP’98), pages 13–26. ACM Press,
September 1998.
[24] P. Wadler. Theorems for free! In Proceedings 4th Int. Conf. on Funct. Prog.
Languages and Computer Arch., FPCA’89, London, UK, 11–13 Sept 1989, pages 347–
359. ACM Press, 1989.
[25] P. Wadler. The essence of functional programming. In ACM, editor, Conference
record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, Albuquerque, New Mexico, pages 1–14. ACM Press, 1992.
[26] P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In ACM
SIGPLAN-SIGACT, editor, Conference Record of the 16th Annual ACM Symposium
on Principles of Programming Languages (POPL ’89), pages 60–76, Austin, TX,
USA, Jan. 1989. ACM Press.
[27] S. Weirich. Type-safe cast. In ACM SIGPLAN International Conference on
Functional Programming (ICFP’00), pages 58–67, Montreal, Sept. 2000. ACM Press.
[28] S. Weirich. Higher-Order Intensional Type Analysis. In D. L. Métayer, editor,
Programming Languages and Systems: 11th European Symposium on Programming,
ESOP 2002, Grenoble, France, number 2305 in LNCS, pages 98–114, 2002.

21

