Modular Reifiable Matching A List-of-Functors Approach to Two-Level Types

This paper presents Modular Reifiable Matching (MRM): a new approach to two level types using a fixpoint of list-of-functors rep-resentation. MRM allows the modular definition of datatypes and functions by pattern matching, using a style similar to the widely popular Datatypes a ̀ la Carte (DTC) approach. However, unlike DTC, MRM uses a fixpoint of list-of-functors approach to two-level types. This approach has advantages that help with various aspects of extensibility, modularity and reuse. Firstly, modular pat-tern matching definitions are collected using a list of matches that is fully reifiable. This allows for extensible pattern matching def-initions to be easily reused/inherited, and particular matches to be overridden. Such flexibility is used, among other things, to imple-ment extensible generic traversals. Secondly, the subtyping relation between lists of functors is quite simple, does not require back-tracking, and is easy to model in languages like Haskell. MRM is implemented as a Haskell library, and its use and applicability are illustrated through various examples in the paper