abstract:
Records in Haskell are notoriously difficult to compose; many solutions have been proposed. Vinyl lies in the space of library-level approaches, and addresses polymorphism, extensibility, effects and strictness. I describe how Vinyl approaches record families over arbitrary key spaces using a Tarski universe construction, as well as a method for immersing each field of a record in a chosen effect modality. Moreover, I give a characterization of records as sheaves of types, which provides a clear motivation for the safety of subtyping and coercion of records, and a path toward records with non-trivial topologies on their key spaces. Lastly, I describe an interpretation of Vinyl-style records into Type Theory as finite products over containers, leading to many possible and interesting extensions, such as compositional universes of polymorphic variants, as well as inductive and coinductive types.
bio:
I’m an amateur type theorist who studied Historical Linguistics during my undergraduate at UC Berkeley, specializing in Ancient Greek, Sumerian, Akkadian and Anglo-Saxon. I’m particularly interested in type-theoretic syntax and semantics for natural language, and am presently exploring the use of multi-modal combinatory categorial grammar for interpreting the hyperbaton-rich syntax of ancient Indo-European languages. In addition to my interest in linguistics, I have become obsessed with extensionality, realizability and PER semantics for Martin-Löf Type Theory, and am currently trying to come up with an extension to Observational Type Theory which internalizes further extensional concepts, such as union, intersection, image and PER types whilst retaining decidability of type checking.