2 edited tags
| link
    Tweeted twitter.com/StackCompSci/status/743519172618035204
source | link

Is there any difference between extensible records and dependent maps

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?