**Problem Detail:**

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?

###### Asked By : Alex R

#### Answered By : Andrej Bauer

*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 `

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/59738

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback