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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelBidrag til bog/antologiForskningpeer review

Abstrakt

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.
OriginalsprogUdefineret/Ukendt
TitelProceedings of the 10th ACM SIGPLAN Workshop on Generic Programming
Antal sider12
UdgivelsesstedNew York, NY, USA
ForlagACM
Publikationsdato1 aug. 2014
Sider71-82
ISBN (Trykt)978-1-4503-3042-8
DOI
StatusUdgivet - 1 aug. 2014

Emneord

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

Citationsformater