Extensible ADT (EADT)

EADTs are “extensible algebraic data types”: they can be transformed (by adding or removing constructors) and their constructors are not tied to a specific EADT type, hence we can use them as constructors of different EADTs.

EADT constructors and operations can be defined independently (even in different modules) allowing a great modularity. As such there are an answer to the “expression problem” (cf Background section).

• 1. Introduction
• 2. Basics
• 3. Explicit recursive traversal
• 4. Constraining constructors with :<:
• 5. Recursion schemes
• 6. Safe pattern matching
• 7. Constructor removal/transformation
• 8. Background
• 9. Examples