1: \documentclass{entcs} 

2: 

3: \usepackage{entcsmacro}

4: \usepackage{times}

5: \usepackage[english]{babel}

6: \usepackage{graphics}

7: \usepackage{url}

8: \usepackage{lhs2TeXPreamble}

9: \usepackage{boxedminipage}

10: 

11: 

12: 

13: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

14: 

15: 

16: \def\lastname{L{\"a}mmel}

17: \newcommand{\aprime}{a'}

18: \newcommand{\cod}{\kappa}

19: \newcommand{\flc}{$\=$}

20: \newcommand{\lc}{$\>$}

21: \renewcommand{\qquad}{\hspace{55\in}}

22: \newcommand{\chapskip}{\vspace{-650\in}}

23: \newcommand{\snipheader}[1]{#1\vspace{-15\in}}

24: \newcommand{\mysection}[1]{\medskip

25: 

26: \noindent

27: {\large\textbf{#1}}}

28: 

29: 

30: \newcommand{\myparagraph}[1]{\medskip

31: 

32: \noindent\textbf{#1}\ }

33: \newenvironment{codesize}{\small}{}

34: \newcommand{\myfigure}[4]{

35: \begin{figure}[#4]

36: {\small

37: \framebox{\parbox{.962\textwidth}{#1\hfill\vspace{-80\in}}}%

38: \vspace{-10\in}\caption{#2}

39: \label{#3}}

40: \end{figure}

41: }

42: 

43: 

44: 

45: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

46: 

47: 

48: 

49: \begin{document}

50: 

51: \begin{frontmatter}

52: 

53: \title{The Sketch of a Polymorphic Symphony}

54: 

55: \vspace{-42\in}

56: 

57: \author{Ralf L{\"a}mmel}

58: \address{Email:

59:          \href{mailto:ralf@cs.vu.nl}%

60:          \texttt{\normalshape ralf@cs.vu.nl}\\

61:          CWI, Kruislaan 413, NL-1098 SJ Amsterdam\\

62:          Vrije Universiteit, De Boelelaan 1081a, NL-1081 HV Amsterdam}

63: 

64: \begin{abstract}

65: In previous work, we have introduced \emph{functional} strategies,

66: that is, first-class generic functions that can traverse into terms of

67: any type while mixing uniform and type-specific behaviour. In the

68: present paper, we give a detailed description of one particular

69: Haskell-based model of functional strategies. This model is

70: characterised as follows. Firstly, we employ \emph{first-class

71: polymorphism} as a form of second-order polymorphism as for the mere

72: types of functional strategies. Secondly, we use an encoding scheme of

73: run-time \emph{type case} for mixing uniform and type-specific

74: behaviour. Thirdly, we base all traversal on a fundamental combinator

75: for \emph{folding over constructor applications}.

76: 

77: Using this model, we capture common strategic traversal schemes in a

78: highly parameterised style. We study two original forms of

79: parameterisation. Firstly, we design parameters for the specific

80: control-flow, data-flow and traversal characteristics of more concrete

81: traversal schemes. Secondly, we use overloading to postpone commitment

82: to a specific type scheme of traversal. The resulting portfolio of

83: traversal schemes can be regarded as a challenging benchmark for

84: setups for typed generic programming.

85: 

86: The way we develop the model and the suite of traversal schemes, it

87: becomes clear that parameterised + typed strategic programming is best

88: viewed as a potent combination of certain bits of parametric,

89: intensional, polytypic, and ad-hoc polymorphism.

90: \end{abstract}

91: 

92: \end{frontmatter}

93: 

94: 

95: 

96: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

97: 

98: 

99: 

100: \mysection{Arrangement}

101: 

102: \myparagraph{The running example}

103: %

104: Given is a tree, say a term. We want to operate on a certain

105: subterm. We search for the subterm $t$ in some traversal order, be it

106: top-down and left-to-right. We want to further constrain $t$ in the

107: sense that it should occur on a certain path, namely below $k$ nodes

108: the fitness of which is determined by predicates. Once we found $t$

109: below certain nodes $n_1$, \ldots, $n_k$, we either want to select $t$

110: as is, \emph{or} we want to compute some value from $t$, \emph{or} we

111: want to transform $t$ in its context in the complete tree. This

112: traversal scenario is illustrated in Fig.~\ref{F:tree} for $k=2$. This

113: sort of problem is very common in programming over tree and graph

114: structures, e.g., in adaptive object-oriented

115: programming~\cite{Lieberherr96}. One might consider additional forms

116: of conditions, e.g., certain kinds of nodes that should \emph{not} be

117: passed, or further forms of computation, e.g., \emph{cumulative}

118: computation along the path.

119: 

120: 

121: 

122: \begin{figure}[ht!]

123: \begin{boxedminipage}{\hsize}

124: \parbox{.30\textwidth}{

125: \resizebox{!}{450\in}%

126: {\includegraphics{problem.eps}}}\hfill\parbox{.67\textwidth}{%

127: %

128: {\small \textsf{Find the subtree $t$ below $n_2$ in turn below $n_1$.

129: We assume two predicates $p_1$ and $p_2$ to identify $n_1$ and $n_2$.

130: We further assume a generic function $f$ to identify and then to

131: process $t$.}}}\vspace{-20\in}%

132: \end{boxedminipage}

133: \caption{Processing a subtree that is reachable via a path}

134: \label{F:tree}

135: \medskip

136: \end{figure}

137: 

138: 

139: 

140: \myparagraph{Sample code}

141: %

142: In the present paper, we refrain from discussing real-world

143: application snippets but we sketch an illustrative instance of the

144: running example in Fig.~\ref{F:running}. As one can see, we assume a

145: combinator \emph{belowlist} that captures the described scheme of path

146: traversal. In the figure, we define a function \emph{test42} to

147: traverse into a sample term \emph{term1} in terms of

148: \emph{belowlist}. The traversal looks for a subterm of type

149: \emph{SortB} to extract its integer component if it occurs on a path

150: with two \emph{SortB} subterms with the integer components 1 and

151: 3. There are a few blind spots in the figure (cf.\ ``\ldots'') which

152: we will resolve in the course of the concert. As the following Hugs

153: session shows, the traversal yields 42:

154: 

155: \myfigure{%

156: \input{snip/running.math}%

157: }{%

158: Illustrative Haskell code for the running example%

159: }{%

160: F:running}{b!}

161: 

162: 

163: \begin{quote}

164: \mbox{}\vspace{-40\in}\\

165: \ \texttt{Main$>$ test42}\\%

166: \ \texttt{Just 42}\\%

167: \ \texttt{Main$>$}

168: \end{quote}

169: 

170: 

171: 

172: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

173: 

174: 

175: 

176: \myparagraph{Side conditions}

177: %

178: The above traversal scenario should be complemented by a few useful

179: side conditions. We assume that (i) we deal with \emph{many sorts},

180: say user-supplied systems of named, mutually recursive datatypes such

181: as syntaxes and formats.  So a traversal will encounter terms of

182: different types. We further require that (ii) traversal schemes are

183: \emph{statically type-safe}, that is, a traversal always delivers a

184: type-correct result (if any) without even attempting the construction

185: of any ill-typed term. Furthermore, we insist on (iii) a

186: \emph{parameterised} solution where the overall traversal scheme is

187: strictly separated from problem-specific ingredients. Also, the kind

188: of processor (recall selection vs.\ computation vs.\ transformation)

189: should not be anticipated. Recall that the actual traversal in

190: Fig.~\ref{F:running} is indeed synthesised by passing predicates and a

191: processor to a presumably overloaded traversal scheme

192: \emph{belowlist}. Last but not least, we require that (iv) a proper

193: combinator approach is adopted where one can easily compose traversals

194: and schemes thereof. As for the assumed \emph{belowlist} combinator,

195: its definition should be a concise and suggestive one-liner based on

196: more fundamental traversal combinators. With combinators, we can

197: easily toggle variation points of traversal, e.g., top-down vs.\

198: bottom-up, left-to-right vs.\ right-to-left, first match vs.\ all

199: matches, and so on.

200: 

201: 

202: 

203: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

204: 

205: 

206: 

207: \myparagraph{Conducted by Strafunski}

208: %

209: If \emph{any} of the above side conditions is given up, the treatment

210: of the scenario becomes less satisfying. If you do not insist on

211: static type safety, then you can resort to Prolog, or preferably to

212: Stratego~\cite{VBT98} which supports at least limited type

213: checks. Types are however desirable to discipline the instantiation of

214: traversal schemes. If you even want to do away with parameterisation

215: and combinator style, then XSLT is your language of choice. If types

216: appeal to you, then you might feel tempted to consider polytypic

217: functional programming~\cite{JJ96}.  However, corresponding language

218: designs do not provide support for generic programming in a combinator

219: style because polytypic values are not first-class citizens. If you

220: are as demanding and simplistic as we are, then you use the

221: \emph{Strafunski}-style of generic programming in Haskell as

222: introduced by the present author and Joost Visser

223: in~\cite{LV02-PADL}.\footnote{URL \url{http://www.cs.vu.nl/Strafunski}

224: where \url{Stra} refers to strategies as in strategic term

225: rewriting~\cite{BKKR01,VBT98}, \url{fun} refers to functional

226: programming, and their harmonious composition is a homage to the music

227: of Igor Stravinsky.}  The style is centred around the notion of

228: functional strategies~---~\emph{first-class} generic functions that

229: can \emph{traverse} into terms of any type while mixing uniform and

230: \emph{type-specific} behaviour.

231: 

232: 

233: 

234: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

235: 

236: 

237: 

238: \myparagraph{The movements}

239: %

240: No previous knowledge of strategic programming is required to enjoy

241: this symphony. We develop a model of functional strategies based on

242: Haskell~98~\cite{HaskellReport} extended with first-class

243: polymorphism~\cite{Jones97}. The symphony consists of four

244: movements. In Sec.~1, the type \emph{Strategic} of functional

245: strategies is initiated and inhabited with parametrically

246: polymorphic~\cite{Reynolds83,Wadler89} combinators.  In Sec.~2, we

247: integrate a combinator \emph{adhoc} to update functional strategies

248: for a specific type. This combinator relies on run-time type

249: case~---~a notion that was studied in the context of intensional

250: polymorphism~\cite{HM95,Weirich02}. In Sec.~3, we integrate a

251: fundamental combinator \emph{hfoldr} to perform primitive portions of

252: traversal by folding over the immediate subterms of a term without

253: anticipation of recursion.  This kind of folding can be regarded as a

254: variation on polytypism~\cite{JJ96}. In Sec.~4, we use overloading,

255: say ad-hoc polymorphism~\cite{WB89,Jones95}, to treat different types

256: of traversal (recall selection vs.\ computation vs.\ transformation)

257: in a uniform manner. At this level of genericity, we succeed in

258: defining a portfolio of highly parameterised traversal schemes,

259: including the scheme \emph{belowlist} that is needed in the running

260: example. This portfolio demonstrates the expressiveness and

261: conciseness of functional strategies.%

262: %

263: \footnote{%

264: %

265: The code shown in the paper is fully operational in Haskell (tested

266: with Hugs~98; Dec.\ 2001 version). A paper-specific \emph{Strafunski}

267: distribution with illustrative examples can be downloaded from the

268: paper's web-site \url{http://www.cwi.nl/~ralf/polymorphic-symphony/}.

269: This distribution also comes with a strategic Haskell program that

270: provides generative tool support for strategic programming against

271: user-supplied datatypes.}

272: 

273: 

274: 

275: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

276: 

277: 

278: 

279: \section{Moderato}

280: 

281: In this section, we initiate the type of generic functions that model

282: functional strategies. For the sake of a systematic development, we

283: will first focus on the most simple, i.e., the \emph{parametrically

284: polymorphic}~\cite{Reynolds83,Wadler89} dimension of the corresponding

285: type scheme. In the subsequent two movements, we go beyond this

286: boundary by adding expressiveness for run-time type case and generic

287: term traversal.

288: 

289: 

290: 

291: \myfigure{%

292: \input{snip/generic.math}%

293: }{%

294: Functional strategies as first-class polymorphic functions%

295: }{%

296: F:generic}{}

297: 

298: 

299: 

300: \myparagraph{First-class polymorphic functions}

301: %

302: In Fig.~\ref{F:generic}, we use a type synonym \emph{Parametric} with

303: two parameters $\alpha$ and $\cod$ to capture the general type scheme

304: $\alpha \to \cod\ \alpha$ of functional strategies. As one can see,

305: the parameter $\alpha$ corresponds to the domain of the function type,

306: and $\cod$ is used to construct the co-domain from $\alpha$. Common

307: options for the co-domain type constructor $\cod$ are the identity

308: type constructor $I$ and the constant type constructor $C$ as defined

309: in the figure, too. Based on the type scheme \emph{Parametric}, we

310: define the ultimate datatype \emph{Strategic} that captures the

311: polymorphic function type for functional strategies.  Polymorphism is

312: expressed via the universal quantifier ``$\forall$'', and the fact

313: that we ultimately need to go beyond parametric polymorphism is

314: anticipated via a class constraint ``$\emph{Term}\ \alpha$'' for

315: `strategic polymorphism'. Note that the ``$\forall$'' occurs in the

316: scope of the \emph{component} of the constructor $G$. This form of

317: second-order polymorphism, where polymorphic entities are wrapped by

318: datatype constructors, is called first-class

319: polymorphism~\cite{Jones97}, and it is a common language extension of

320: Haskell~98. (Implicit) top-level universal quantification would be

321: eventually insufficient to construct strategy combinators.

322: 

323: 

324: 

325: \myparagraph{Strategic type schemes}

326: %

327: In Fig~\ref{F:generic}. we also define the identity type constructor

328: $I$, the constant type constructor $C$, and the constructor $S$ for

329: sequential composition of type constructors. Based on these, we derive

330: three classes \emph{MG}, \emph{TP}, and \emph{TU} of generic functions

331: from \emph{Strategic}. The synonym \emph{MG} captures monadic

332: strategies.  Monadic style~\cite{Wadler92} is favoured here because

333: that way we can deal with effects during traversal, e.g., success and

334: failure, state, or nondeterminism. We could also consider extra

335: variants for non-monadic strategies but we instead assume that the

336: trivial identity monad is used for that purpose. The synonym \emph{TP}

337: instantiates \emph{MG} via $I$ so that \emph{T}ype-\emph{P}reserving

338: strategies are identified. The synonym \emph{TU} instantiates

339: \emph{MG} via $C$ so that \emph{T}ype-\emph{U}nifying strategies are

340: identified, that is, polymorphic functions with a fixed result

341: type. At the bottom of Fig.~\ref{F:generic}, we provide trivial

342: definitions of `application' combinators. The combinator \emph{apply}

343: complements ordinary function application by some unwrapping that

344: accounts for first-class polymorphism (cf.\ \emph{unG}), and for

345: type-constructor composition (cf.\ \emph{unS}). The combinators

346: \emph{applyTP} and \emph{applyTU} specialise \emph{apply} for

347: \emph{TP} and \emph{TU} to hide the employment of the datatypes $I$

348: and $C$ for co-domain construction. Their result types point out the

349: basic type schemes for \emph{TP} and \emph{TU} without any noise.%

350: %

351: \footnote{%

352: %

353: We should revise our sample code from Fig.~\ref{F:running} to use

354: \emph{applyTU} in the synthesis of the traversal:

355: \input{snip/revise.math}}

356: 

357: 

358: \myfigure{

359: \input{snip/constants.math}

360: }{Parametrically polymorphic strategies}{F:constants}{}

361: 

362: 

363: 

364: \myparagraph{Nullary combinators}

365: %

366: Let us start to inhabit the strategy types while restricting ourselves

367: to parametrically polymorphic inhabitants. In Sec.~2 and Sec.~3, we

368: will inhabit the type \emph{Strategic} in other ways by employing

369: designated combinators for `strategic polymorphism'. If we neglect the

370: monadic facet of functional strategies for a second, then there are

371: few parametrically polymorphic inhabitants: the identity function for

372: the type-preserving scheme, and constant functions for the

373: type-unifying scheme. This is generalised for the monadic setup in

374: Fig.~\ref{F:constants}. For clarity, we define the function

375: \emph{para} that approves a parametrically polymorphic function as a

376: member of \emph{Strategic}. While its definition coincides with the

377: constructor $G$, its type insists on a parametrically polymorphic

378: argument (no mentioning of the \emph{Term} class). Using \emph{para},

379: we can define the identity strategy \emph{idTP} and a combinator

380: \emph{constTU} for constant strategies. Relying on the extended monad

381: class \emph{MonadPlus}, we can also define the always failing strategy

382: \emph{fail} in terms of the member \emph{mzero} denoting failure,

383: e.g., \emph{Nothing} in the case of the \emph{Maybe} instance of the

384: \emph{MonadPlus} class. The inhabitant \emph{fail} is meant to

385: illustrate that functional strategies might exhibit success and

386: failure behaviour, or they even might be non-deterministic depending

387: on the actual choice of the \emph{MonadPlus} instance.

388: 

389: 

390: 

391: \myfigure{

392: \input{snip/combinators.math}

393: }{Composition combinators for functional

394: strategies}{F:combinators}{}

395: 

396: 

397: 

398: \myparagraph{Binary combinators}

399: %

400: In Fig.~\ref{F:combinators}, we define three prime combinators to

401: compose functional strategies. The combinator \emph{seq} lifts monadic

402: sequencing of function applications to the strategy level (cf.\

403: ``$\bind$''). The combinator \emph{pass} composes two strategies which

404: share a term argument and where the result of the first strategy is

405: passed as additional input to the second strategy. The combinator

406: \emph{choice} composes alternative function applications. The actual

407: kind of choice depends on the (extended) monad which is employed in

408: the definition (cf.\ class \emph{MonadPlus} and its member

409: \emph{mplus}), e.g., the \emph{Maybe} monad for partiality or the

410: \emph{List} monad for multiple results. In the definitions of the

411: binary combinators, we use \emph{apply} to deploy the polymorphic

412: function arguments, and we use $G$ to re-wrap the composition as a

413: polymorphic function of type \emph{Strategic}. In composing functional

414: strategies, we cannot use the disciplined \emph{para} as a substitute

415: for $G$ because, eventually, we want to compose functions that go

416: beyond parametric polymorphism.

417: 

418: 

419: 

420: \myparagraph{Rank-2 types}

421: %

422: A crucial observation is that the composition combinators \emph{seq},

423: \emph{pass} and \emph{choice} really enforce us to use some form of

424: second-order polymorphism~\cite{GirardPhD,Reynolds74}. Other function

425: combinators like ``$\circ$'' or ``$\bind$'' have rank-1 types, that

426: is, they are quantified at the top-level. This implies that they

427: (also) accept monomorphic function arguments. By contrast, the types

428: of \emph{seq}, \emph{pass} and \emph{choice} have rank-2 types, that

429: is, they are quantified \emph{argument-wise}. These types model

430: insistence on polymorphic function arguments as required for

431: \emph{generic} programming in a combinator style. Rank-2 types are not

432: just needed for the binary composition combinators, but also for the

433: upcoming traversal primitive, and for non-recursive and recursive

434: traversal combinators. Actually, generic traversal in a combinator

435: style necessitates rank-2 types. This is because, in general, a

436: traversal \emph{scheme} takes universally quantified arguments.

437: Nested quantification reflects that ingredients of traversals must be

438: applicable to subterms of any type.

439: 

440: 

441: 

442: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

443: 

444: 

445: 

446: \section{Larghetto}

447: 

448: At this point in our polymorphic concert, we still lack the original

449: expressiveness of functional strategies: the ability to perform

450: traversal into terms while mixing uniform and type-specific

451: behaviour. This section and the subsequent one are concerned with this

452: `strategic polymorphism'. In the present section, we provide a

453: combinator \emph{adhoc} for type-specific customisation of functional

454: strategies. In the next section, generic traversal into terms will be

455: enabled.

456: 

457: 

458: 

459: \myparagraph{Informal explanation}

460: %

461: The type of the \emph{adhoc} combinator is given at the top of

462: Fig.~\ref{F:adhoc}. The combinator allows us to update an existing

463: strategy for a specific type via a monomorphic function. We call this

464: idiom \emph{type-based function dispatch}. We also use the term

465: \emph{strategy update} because of the affinity to point-wise

466: modification of ordinary functions. In this sense, strategy update is

467: about ``type-wise'' modification of a polymorphic function. Here are

468: two samples of strategy update:

469: 

470: 

471: 

472: \input{snip/negbool.math}

473: 

474: \input{snip/recint.math}

475: 

476: \noindent

477: The strategy \emph{negate\_bool} behaves like \emph{idTP} most of the

478: time but it performs negation when faced with a Boolean (cf.\

479: ``$\neg$'').  We use the \emph{Identity} monad. The strategy

480: \emph{return\_int} is meant to recognise integers, that is, it simply

481: fails if it does not find an integer. So we use the \emph{Maybe} monad

482: to deal with failure. Note that we use type-specialised variants

483: \emph{adhocTP} and \emph{adhocTU} as defined in

484: Fig.~\ref{F:adhoc}. They allow the strategic programmer to forget

485: about wrapping and unwrapping $I$, $C$, and $S$.

486: 

487: \medskip

488: 

489: \noindent

490: In Fig.~\ref{F:blind}, we use strategy update to resolve two blind

491: spots in Fig.~\ref{F:running}~---~the sample code for our running

492: example. The strategy \emph{sortb2int} extracts an integer from a term

493: of type \emph{SortB}. The strategy \emph{sortbEqInt} insists on a

494: specific extracted integer. This is a predicate-like strategy which

495: either returns $\mathit{Just}\,()$ or $\mathit{Nothing}$.

496: 

497: 

498: 

499: \myfigure{%

500: \input{snip/adhoc.math}}{%

501: Updating functional strategies by type-specific cases% 

502: }{%

503: F:adhoc%

504: }{t}

505: 

506: 

507: 

508: \myfigure{%

509: \input{snip/blind.math}}{%

510: Use of strategy update in the running example% 

511: }{%

512: F:blind%

513: }{t}

514: 

515: 

516: 

517: \myparagraph{Definition of strategy update}

518: %

519: Given a strategy \emph{poly} of type $\mathit{Strategic}\ \cod$, and a

520: function \emph{mono} of type $\mathit{Parametric}\ \alpha\ \cod$, the

521: updated function $\mathit{adhoc}\ \mathit{poly}\ \mathit{mono}$

522: branches according to the type $\alpha'$ of an eventual input value

523: $v$: if $\alpha=\alpha'$, then \emph{mono} is applied to $v$,

524: otherwise \emph{poly}. That is:

525: \[

526: \mathit{adhoc}\ \mathit{poly}\ \mathit{mono}\ v\ =\ \left\{%

527: \begin{array}{ll}

528: \mathit{mono}\ v, & \mbox{if type of $v$ = domain of

529: $\mathit{mono}$}\vspace{-30\in}\\

530: \mathit{poly}\ v, & \mbox{otherwise}

531: \end{array}

532: \right.

533: \]

534: 

535: \medskip

536: 

537: \noindent

538: Strategy update can be considered as a simple and very disciplined

539: form of type case at run-time. Such type case was studied in the

540: context of intensional polymorphism~\cite{HM95,Weirich02}. One might

541: feel tempted to compare strategy update to dynamic

542: typing~\cite{ACPP91,ACPR92} but note that first-class polymorphic

543: strategies, as designed in the present paper, operate on terms of

544: algebraic datatypes as opposed to `dynamics'. Dynamic typing can be

545: employed, however, in other models of functional strategies, e.g., in

546: the way described in~\cite{LV02-PADL}.

547: 

548: 

549: 

550: \myfigure{%

551: \input{snip/typecase.math}}{%

552: Per-datatype support for strategy update%

553: }{%

554: F:typecase%

555: }{b!}

556: 

557: 

558: 

559: \myparagraph{Encoding scheme}

560: %

561: A strategic programmer considers the \emph{adhoc} combinator as a

562: primitive. In Haskell, we cannot define the \emph{adhoc} combinator

563: once and for all, but it can be supported per datatype. This is

564: precisely what the \emph{Term} class is needed for in the definition

565: of \emph{Strategic} (recall Fig.~\ref{F:generic}). So we basically

566: place the \emph{adhoc} combinator in the \emph{Term} class with the

567: provision to add another member for generic traversal later. There are

568: several ways to encode strategy update. We will explain here a scheme

569: that is inspired by type-safe cast as of~\cite{Weirich00}. In fact, we

570: revise this scheme to model a \emph{single-branching type case} (as

571: opposed to a plain type cast) while assuming \emph{nominal type

572: analysis} (as opposed to a structural one).

573: 

574: \medskip

575: 

576: \noindent

577: The scheme is illustrated in Fig.~\ref{F:typecase}. In the \emph{Term}

578: class, we place a primed member $\mathit{adhoc}'$ with an implicitly

579: quantified type. This is necessary because we need to link the type

580: parameter $\alpha$ of the class declaration to the type of

581: $\mathit{adhoc}'$. In the type of $\mathit{adhoc}'$, the parameter

582: $\alpha$ acts as a place-holder for the term type of the updating

583: monomorphic function, and there is an extra parameter $\alpha'$ for

584: the term type of the input term. The first-class polymorphic

585: \emph{adhoc} is easily derived from $\mathit{adhoc}'$ via wrapping

586: with $G$ as shown in the figure. The overall idea for the

587: implementation of $\mathit{adhoc}'$ is to compare the term type

588: $\alpha$ of the update with the term type $\alpha'$ of the ultimate

589: input term. To this end, we need to encode a kind of decision matrix

590: to check for $\alpha=\alpha'$ for all possible combinations of term

591: types. The dimension for $\alpha$ is taken care of by overloading

592: $\mathit{adhoc}'$ in $\alpha$. The dimension for $\alpha'$ is taken

593: care of by extra helper members~---~one for each type. These helper

594: members model strategy update for a specific type of update while they

595: are overloaded in the input term type. This is exemplified in the

596: figure with the helpers \emph{int}, \emph{sorta}, and \emph{sortb} for

597: the sample term types in our running example (cf.\

598: Fig.~\ref{F:running}). It makes sense to initialise the definitions of

599: the helper members to resort to \emph{poly} by default. In any given

600: instance of the \emph{Term} class, we need to define

601: $\mathit{adhoc}'$, and we override the default definition for the

602: specific helper member that handles the instance's type. The

603: definition of $\mathit{adhoc}'$ simply dispatches to the helper

604: member. The helper member is redefined to dispatch to \emph{mono}

605: instead of \emph{poly}. This is again illustrated for the sample term

606: types in our running example. Note that we are faced with a

607: closed-world assumption because we need one member per term type in

608: our strategic program (see~\cite{LV02-PADL} for another model).

609: 

610: 

611: 

612: \myparagraph{Mixture of specificity and genericity}

613: %

614: The contribution of strategy update is the following. It allows us to

615: lift type-specific behaviour in a type-safe and transparent way to the

616: strategy level. Note that parametric polymorphism only works the other

617: way around: a polymorphic function can be applied to a value of a

618: specific type, and in fact, the actual behaviour will be entirely

619: uniform, independent of the specific

620: type~\cite{Reynolds83,Wadler89}. In generic programming with

621: traversals, type-specific customisation is indispensable because a

622: traversal is typically concerned with problem-specific datatypes and

623: constructors. At a more general level, one can say that the

624: \emph{adhoc} combinator implements the following admittedly very much

625: related requirements regarding the tension between genericity and

626: specificity:

627: %

628: \begin{description}

629: \item[(i)] Separability of generic and type-specific behaviour

630: \item[(ii)] Composability of generic and type-specific behaviour

631: \item[(iii)] First-class status of updatable generic functions

632: \end{description}

633: %

634: In functional programming, the common approach to the definition of

635: polymorphic functions with type-specific behaviour is to use ad-hoc

636: polymorphism, say type and constructor classes~\cite{WB89,Jones95}

637: as supported in Haskell. This approach does not meet the above

638: requirements because a class and its instances form a declaration

639: unit. Any new combination of generic and type-specific behaviour has

640: to be anticipated by a dedicated class. Hence, strategy update is

641: complementary.

642: 

643: 

644: 

645: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

646: 

647: 

648: 

649: \section{Allegretto}

650: 

651: Ultimately, functional strategies are meant to perform term traversal.

652: Hence, we need to add another bit of polymorphism. In fact, the kind

653: of term traversal that we envisage can be regarded as a variation on

654: polytypism~\cite{JJ96}. That is, recursion into terms is performed on

655: the basis of the structure of the underlying algebraic

656: datatypes. First we will briefly categorise traversal approaches in

657: previous work. Then we will generalise one of the approaches to

658: contribute a very flexible means of traversal to the ongoing

659: reconstruction of functional strategies.

660: 

661: 

662: 

663: \myparagraph{Traversal approaches}

664: %

665: We identify the following categories:

666: \begin{description}

667: \item[(i)] Recursive traversal schemes~\cite{MFP91,CS92,Thompson97,LVK00,BKV01}

668: \item[(ii)] One-layer traversal

669: combinators~\cite{VBT98,Laemmel02-TGT,LV02-PADL}

670: \item[(iii)] Traversal by type induction~\cite{JJ96}

671: \item[(iv)] Traversal at a representation-type level~\cite{BKKR01}

672: \end{description}

673: %

674: (i) Recursive traversal schemes, e.g., generalised folds or iterators

675: over data structures, follow a fixed scheme of recursion into terms,

676: and the style of composition of intermediate results is also

677: intertwined with the recursion scheme. (ii) One-layer traversal

678: combinators add flexibility because they do not recurse into terms by

679: themselves but they rather capture single steps of traversals. Hence,

680: different recursion schemes and different means to compose

681: intermediate results can still be established by plain (recursive)

682: function definition. The value of one-layer traversal combinators was

683: identified in the context of strategic term rewriting~\cite{VBT98} in

684: the application domain of program transformation. (iii) Polytypic

685: programming suggests that a traversal can also be viewed as a function

686: that is defined by induction on the argument type. So one can capture

687: term traversal schemes by polytypic definitions. However, these

688: definitions could not be used in a combinator style because existing

689: language designs do not cover `rank-2 polytypism', that is, one cannot

690: pass one polytypic function to another one. (iv) Finally, a programmer

691: can resort to a universal representation type to perform

692: traversal. Here we assume that the programmer is provided with

693: implosion and explosion functionality to mediate between

694: programmer-supplied term types and the representation type. While

695: unrestricted access to a representation type corresponds to a less

696: safe way of generic programming due to the potential of implosion

697: problems, \emph{implementations} of (i)--(iii) might very well be

698: based on a representation type. To give an example,

699: in~\cite{LV02-PADL}, traversal combinators are implemented using a

700: representation type without any exposure to the generic

701: programmer. Hence, implosion safety can be certified.

702: 

703: 

704: 

705: \myparagraph{Right-associative, heterogeneous fold}

706: %

707: In this symphony, we basically follow the one-layer

708: traversal-combinator approach, but we generalise it in the following

709: manner. Rather than making a somewhat arbitrary selection of traversal

710: combinators as in previous work~\cite{VBT98,Laemmel02-TGT,LV02-PADL},

711: we identify the fundamental principle underlying all one-layer

712: traversal. To this end, we define a primitive combinator for folding

713: over constructor applications. This kind of folding views the

714: immediate subterms of a term (say, its children) as a heterogeneous

715: list of terms.  Without loss of generality, we favour a

716: \emph{right-associative} fold in the sequel. We call the resulting

717: fold operation \emph{hfoldr} for right-associative, heterogeneous

718: fold. Let us recall how the ordinary \emph{foldr} folds over a

719: homogeneous list. Given the fold ingredients $f$ and $z$ for the

720: non-empty and the empty list form, the application of \emph{foldr} to

721: a list is defined as follows:

722: %

723: \[%

724: \mathit{foldr}\ f\ z\ [x_1,x_2,\ldots,x_n]\ =\ f\ x_1\ (f\ x_2\ (\cdots\ (f\ x_n\ z)\ \cdots))\]

725: %

726: The combinator \emph{hfoldr} folds over a constructor application

727: in nearly the same way:

728: %

729: \[%

730: \mathit{hfoldr}\ f\ z\ (C\ x_n\ \cdots\ x_2\ x_1)\ =\ %

731: f\ x_1\ (f\ x_2\ (\cdots\ (f\ x_n\ (z\ C))\

732: \cdots))\]

733: %

734: Note the order of the children in a constructor application. Due to

735: curried style, we have a kind of snoc-list, that is, the leftmost

736: child is the head of the list, and so on. Also note that the empty

737: constructor application $C$ is passed to $z$ so that the constructor

738: can contribute to the result of folding.

739: 

740: 

741: 

742: \myfigure{%

743: \input{snip/hfoldr.math}

744: }{%

745: Folding over constructor applications

746: }{%

747: F:hfoldr%

748: }{t}

749: 

750: 

751: 

752: \myfigure{%

753: \input{snip/hfoldrprime.math}

754: }{%

755: Per-datatype support for \emph{hfoldr}~---~sample instances%

756: }{%

757: F:hfoldr'%

758: }{t}

759: 

760: 

761: 

762: \myparagraph{Encoding scheme}

763: %

764: A strategic programmer considers \emph{hfoldr} as a primitive.  In

765: Haskell, we cannot define the \emph{hfoldr} combinator once and for

766: all, but it can be supported per datatype~---~as in the case of

767: strategy update. In Fig.~\ref{F:hfoldr}, we complete the \emph{Term}

768: class accordingly. We add a primed helper member $\mathit{hfoldr}'$ to

769: the class, and we define the actual combinator \emph{hfoldr} via

770: wrapping with $G$. Due to the employment of first-class polymorphism,

771: we need to pack the ingredients $f$ and $z$ for \emph{hfoldr} in a

772: datatype \emph{HFoldrAlg}. This is a deviation from the curried style

773: that is used for the rank-1 \emph{foldr} for lists. The datatype

774: constructor $A$ is used for packaging. The types of the two components

775: deserve some explanation. The first component, i.e., the one that

776: corresponds to $f$, is universally quantified in $\alpha$ and $\beta$

777: corresponding to the type of the heading child (i.e., the outermost

778: argument in the constructor application), and the type of the

779: constructor application at hand, respectively. The type of the

780: recursively processed tail is $\cod\ (\alpha \to \beta)$ because it

781: `lacks' a child of type $\alpha$.  Given a constructor application $C\

782: x_n\ \cdots\ x_2\ x_1$, the type variable $\alpha$ would be bound to

783: the respective types of the $x_i$ in the several folding steps while

784: the type $\beta$ variable would be bound to the corresponding

785: remainders of $C$'s type. The second component of $A$, i.e., the one

786: that corresponds to the base case $z$, is simply a parametrically

787: polymorphic function for processing the empty constructor

788: application. The per-datatype definition of \emph{hfoldr} is

789: illustrated in Fig.~\ref{F:hfoldr'} with the sample datatypes from our

790: running example. We basically need one equation for $\mathit{hfoldr}'$

791: of the above form for each specific datatype constructor.

792: 

793: 

794: 

795: \myfigure{%

796: \input{snip/allone.math}%

797: }{%

798: Examples of one-layer traversal combinators%

799: }{%

800: F:allone%

801: }{}

802: 

803: 

804: 

805: \myparagraph{One-layer traversal combinators}

806: %

807: Based on \emph{hfoldr}, one can define all kinds of one-layer traversal

808: combinators. We indicate an open-ended list of candidates by

809: reconstructing combinators that were presented

810: elsewhere~\cite{VBT98,LV00,LV02-PADL,Laemmel02-TGT}:

811: %

812: \begin{description}

813: \item[\emph{allTP}] Process all children; preserve the constructor.

814: \item[\emph{oneTP}] Try to process the children until one succeeds;

815: preserve the constructor.

816: \item[\emph{allTU}] Process all children; reduce the intermediate

817: results.

818: \item[\emph{oneTU}] Try to process the children until one succeeds;

819: return the processed child.

820: \end{description}

821: %

822: One can think of further combinators, e.g., combinators dealing with

823: different orders of processing children, monadic effects, and

824: different constraints regarding success and failure behaviour.

825: 

826: \medskip

827: 

828: \noindent

829: The definition of the combinators is shown in Fig.~\ref{F:allone}.

830: Let us explain the first one, that is, \emph{allTP}. We construct a

831: (type-preserving) fold algebra $A\ f\ z$ and pass it to

832: \emph{hfoldr}. The ingredient $z$ for the empty constructor

833: application simply \emph{return}s, i.e., preserves the constructor.

834: Additional wrapping of $S$ and $I$ is needed to deal with our

835: `datatypes-as-type-constructors' encoding. The ingredient $f$ sequences

836: three computations. Firstly, the tail $t$ is computed. Secondly, the

837: head $h$ (i.e., the child at hand) is processed via $s$. Thirdly, the

838: processed head $h'$ is passed to the computed tail $t'$ (modulo

839: wrapping and unwrapping). The definition of the other combinators is

840: similar. A challenging complication shows up when we want to define

841: \emph{oneTP} because it turns out that this fold over children is

842: paramorphic in nature~\cite{Meertens92} while our combinator

843: \emph{hfoldr} is catamorphic. We use a pairing technique adopted

844: from~\cite{Meertens92} to encode the paramorphic fold with

845: \emph{hfoldr} (cf.\ the new type constructor $D$). This complication

846: also illustrates the potential for further generic function types,

847: namely $\mathit{MG}\ (D\ \mathit{Maybe})\ m$ in this case.

848: 

849: \newpage

850: 

851: \myparagraph{Sums of products vs.\ curried constructor applications}

852: %

853: The combinator \emph{hfoldr} roughly covers the sum and product cases

854: in a polytypic definition~\cite{JJ96} but without resorting to a

855: constructor-free representation type. While a polytypic definition

856: deals with the many children in a term via nested binary products,

857: \emph{hfoldr} processes all children in a curried constructor

858: application as is. While the different constructors of a datatype

859: amount to nested binary sums in a polytypic definition, the base case

860: of \emph{hfoldr} handles the empty constructor application. Also note

861: that polytypic definitions employ a designated declaration form for

862: type induction while functional strategies are defined as ordinary

863: recursive functions. Finally, polytypic definitions are normally

864: implemented by compile-time specialisation. Functional strategies only

865: require a \emph{Term} interface for datatypes to enable \emph{hfoldr}

866: and \emph{adhoc}.

867: 

868: 

869: 

870: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

871: 

872: 

873: 

874: \section{Largo}

875: 

876: We are now in the position to define all kinds of traversal schemes in

877: terms of the strategy combinators and recursion. Before we present a

878: portfolio of such schemes, we impose some extra structure on our

879: combinator suite in order to allow for a uniform treatment of

880: type-preserving and type-unifying traversal.

881: 

882: 

883: 

884: \myparagraph{Overloading \emph{TP} and \emph{TU}}

885: %

886: The strategy combinators are usually typed in a manner that they can

887: be used to derive strategies of both type \emph{TP} and type

888: \emph{TU}. Hence, one would expect that traversal schemes can be

889: composed in a manner to work for both type schemes as well. There are

890: two asymmetries which we need to address. Firstly, there is no obvious

891: way to write fold algebras that cover both \emph{TP} and

892: \emph{TU}. This is the reason why we have a \emph{oneTP} vs.\ a

893: \emph{oneTU}, and an \emph{allTP} vs.\ an \emph{allTU}. These

894: combinators should be overloaded. Secondly, there is no uniform way to

895: \emph{combine} the execution of two strategies of the \emph{same}

896: type. We can only compose \emph{alternative} branches via

897: \emph{choice}. For the sake of sequential composition being generic,

898: the \emph{seq} combinator insists on a type-preserving first

899: argument. For the sake of value passing to deliver an extra input to

900: the second operand, the \emph{pass} combinator insists on a

901: type-unifying first argument. We suggest an overloaded composition

902: combinator \emph{comb} as follows. In the \emph{TP} instance,

903: sequential composition via \emph{seq} is appropriate: the term as

904: returned by the first type-preserving application is passed to the

905: second. In the \emph{TU} instance, both strategies are evaluated via

906: \emph{pass}, and then, the two resulting values are combined via the

907: binary operation of a monoid. Note that the \emph{Monoid} class is

908: also appropriate to harmonise the types of the one-layer traversal

909: combinators \emph{allTP} and \emph{allTU} for overloading. That is,

910: the additional parameters for \emph{allTU} are assumed to correspond

911: to the monoid operations.

912: 

913: \medskip

914: 

915: \noindent

916: In Fig.~\ref{F:overloading}, the overloaded combinators for

917: traversal (cf.\ \emph{one} and \emph{all}) and combination of

918: strategies (cf.\ \emph{comb}) are defined. For completeness, we also

919: overload \emph{idTP} and \emph{constTU} in a way that an always

920: succeeding strategy is defined (cf.\ \emph{skip}). The overloaded

921: combinators are placed in two Haskell type classes

922: \emph{StrategicMonadPlus} and \emph{StrategicMonoid} in order to deal with

923: the different class constraints for the overloaded combinators.

924: 

925: 

926: 

927: \myfigure{

928: \input{snip/overloading.math}%

929: }{%

930: Classes of generic function combinators

931: }{%

932: F:overloading%

933: }{}

934: 

935: 

936: 

937: \myparagraph{Full traversal control}

938: %

939: In Fig.~\ref{F:schemes}, we define traversal schemes in three

940: groups. The highly parameterised function \emph{traverse} captures a

941: rich class of traversal schemes as illustrated by the given

942: instantiations. Some of the type-preserving instantiations of

943: \emph{traverse} were identified in \cite{VBT98}. In

944: \cite{LV00,Laemmel02-TGT,LV02-PADL}, some type-unifying instantiations

945: were added. In the definition of \emph{traverse}, we separate out the

946: distinguishing parameters of such more specific traversal schemes. The

947: argument \emph{op} is the function combinator to compose term

948: processing and recursive descent. The argument $t$ defines how to

949: descend into children. Finally, $f$ is the strategy for term

950: processing. Here is the normative type for this `mother of traversal':

951: 

952: \input{snip/mother.math}

953: 

954: 

955: 

956: \myfigure{

957: \input{snip/schemes.math}

958: }{%

959: Traversal schemes%

960: }{%

961: F:schemes%

962: }{}

963: 

964: 

965: 

966: \noindent

967: We call this a \emph{normative} type because the inferable type is

968: much more general, namely $\mathit{traverse} :: (a \to b \to c) \to (c

969: \to b) \to a \to c$. Not even the normative type captures all our

970: intentions, e.g., the one that $t$ actually specifies descent into

971: children. It is a topic for future work to capture such constraints in

972: suitable types.

973: 

974: \medskip

975: 

976: \noindent

977: The scheme \emph{traverse} is illustrated by several instances in the

978: figure. The first two instances \emph{all\_rec} and \emph{one\_rec}

979: refine \emph{traverse} to opt either for descent with \emph{all} or

980: \emph{one}, respectively.  The postfixes ``...\emph{td}'' or

981: ``...\emph{bu}'' stand for top-down or bottom-up, respectively.  The

982: prefixes ``\emph{full}...'', ``\emph{once}...'', or ``\emph{stop}...''

983: hint on the style of traversal control: full traversal where all nodes

984: are processed vs.\ single hit traversal where the argument strategy

985: has to succeed once vs.\ cut-off traversal where descent stops when a

986: subterm was processed successfully. All the more concrete schemes are

987: still overloaded as for the choice of \emph{TP} vs.\ \emph{TU}. To

988: give an example, the scheme \emph{full\_td} models full traversal of a

989: term where all nodes are processed in top-down manner. In this

990: example, the argument $t$ for descent is instantiated with \emph{all}

991: (via \emph{all\_rec}). The argument \emph{op} for the composition of

992: term processing and recursive descent is instantiated with

993: \emph{comb}.

994: 

995: 

996: 

997: \myparagraph{Traversal with propagation}

998: %

999: The second group in Fig.~\ref{F:schemes} illustrates a class of

1000: traversal schemes that go beyond simple node-wise processing. In

1001: addition to traversal, \emph{p}ropagation of an \emph{e}nvironment

1002: (abbreviated by the postfix ``...\emph{pe}'') is performed.  The

1003: scheme \emph{propagate} takes the same arguments \emph{op}, $t$, and

1004: $f$ as \emph{traverse}.  In addition, the scheme carries a generic

1005: function argument $u$ to update the environment before descent into

1006: the children, and an argument $e$ for the initial environment. Here is

1007: the normative type for \emph{propagate}:

1008: 

1009: \newpage

1010: 

1011: \input{snip/pe.math}

1012: 

1013: \noindent

1014: The shown instances of \emph{propagate} favour top-down traversal

1015: because bottom-up traversal seems to be less obvious when combined

1016: with propagation. In is interesting to notice that the scheme

1017: \emph{propagate} provides an alternative to using the environment

1018: monad~\cite{Wadler92} in a strategic program.

1019: 

1020: 

1021: 

1022: \myparagraph{Path schemes}

1023: %

1024: The last group in Fig.~\ref{F:schemes} deals with traversal

1025: constrained by the path leading to or starting from a node (say, a

1026: subterm). For this reason, we do not just use a processor strategy

1027: $f$, but we also use predicates $p$ for constraints. The scheme

1028: \emph{beloweq} attempts to process a subterm via $f$ (not necessarily

1029: strictly) below a node for which $p$ succeeds; dually for

1030: \emph{aboveeq}. The \emph{below} and \emph{above} variants enforce the

1031: root of the processed subterm not to coincide with the constrained

1032: node. In the definition of the path schemes, we use the simpler

1033: traversal schemes \emph{once\_td} and \emph{once\_bu} from above. The

1034: types of the path schemes are as follows:

1035: 

1036: \input{snip/path.math}

1037: 

1038: 

1039: 

1040: \noindent

1041: These types illustrate that predicates are encoded as type-unifying

1042: functions of type $\mathit{TU}\ ()\ m$ where $m$ is normally the

1043: \emph{Maybe} monad or another instance of the \emph{MonadPlus}

1044: class. So success and failure behaviour encodes the truth value.

1045: 

1046: \medskip

1047: 

1048: \noindent

1049: The final three schemes in the group elaborate the more basic path

1050: schemes to deal with \emph{lists} of predicates. The schemes

1051: \emph{belowlist} and \emph{abovelist} constrain the prefix or postfix

1052: of a node rooting a subtree of interest, respectively. The last scheme

1053: \emph{prepost} combines \emph{belowlist} and \emph{abovelist}. Note

1054: that the path scheme \emph{belowlist} resolves the remaining blind

1055: spot in the sample code for our running example in

1056: Fig.~\ref{F:running}.

1057: 

1058: 

1059: 

1060: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1061: 

1062: \medskip

1063: 

1064: \hfill{\textsf{[End Of Symphony]}}

1065: 

1066: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1067: 

1068: \newpage

1069: 

1070: \mysection{Appraisal}

1071: 

1072: \medskip

1073: 

1074: \noindent

1075: The four movements of this symphony combine certain bits of parametric

1076: polymorphism, type case (i.e., intensional polymorphism), polytypism,

1077: and overloading to provide a concise and expressive model for

1078: functional strategies~\cite{LV02-PADL}. The development culminates in

1079: the last movement when typed highly parameterised traversal schemes

1080: are defined. This paper makes the following overall contributions when

1081: compared to previous work on strategic programming. Firstly, the

1082: developed model is more concise and expressive than in our previous

1083: work~\cite{LV00,Laemmel02-TGT,LV02-PADL}. Secondly, the defined

1084: traversal schemes reach new limits of parameterisation. We shall

1085: elaborate on these two claims accordingly.

1086: 

1087: 

1088: \medskip

1089: 

1090: \noindent

1091: The overall model ``functional strategies = first-class polymorphic

1092: functions'' was already sketched in~\cite{LV02-PADL}. In addition to

1093: working out this model, we improved it in two important ways. Firstly,

1094: the type schemes for type-preserving and type-unifying strategies are

1095: viewed as instances of one common type scheme \emph{Strategic}.  This

1096: allows us to define combinators like \emph{choice} and \emph{adhoc}

1097: without commitment to any specific type scheme. Secondly, we

1098: eliminated the need for an open-ended list of primitive one-layer

1099: traversal combinators. To this end, we designed a generic fold

1100: combinator for processing the immediate subterms of constructor

1101: applications.  A related language construct is described

1102: in~\cite{DV01}: pattern matching is generalised in a way that generic

1103: access is granted to subterms of constructor applications. A limited

1104: form of folds over constructor applications was first proposed in

1105: \cite{Laemmel02-TGT} in a term-rewriting setting, but there it was by

1106: far less potent and it was difficult to type due to the limitations of

1107: the underlying type system.

1108: 

1109: \medskip

1110: 

1111: 

1112: \noindent

1113: The key idea to define traversal schemes in terms of one-layer

1114: traversal combinators carries over from the seminal work on term

1115: rewriting strategies~\cite{VBT98}. The present paper reaches a new

1116: level of genericity for the following two reasons. Firstly, we

1117: effectively overload the two prime type schemes of generic

1118: traversal. This allows us to capture meaningful traversal schemes

1119: without anticipating their use for transformation vs.\ analysis.

1120: Secondly, we identify a few highly parameterised traversal schemes

1121: with parameters for various forms of control. These `skeleton' or

1122: `meta' schemes capture more concrete traversal schemes favoured in

1123: previous work.

1124: 

1125: 

1126: 

1127: \myparagraph{Acknowledgement}

1128: %

1129: The following people contributed beats to this polymorphic symphony:

1130: Jan Kort, Andres L{\"o}h, Simon Peyton-Jones, Joost Visser, and

1131: Stephanie Weirich. I am grateful for the remarks and suggestions by

1132: the anonymous WRS'02 referees. I devote my first symphony to Berenike

1133: and Bernadette.

1134: 

1135: 

1136: 

1137: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1138: 

1139: 

1140: 

1141: \bibliographystyle{abbrv}

1142: \bibliography{paper}

1143: 

1144: 

1145: 

1146: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1147: 

1148: 

1149: 

1150: \end{document}

1151: