> Je vous écrit à propos de ce commentaire que vous m’avez envoyé:
>
> ```
> %% SM: Hmm... doesn't this break type-preservation since `a` has type `A i₀`
> %% whereas `transp A i₀ a` has type `A i₁`?
> ```
>
> Ma justification est que puisque A (_ := i0) et A (_ := i1) sont
> équivalents car l’argument `i` est effaçable, la règle n’est pas
> trop déraisonnable.
>
> J’imagine qu’on peut reproduire la même ‘situation' en utilisant
> l’égalité précédente de Typer. On peut par exemple construire une
> preuve d’égalité entre A (_ := i0) et A (_ := i1) en utilisant
> Eq_refl, on peut ensuite faire un cast sur un terme `a : A (_ := i0)`
> qui va tout simplement renvoyer le `a` tel quel.
La *normalisation* de `cast ... a` n'est en général pas `a`.
Une telle normalisation casserai notre système.
Il l'est seulement lorsque la preuve est égale à `Eq_refl`.
Et cela malgré que l'argument est effaçable. 🙁
Par exemple:
λ (P : Eq Int String) -> String_concat (cast P 3) "Oops"
ne doit pas se réduire à
λ (P : Eq Int String) -> String_concat 3 "Oops"
vu que ce n'est pas well-typed!
C'est discuté par exemple dans:
@Article{Werner08,
author = Werner,
title = {On the Strength of Proof-Irrelevant Type Theories},
journal = LMCS,
year = 2008,
volume = 4,
number = 3,
pages = {1-20},
doi = {10.1007/11814771_49},
url = {https://arxiv.org/abs/0808.3928},
abstract = {We present a type theory with some proof-irrelevance built
into the conversion rule. We argue that this feature is
particularly useful when type theory is used as the
logical formalism underlying a theorem prover. We also
show a close relation with the subset types of the theory
of PVS. Finally we show that in these theories, because of
the additional extentionality, the axiom of choice implies
the decidability of equality, that is, almost classical
logic. Finally we describe a simple
set-theoretic semantics.}
}
Lors de l'*évaluation*, oui, `cast ... a` devient `a` sans avoir besoin
de regarder la preuve, parce que lors de l'évaluation le contexte est
vide, donc la preuve ne peut être que `Eq_refl` de toute façon.
Stefan
