Is there any difference between extensible records and dependent maps

Question

In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the resulting type and a dependent map in a dependently typed language?

Answer 1

Simple records correspond to maps of dependent type (and we don't have a merge operation yet). More precisely, the record type

{ lbl1 : A1, lbl2 : A2, ..., lblN : AN }

corresponds to the product type

∏ (ℓ : label), A ℓ

where label is the sum type

lbl1 + lbl2 + ... + lblN

and A : label → Type is the type family defined by

A lbl1 ≡ A1
A lbl2 ≡ A2
       ⋮
A lblN ≡ AN

The record type above is also equivalent to the simple product

A1 × A2 × ⋯ × AN.

You asked about extensible records. There are at least two ways to do this. Without any additional technology we can model an extension of

{ foo : A, bar : B } ≤ { foo : A, bar : B, baz C }

with a couple of function that map between them (projection in one direction and extension by an extra field in the other). This is all very mundane.

We could also ask for the type of all possible record types. Suppose we have a type label of all possible labels (in practice it could be string or some such). The type of all record types is

record ≡ label → option Type

An element R : record is a mapping from labels to optional types, where R lbl takes value None if label lbl does not appear in R and value Some A if it appears and have type A.

If R : record then the type decribed by R is the product type

∏ (ℓ : label),
  match R ℓ with
  | Some A ⇒ A
  | None ⇒ unit
  end

This means that a record r of type R is a dependent function which takes a label ℓ to an element of A if ℓ appears in R and to the unit otherwise.

However, a merge operation is problematic, as well as a subtyping relation R ≤ Q. This is so because we cannot express the fact that a label lbl has the same type in record R and record Q. At best you can say that the types are isomorphic, or propositionally equal, but that's not what you want.

We can define an extend operation

extend : record → record → record

in which the first argument overrides the second one so that extend R Q has the fields of R additionally those fields of Q that do not appear in R:

extend R Q ≡
   λ (ℓ : label),
     match Q ℓ with
     | Some A ⇒ Some A
     | None ⇒ Q ℓ
     end