Composing and decomposing data types: a closed type families implementation of data types à la carte

TY - GEN

T1 - Composing and decomposing data types

T2 - ACM SIGPLAN Workshop on Generic Programming

AU - Bahr, Patrick

N1 - Conference code: 10

PY - 2014

Y1 - 2014

N2 - Wouter Swierstra's data types à la carte is a technique to modularise data type definitions in Haskell. We give an alternative implementation of data types à la carte that offers more flexibility in composing and decomposing data types. To achieve this, we refine the subtyping constraint, which is at the centre of data types à la carte. On the one hand this refinement is more general, allowing subtypings that intuitively should hold but were not derivable beforehand. This aspect of our implementation removes previous restrictions on how data types can be combined. On the other hand our refinement is more restrictive, disallowing subtypings that lead to more than one possible injection and should therefore be considered programming errors. Furthermore, from this refined subtyping constraint we derive a new constraint to express type isomorphism. We show how this isomorphism constraint allows us to decompose data types and to define extensible functions on data types in an ad hoc manner. The implementation makes essential use of closed type families in Haskell. The use of closed type families instead of type classes comes with a set of trade-offs, which we review in detail. Finally, we show that our technique can be used for other similar problem domains.

AB - Wouter Swierstra's data types à la carte is a technique to modularise data type definitions in Haskell. We give an alternative implementation of data types à la carte that offers more flexibility in composing and decomposing data types. To achieve this, we refine the subtyping constraint, which is at the centre of data types à la carte. On the one hand this refinement is more general, allowing subtypings that intuitively should hold but were not derivable beforehand. This aspect of our implementation removes previous restrictions on how data types can be combined. On the other hand our refinement is more restrictive, disallowing subtypings that lead to more than one possible injection and should therefore be considered programming errors. Furthermore, from this refined subtyping constraint we derive a new constraint to express type isomorphism. We show how this isomorphism constraint allows us to decompose data types and to define extensible functions on data types in an ad hoc manner. The implementation makes essential use of closed type families in Haskell. The use of closed type families instead of type classes comes with a set of trade-offs, which we review in detail. Finally, we show that our technique can be used for other similar problem domains.

KW - closed type families, expression problem, modularity, two-level types

U2 - 10.1145/2633628.2633635

DO - 10.1145/2633628.2633635

M3 - Article in proceedings

SN - 978-1-4503-3042-8

SP - 71

EP - 82

BT - Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming

PB - Association for Computing Machinery

Y2 - 31 August 2014

ER -