Tech Talk: Vinyl: Records in Haskell & Type Theory

  • Date Friday, August 01, 2014  Time
  • Speaker Jon Sterling
  • Location Galois, Inc., 421 SW 6th Ave., Suite 300, Portland, OR, USA (3rd floor of the Commonwealth Building)
  • Galois is pleased to host the following tech talk. These talks are free and open to the interested public--please join us! (There is no need to pre-register for the talk.)

    The talk starts at 11am.

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.

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.