Row Polymorphic Programming

Summary

Sometimes, especially when dealing with business logic, we have to deal with data that comes in from the real world, or elsewhere, naturally very messily typed, leading to nasty type signatures and messes of macros or code generation to build data structures from a schema. Row polymorphism can help us by abstracting over the fields contained in a record type in the type signature, letting us define records based on data, concatenate records together, and define functions that are generic across any record containing the required fields, all without macros. This article is inspired by my work on implementing the Brown Benchmark for Table Types for my Structures library, an update for which will be released soon, providing a much more comprehensive collection of types for row-polymorphic programming. At time of writing, the Wikipedia page for row polymorphism starts with: In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are polymorphic on row types such as record types and polymorphic variants. leading into some text dense with mathematical notation that doesn't do much in explaining what any of this looks like, and what the hell does "polymorphic on row types" even mean? Consider a basic record in Idris as an example: record ImACat where constructor MkCat name : String age : Nat meows_a_lot : Bool This certainly seems like it might fit the bill, it says record right there, and the wikipedia snippet did mention records. But what are these "row types"? "Row Type" and "Record Type" are sometimes used interchangeably in this corner of type theory. While "record" may be a somewhat more intuitive name for someone approaching this from the perspective of many popular programming languages, we will mostly be using the name "Row Type", as it will make more sense in the tabular data context that will serve as framing for this article. Imagine some tabular data, say a table in a database or a spread sheet. Ta...