Abstract

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, and some literature on formalizing mathematical structure.

In this talk I develop 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 will not explain the subtyping system in detail, but only show some examples.)

I will discuss the two standard approaches to sharing substructures: "Pebble style" and "manifest types" (ML style). By example I argue --Morethat we really do need "manifest types" to formalize mathematics, and extend the dependently typed records to include "manifest types"

Much of my proposed approach can be represented by inductive definitions in Coq or Lego, so features such as "manifest types" can easily be experimented with.