Resources on type inference for dependent types

Stream: Type theory

[ohhaimark]

I would like to understand how dependent type inference works, but am struggling to get a foothold. Is there a central resource or text book that covers this territory?

[ohhaimark]

In NbE, why is eta-expansion done rather than eta-reduction when doing a read-back?

[Notification Bot]

ohhaimark has marked this topic as unresolved.

[David Thrane Christiansen]

In NbE, why is eta-expansion done rather than eta-reduction when doing a read-back?

Eta-long normal forms are easy to implement - when readback sees a type with an eta rule, it can immediately spit out the corresponding introduction form and recur down to each sub-expression. For instance, if the type is Unit, just emit Unit.unit, and if the type is A -> B, just emit a fun (x : A) => and read back the value applied to x at type B. This works for everything with a nice eta rule but Empty, for which some special hacks are needed (but if you're reading back normal forms for conversion checking, then you'll have a slow implementation anyway - the right answer is to convert the values incrementally based on their types, only computing what's needed, and then you can just directly equate all values of type Empty with no further computation).

Univesral eta contraction is more difficult. For functions, it's reasonably easy to implement, but not efficiently (it requires a full traversal of the body to find variable occurrences). For non-Unit products, it would require conversion checks on all the fields, which is inelegant as a rule and also probably very slow. For Unit, it's hard to even know what it would mean.