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

Patrick Bahr

10 Citations (Scopus)

Abstract

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 languageEnglish
Title of host publicationProceedings of the 10th ACM SIGPLAN Workshop on Generic Programming
Number of pages12
PublisherAssociation for Computing Machinery
Publication date2014
Pages71-82
ISBN (Print)978-1-4503-3042-8
DOIs
Publication statusPublished - 2014
EventACM SIGPLAN Workshop on Generic Programming - Gothenburg, Sweden
Duration: 31 Aug 2014 → …
Conference number: 10

Conference

ConferenceACM SIGPLAN Workshop on Generic Programming
Number10
Country/TerritorySweden
CityGothenburg
Period31/08/2014 → …

Cite this