Zulip Chat Archive

Stream: Type theory

Topic: Resources on type inference for dependent types


ohhaimark (Jul 08 2022 at 22:50):

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 (Jul 20 2022 at 12:08):

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

Notification Bot (Jul 20 2022 at 12:09):

ohhaimark has marked this topic as unresolved.

David Thrane Christiansen (Aug 14 2022 at 19:24):

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.


Last updated: Dec 20 2023 at 11:08 UTC