Type-Directed Partial Evaluation

Olivier Danvy

December 1998

Abstract:

Type-directed partial evaluation uses a normalization function to achieve partial evaluation. These lecture notes review its background, foundations, practice, and applications. Of specific interest is the modular technique of offline and online type-directed partial evaluation in Standard ML of New Jersey

Contents

1

Background and introduction

1.1

Partial evaluation by normalization

1.2

Prerequisites and notation

1.3

Two-level programming in ML

1.4

Binding-time coercions

1.5

Summary and conclusion

2

Normalization by evaluation

2.1

A normalization function

2.2

Application to decompilation

2.3

Normalization by evaluation

2.4

Naive normalization by evaluation in ML

2.5

Towards type-directed partial evaluation

2.6

Normalization by evaluation in ML

2.7

Summary and conclusion

3

Offline type-directed partial evaluation

3.1

The power function, part 1

3.2

The power function, part 2

3.3

Summary and conclusion

4

Online type-directed partial evaluation

4.1

Online simplification for integers

4.2

The power function, revisited

4.3

Summary and conclusion

5

Incremental type-directed partial evaluation

6

Conclusion and issues