Folds for Abstract Data Types

Project Description

Generalized fold operations were originally introduced for data types as found in Haskell or ML (which correspond to free term algebras). The scope of folds can be extended to abstract data types if an ADT is represented by a pair consisting of a constructor and a destructor, which are essentially functions to/from a common representation. Then a fold can work on an ADT by applying parameter functions to values that are delivered by the ADT's destructor. Fold operations that use as a parameter the constructor of another ADT, called ADT transformers,play an important role and offer a concise programming style. Several laws for ADT folds and transformers exist that can be used for program optimization and verification.

Selected Publications

Comprehending ADTs, Martin Erwig
Draft paper, 1999, 2011 (revised version)

Random Access to Abstract Data Types, Martin Erwig
8th Int. Conf. on Algebraic Methodology and Software Technology, LNCS 1816, 135-149, 2000

Categorical Programming with Abstract Data Types, Martin Erwig
7th Int. Conf. on Algebraic Methodology and Software Technology, LNCS 1548, 406-421, 1998

The Categorical Imperative - Or: How to Hide Your State Monads, Martin Erwig
10th Int. Workshop on Implementation of Functional Languages, 1-25, 1998

Software

Participating Researchers

Support