Generic record combinators with static type checking

Common record systems only provide access to individual record fields. However, it is often useful to have generic record combinators, that is, functions that work with complete records of varying structure. Traditionally, generic record combinators can only be implemented in dynamically typed languages. In this paper, we present a record system for Haskell that allows us to define generic record combinators without giving up static type checks. The system is implemented as a library so that it works without modifications to the language. We achieve this mainly by using advanced type system features such as type equality constraints, type families, and higher-rank polymorphism. A key contribution of our paper is a technique for emulating subkinds, including subkind polymorphism. We use this to give the record system additional expressiveness. Our system is not only useful in itself. It also shows what features should be taken into account when designing language support for records...

• Type: Journal
• Year: 2010
• Where: PPDP
• Authors: Wolfgang Jeltsch
• Keywords: Common Record Systems, Generic Record Combinators, PPDP 2010, Programming Languages, Static Type Checks