I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by:
- the well-typedness of the clauses (type check)
- the coverage of the patterns (coverage check)
- the fact that recursive calls are structurally recursive (termination check)
- the overlapping clauses are confluent (
IApplyConfluence) -- see https://amelia.how/quick/boundaries-in-cubical-agda.html
My question: in what order does it make the best sense? Obviously type check should come first, but what about the others?
IApplyConfluencerequires reduction of function bodies (for the conversion checks), we may potentially need to reduce the function being type-checked. If there is a non-termination problem, then we are in trouble (the type checker may loop). However, it makes me worried because how am I about to reduce a function that we do not yet know if it's well-defined?
- Termination check is, in my impression, the last phase of the type checking, because there are techniques developed to do some clever reduction to make more definitions type-checked. It seems that we should definitely termination-check those who have no problem on reduction. However, if the clauses are not even confluent, we may reduce the wrong thing!
- In case of mutually recursive functions, it's worse: the termination check of the two functions happens after both of their type checking, which means
- if termination comes last, then both of their confluence check will happen when the other is neither known to be structurally recursive nor confluent.
- if confluence comes last, then both of their termination check will happen when the other is neither known to be structurally recursive nor confluent.
f (suc (suc x)) = g xfor a function
gwhile it's quite difficult to do with fix. But this is an interesting perspective $\endgroup$