Dependently Types Records
               for Representing Mathematical Structure

                            Randy Pollack

                    preliminary paper available at
            <www.dcs.ed.ac.uk/home/rap/export/records.ps>

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.

This paper 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, and
extend 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.  Since submitting the paper I found that
records with dependent and manifest signatures and first-class labels,
can be programmed in type theory using Dybjer's "inductive-recursive"
definition.  This gives some confidence about the meta-theory of such
records, and clarifies some points in my paper.