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?


1 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?

  • $\begingroup$ I decided to look into the bog and found a few subtyping papers for records. Including this one: researchgate.net/publication/… $\endgroup$
    – Cheery
    Commented Feb 28, 2022 at 15:04
  • $\begingroup$ I spoke too soon, that paper is not helping me much. $\endgroup$
    – Cheery
    Commented Feb 28, 2022 at 19:27
  • $\begingroup$ What are you doing? What's the larger problem you're solving? $\endgroup$ Commented Feb 28, 2022 at 19:32
  • $\begingroup$ I addded a fourth possibility. $\endgroup$ Commented Feb 28, 2022 at 19:34
  • 3
    $\begingroup$ @Cheery that source is significantly improved upon by: dl.acm.org/doi/10.1145/3408983 Which in turn, IMO, is practically obsoleted by github.com/AndrasKovacs/elaboration-zoo/tree/master/… $\endgroup$ Commented Feb 28, 2022 at 23:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.