I am fairly used to debates among mathematicians, constructivists, intuitionists etc. over principles like the law of excluded middle or the axiom of choice. However I am somewhat at a loss when it comes to some of the axioms that arise in type theory, like function extensionality.
I understand that when we assume an axiom we are fabricating an element of a type which cannot actually be constructed. So in the case of function extensionality, one is asserting that there's an inhabitant of the equality type.
This leads to something like
Definition p : f = g := (proof involving function extensionality)
Definition t : nat := match p with
| refl f => 0
end
where the match statement will not simplify to zero because p is not constructed with refl. Therefore we have some blocked computation. This destroys canonicity because now we have a term of natural number type which is not a numeral. Ok.
However I don't really understand the practical repercussions of this. As a mathematician interested in formalizing mathematics can someone give me a reason why I might be concerned about this? What justification might someone have for trying to avoid this?
I guess in the case above, the term t
is propositionally equal to zero even if not judgementally equal.
Short answer: For mathematicians proving things, it mostly doesn't matter. For people wanting to compute things, it can get in the way. (The first group overlaps with the second).
It is possible to come up with a model of type theory where function extensionality doesn't hold, but I don't know if that is of much interest to somebody formalizing mathematics unrelated to logic.
Reminds me of a related question: contrary to some axioms like excluded middle, it's easy to provide a computation rule for FunExt which just returns refl, making it possible to compute with it. I think having such a computation rule in the empty context should be safe, but has anyone worked out the implications of having such a reduction rule in other (potentially inconsistent) contexts?
what does "safe" mean? refl does not have type (fun x : bool => x) = (fun x : bool => if x then true else false)
so it would break subject reduction
Ali Caglayan said:
Short answer: For mathematicians proving things, it mostly doesn't matter. For people wanting to compute things, it can get in the way. (The first group overlaps with the second).
Ok, this is helpful. This problem is intangible to me. Can you think of any good examples of computations we would want to carry out which would be hindered by assuming function extensionality? I am not sure whether the kinds of computations I'm interested in would be hindered by assuming this axiom. If I only use it for proving correctness results about algorithms rather than defining the algorithms themselves it should be fine.
I would guess that's basically it. If you only use it "at the end", for proving equalities, but not for defining programs, then you should be mostly fine.
agree with Théo — the exception is ver e.g. if you use Definition some_function. ... rewrite foo. ... Defined.
, and foo
is an equality proof that does not reduce to eq_refl
(or is not even propositionally equal to it) because it is stuck on functional extensionality. However, such definitions are questionable even without axioms, because they'll often be stuck on Qed
(https://gmalecha.github.io/reflections/2017/qed-considered-harmful has examples of the problems, but I would NOT recommend those solutions).
(also OTOH, equalities on types with decidable equalities can be okay, since those equalities are provably proof irrelevant anyway)
@Paolo Giarrusso Hm, ok so just to be sure I understand you correctly, if f, g
are not themselves judgementally equivalent then we can never have that some p : f =g
is even propositionally equivalent to refl
, right? Because f =f
and f=g
are different types.
Or do you mean up to transport along p
or something?
I am not sure if your point about decidable equality is meant to be directly related to the functional extensionality question.
I probably spoke too quickly; the decidable equality point is about equalities which are "easier" to mix with data (the example I use most often is { x : T | bool_pred T = true }
)
and it remains true that if you don't mix proofs and computations, you won't get stuck on funext in computation
(at least IIANM)
Last updated: Oct 13 2024 at 01:02 UTC