Composing and Decomposing Data Types: A Closed Type Families Implementation of Data Types à La Carte

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review


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.
Original languageUndefined/Unknown
Title of host publicationProceedings of the 10th ACM SIGPLAN Workshop on Generic Programming
Number of pages12
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication date1 Aug 2014
ISBN (Print)978-1-4503-3042-8
Publication statusPublished - 1 Aug 2014

Cite this