Type Fusion
Ralf Hinze
Abstract
Fusion is an indispensable tool in the arsenal of techniques for program derivation. Less well-known, but equally valuable is type fusion, which states conditions for fusing an application of a functor with an initial algebra to form another initial algebra. We provide a novel proof of type fusion based on adjoint folds and discuss several applications: type firstification, type specialisation and tabulation.
Affiliation
University of Oxford‚ Computing Laboratory‚ Wolfson Building‚ Parks Road‚ Oxford OX1 3QD‚ England
Book Title
Thirteenth International Conference on Algebraic Methodology And Software Technology (AMAST 2010)
Editor
Pavlovic‚ Dusko and Johnson‚ Michael
Location
Manoir St−Castin‚ Québec‚ Canada
Pages
92−110
Publisher
Springer−Verlag
Series
Lecture Notes in Computer Science
Volume
6486
Year
2011