2
$\begingroup$

It is claimed in many sources (for example, here) that adding a rule like "if Id(X,Y) then X really equals Y" to a type theory is "problematic" because then its type-checking becomes undecidable. I have read Martin Hoffman's proof ("Extensional concepts in intensional type theory", Section 3.2.2), as well as this SE question, but I still don't see how this creates a problem for a "down-to-earth" programming language.

I understand that deciding whether x:A has type B can get difficult, because there might exist a proof of Id(A,B). But the purpose of any "normal" type-checker is to verify, not to decide, so how is it problematic?

As I see it, nothing prevents the compiler from functioning like this: whenever the user tries to use a value of type X where a Y belongs, if the user has previously provided a proof that Id(X,Y), then we allow it, as if X and Y were syntactically identical. But if such a proof hasn't been provided, we treat it as an error, because the user "hasn't made his case".

My question is: what difficulties, if any, can arise from treating identity types like that?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

You can't expect to find a ready-to-use proof of Id(a,b) when you need one. For instance, you have proofs of Id(a,c) and Id(c,b), but not of Id(a,b). You would need some intelligence to find automatically new proofs of equality, and avoid always having to ask the user to do the job manually. But there is no perfect algorithm to implement such an intelligence: whatever you implement, it will always have limitations.

There are however solutions to this difficulty, see for instance the Andromeda project.

Improve this answer
$\endgroup$
6
  • $\begingroup$ How difficult could it be to do it manually? I'm envisioning it like this: the user writes a special statement equate e1;, where e1 : Id(a,c), and then all the cs in the current scope magically turn into as, including the one in the definition of e2 : Id(c,b). So now the user can write equate e2; to accomplish what he wanted. $\endgroup$
    – Сергей Макеев
    Oct 22, 2020 at 11:36
  • $\begingroup$ The goal of the type checker is to check a proof. If you have to help the type checker manually, then the proof is uncomplete: if you give it to a colleague, or another type checker, he may not be able to check it again (not all equality proof are so trivial; e.g. you may have to use induction to prove an equality). A proof that is uncomplete is not really a proof: the checking process should be fully repeatable. You need a way to record all the checking steps, they are all part of the proof. $\endgroup$
    – L. Garde
    Oct 22, 2020 at 19:45
  • $\begingroup$ An angle to consider is: what is the advantage of the undecidable theory? The use of a rigorous formal type theory is to be reliably verifiable, but it does not need to be used directly. Ad hoc, convenient elaborations/solvers can translate from a surface syntax into a core theory with better metatheoretic properties. Sometimes even programming languages work this way. Attempting to formalize the 'convenient' theory directly may be advantageous when working by hand, but for a computer implementation, it seems to lose much of its value, while retaining disadvantages. $\endgroup$
    – Dan Doel
    Oct 23, 2020 at 17:16
  • $\begingroup$ @L.Garde Are you saying that a transition from Id(a,c) and Id(c,b) into Id(a,b) is not part of the proof? I think that it is, and so has to be written out somehow, whether manually or as part of some standard library. It's not "helping the type checker", it's a logical step like any other. $\endgroup$
    – Сергей Макеев
    Oct 23, 2020 at 21:15
  • $\begingroup$ @СергейМакеев I was meaning that each time the type checker has to ask for help, it is because it is missing a part of the proof. The goal of a type-checker is to verify a succession of logicial steps against the rules of a well-defined theory. Searching a theorem in some standard library is another job, for another module of your proof assistant. So the type checking compiler that you are describing is not really a type-checker, it is a proof assistant that includes a decidable type-checker able to check the equality proofs extracted from some standard library or entered manually. $\endgroup$
    – L. Garde
    Oct 24, 2020 at 17:05

Your Answer

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

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