Bonjour à tous,
J'ai récemment travaillé à ajouter l'élimination dépendante à Typer
(4c632a1f, 8a7b7910), qui repose sur des égalités dans les expressions
`case`. Pour les utiliser, on élimine éventuellement ces égalités avec
`Eq.cast` (c'est ce que fait la macro `case_return_`, d'ailleurs). On
dirait que dans certains cas de son utilisation (au niveau des types),
il serait utile que les appels à `Eq.cast` puissent être réduits dans
le calcul des WHNF, ce qui n'est pas le cas en ce moment.
Je me pose quelques questions quant à l'implantation de la WHNF de
`Eq.cast`, sur lesquelles j'apprécierais vos commentaires. Aussi, pour
rendre la discussion plus concrète, j'ai construit un petit exemple où
l'unification échoue quand la réduction bloque sur un appel à `Eq.cast`.
Pour obtenir le code de l'exemple à partir de ce courriel, exécutez :
$ sed -n 's/^\s*> \?\(.*\)/\1/p' <email.txt >exemple.typer
1. Question
Je me demande comment implanter la WHNF de `Eq.cast`, j'ai
l'impression, intuitivement, qu'il suffit de vérifier que son
argument `p` est bel et bien convertible à `Eq.refl` (autrement
dit, ce n'est pas simplement une variable/hypothèse), auquel cas,
il me paraît correct d'ignorer l'argument `f` et de se réduire à
l'argument explicite.
Évidemment, si `p` n'est pas convertible à `Eq.refl`, la réduction
doit bloquer.
Est-ce que cette approche peut causer des problèmes au niveau
théorique?
2. Exemple
Utilisons, au niveau des types, `decideBoolEq`, une fonction que
l'on définit avec l'élimination dépendante, pour illustrer le
problème.
Petite parenthèse, je vais utiliser le `case` builtin pour
simplifier les affichages:
> case_ = ##case_;
Prenons le type `Decidable` défini de cette façon:
>
> Decidable =
> typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ))
> (yes (p :: prop)) (no (p :: Not prop));
> yes = datacons Decidable yes;
> no = datacons Decidable no;
>
Définissons `decideBoolEq`, qui prouve la décidabilité de l'égalité
de booléens. On se sert des lemmes `true≠false` et `false≠true`
qu'on définit au passage.
>
> true≠false (p : Eq true false) =
> Eq_cast (p := p)
> (f := lambda tf -> case tf
> | true => True
> | false => False)
> (); % This is unit, an inhabitant of `True = Unit`.
>
> false≠true (p : Eq false true) = true≠false (Eq_comm p);
>
> decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b);
> decideBoolEq =
> lambda (a : Bool) (b : Bool) =>
> case a return (Decidable (Eq a b))
> | true =>
> (case b return (Decidable (Eq true b))
> | true => yes (p := Eq_refl)
> | false => no (p := true≠false))
> | false =>
> (case b return (Decidable (Eq false b))
> | true => no (p := false≠true)
> | false => yes (p := Eq_refl));
>
Note: Ici, on utilise la macro `case_return_`, qui insère les bons
appels à `Eq.cast`.
Définissons maintenant une méthode d'accès pour obtenir la preuve
d'un `Decidable`, qu'il soit vrai ou faux:
>
> getProof :
> (l : TypeLevel) ≡>
> (prop : Type_ l) ≡>
> (d : Decidable prop) ->
> case d | yes => prop | no => Not prop;
> getProof d =
> case d return (case d | yes => prop | no => Not prop)
> | yes (p := p) => p
> | no (p := p) => p;
>
Ces définitions nous permettent de définir un terme qui fait
échouer l'élaboration:
>
> this_fails =
> (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true);
>
Voici l'erreur qu'on obtient:
% ./samples/exemple.typer:48:9:Error:(ELAB) Type mismatch (residue)! Context expected:
% (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210])
% but expression has type:
% case (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true) | no _ => (Not[53] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])) | yes _ => (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])
% can't unify:
% (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210])
% with:
% case (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true) | no _ => (Not[53] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])) | yes _ => (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])
% > Call: (getProof[0] ##TypeLevel.z (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210]) (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true))
%
Pourquoi? On doit unifier le type de
getProof (decideBoolEq : Decidable (Eq true true))
qui est
case (decideBoolEq (a := true) (b := true))
| yes => Eq true true
| no => Not (Eq true true)
avec `Eq true true`. Pour que cette unification fonctionne, il faut
que `decideBoolEq (a := true) (b := true)` se réduise à un
constructeur de `Decidable`, en l'occurence `yes`. Or, quand on
regarde la première branche de `decideBoolEq`, on se rend compte
qu'à cause de l'élimination dépendante, on obtient plutôt un appel
à `Eq.cast`. Effectivement, en déboggant, j'obtiens le terme:
% (##Eq.cast
% ##TypeLevel.z
% ##TypeLevel.z
% typecons (Bool) (false) (true)
% true[210]
% datacons Bool[211] true
% (##Eq.refl
% ##TypeLevel.z
% Bool[211]
% datacons Bool[211] true)
% lambda (a : typecons (Bool) (false) (true)) ->
% (Decidable[7]
% ##TypeLevel.z
% (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) a[0] datacons Bool[212] true))
% case datacons Bool[211] true
% | false => (##Eq.cast ##TypeLevel.z ##TypeLevel.z typecons (Bool) (false) (true) false[210] datacons Bool[212] true <anon>[0] lambda (b : typecons (Bool) (false) (true)) -> (Decidable[8] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] b[0])) (no[5] ##TypeLevel.z (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) true[211] false[210]) true≠false[4]))
% | true => (##Eq.cast
% ##TypeLevel.z
% ##TypeLevel.z
% typecons (Bool) (false) (true)
% true[211]
% datacons Bool[212] true
% <anon>[0]
% lambda (b : typecons (Bool) (false) (true)) ->
% (Decidable[8] ##TypeLevel.z
% (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] b[0]))
% (yes[6]
% ##TypeLevel.z
% (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) datacons Bool[212] true datacons Bool[212] true)
% (Eq_refl[216] ##TypeLevel.z typecons (Bool) (false) (true) datacons Bool[212] true))))
On constate que le `yes` que l'on cherche se trouve sous deux
niveaux de `Eq.cast` à cause des deux niveaux de `case_return_`
dans `decideBoolEq`. Ces deux appels à `Eq.cast` devraient pouvoir
être réduits!
Jean-Alexandre
