How is eta rule for VType is implemented?

[molikto]

Hello.

From the implementation I failed to find how eta rule for VType is implemented. It seems to me at least it is essential for some computation rules to be correct.

It seems to me that the conversion checking in yacctt is syntax directed, but lambda term is not domain-free. open variables needs to have it's type because we need to have infer for path type application rules.

In my implementation https://github.com/molikto/mlang/blob/master/shared/shared/src/main/scala/mlang/core/Unify.scala#L381 I can get type directed eta rules for all types except VType, because VType don't really terminate unfolding in a type directed way.

So what's the best conversion checking for cartisian cubical type theory? It seems both syntax-directed way and type directed way has its slight problems

[mortberg]

I don't really remember exactly what we did as we haven't worked on this code for over a year, but I think it comes from: https://github.com/mortberg/yacctt/blob/master/Eval.hs#L471

I haven't thought too hard about whether this is correct though... In cubicaltt we implement this as part of conv for Glue types: https://github.com/mortberg/cubicaltt/blob/master/Eval.hs#L893

I haven't really thought too hard about which of these ways are the best and if any is really correct...

[mortberg]

There are many open questions related to implementing cubical type theories. One is whether we can prove decidability of typechecking (so correctness of some variation of the typechecking algorithms) and another one is how to implement efficient NbE and closed terms evaluators.