How to elaborate with dependent records present?

Question

Dependent records can be implemented in various ways, but some papers suggests I could do it in the following way:

• The construction of dependent record type is made by selecting labels and types.
• The construction of dependent record is made by filling up the fields.
• The destruction is made by selecting a label.

Eg. We could therefore do something like: sig : {fst: A, snd: B fst} to represent sigma. Then construct it with sig = {fst=a, snd=b}, and retrieve the second field with sig.snd.

But now I hit elaboration phase where the input program is turned into bunch of constraints. This means I do not necessarily have information about the record type before I resolve record fields. With the naive elaborator I have no information about types during elaboration.

Specifically for inference. Given some (a:_) with type yet undetermined and then label a.snd. Which type should I give when I cannot know the specific record? What can I do in this situation?

Answer 1

You can:

1. Complain that not enough typing information has been given, the same way that you would complain if the input is just a bare λ x → x. Bidirectional type checking is good at doing that.

2. Require that all record types be defined in advance. For a simple life, you disallow reuse of field names so that upon seeing a field name you know which type it belongs to. For a more interesting life you disambiguate field names when possible.

3. You walk into the bogs of record subtyping. This is a radical move that has to be carefully combined with the rest of your type theory.

4. You might be able to use row polymorphism, although that seems to work only for non-dependent record types. Or am I mistaken?