Dualizing Generalized Algebraic Data Types by Matrix Transposition
by Klaus Ostermann and Julian Jabs
In Proc. Europ. Symposium on Programming (ESOP). Lecture Notes in Computer Science, 2018.
This publication is related to the Uroboro research project.
Abstract
We characterize the relation between generalized algebraic datatypes (GADTs) with pattern matching on their constructors one hand, and generalized algebraic co-datatypes (GAcoDTs) with copattern matching on their destructors on the other hand: GADTs can be converted mechanically to GAcoDTs by refunctionalization, GAcoDTs can be converted mechanically to GADTs by defunctionalization, and both defunctionalization and refunctionalization correspond to a transposition of the matrix in which the equations for each constructor/destructor pair of the (co-)datatype are organized. We have defined a calculus, GADT^T, which unifies GADTs and GAcoDTs in such a way that GADTs and GAcoDTs are merely different ways to partition the program.
We have formalized the type system and operational semantics of GADT^T in the Coq proof assistant and have mechanically verified the following results: (1) The type system of GADTT is sound, (2) defunctionalization and refunctionalization can translate GADTs to GAcoDTs and back, (3) both transformations are type- and semantics-preserving and are inverses of each other, (4) (co-)datatypes can be represented by matrices in such a way the aforementioned transformations correspond to matrix transposition, (5) GADTs are extensible in an exactly dual way to GAcoDTs; we thereby clarify folklore knowledge about the “expression problem”. We believe that the identification of this relationship can guide future language design of “dual features” for data and codata.