Dependently Typed Records for Representing Mathematical Structure

It is folklore that dependently typed tuples suffice to formalize abstract mathematical structures such as semi-group, monoid, group, ring, field,... We want natural properties of informal mathematical language to be preserved; e.g. inheritance of properties and sharing of substructures. There is a big literature on the related topic of programming language modules.

This talk develops a notion of dependently typed records by adding field labels to Sigma types. Some obscure features from the literature are simplified and explained. E.g. field variables (local) vs field labels (global) are explained by ordinary lambda-binding. Subtyping is orthogonal to records, and is introduced using Luo's coercive subtyping. (Hence I do not explain the subtyping system in detail, but only show some examples.)

I discuss the two standard approaches to sharing substructures: "Pebble style" and "manifest types" (ML style). By example, I argue that we really do need manifest types to formalize mathematics. I extend dependently typed records to include manifest types and the "with" notation for adding manifest information to an existing signature.

I program records with first-class labels, dependent, manifest signatures and "with" directly in type theory (checked in both Coq and Lego), using inductive definition. All of the rules (projection, subtyping, "value rules", definition of "with") are derivable from the inductive definition, which has only three constructors and three corresponding computation rules.

Preliminary paper