Type Fusion

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.

• Type: Journal
• Year: 2010
• Where: AMAST
• Authors: Ralf Hinze
• Keywords: AMAST 2010, Indispensable Tool, Initial Algebra, Software Engineering, Type Fusion