Generalized algebraic data types (GADTs) are at the cutting edge of functional programming, and become more widely used every day. Nevertheless, the foundations of GADTs are not well understood. This research aims to show that GADTs support the same kind of initial algebra semantics as other advanced data types, and to use this semantics to derive collections of expressive and principled tools --- called initial algebra packages --- for understanding GADT structures, structuring programs which manipulate those structures, reasoning about properties of those programs, and automatically improving the performance of modularly constructed such programs. The research employs a three-part approach to deriving initial algebra semantics and packages for GADTs. First, an equivalent nested type is derived for each GADT.
Secondly, initial algebra semantics and packages for these nested types are derived. Finally, the initial algebra semantics and packages for the nested types are used to derive initial algebra semantics and packages for their corresponding GADTs. By providing reasoning, programming, and optimization tools for GADTs, this research has the potential to offer programmers a wider range of options for effectively handling data than is currently available, and thus to improve programming by enabling programs to better structure and manipulate data.
