Bonjour,
Decidable est définit comme suit
Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));
Ce qui est élaboré en
Decidable' = lambda (ℓ : TypeLevel) ≡> typecons (Decidable (prop : Type_ ?ℓ)) …
C'est problématique parce que Typer n'élabore pas les lambda dans les datacons. Le code suivant est rejeté parce que Decidable n'est pas un type.
yes = datacons Decidable true;
Je propose le changement [0], qui instancie les arguments implicites dans les datacons, mais plus j'y pense, plus je me rends compte que ce n'est pas la bonne solution à ce problème. (Je pense quand même que ce changement est correct, mais pour d'autres circonstances.) Decidable ne devrait-il pas être définit comme
Decidable'' = typecons (Decidable (ℓ ::: TypeLevel) (t : Type_ ℓ)) …
Mes deux questions sont: - Quelle est la différence sémantique entre les deux formulations? - Si la première est incorrecte, est-ce que l'élaboration des typecons devrait être changé pour que l'élaboration du code le plus naturel donne "la bonne chose".
Bon typage Simon
[0]: https://gitlab.com/monnier/typer/-/commit/da12222203e536730456fefc0eaa2f2464...
Afficher les réponses par date
Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));
Ce qui est élaboré en
Decidable' = lambda (ℓ : TypeLevel) ≡> typecons (Decidable (prop : Type_ ?ℓ)) …
C'est problématique parce que Typer n'élabore pas les lambda dans les datacons. Le code suivant est rejeté parce que Decidable n'est pas un type.
Oui, en fait il y a deux options:
- à l'heure actuelle, Typer ne gère correctement que la définition
Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop)); yes = datacons Decidable true; no = datacons Decidable false;
- dans le futur (aussi proche que possible, mais je n'ai pas eu beaucoup de temps à y consacrer), Typer n'acceptera probablement que la définition
Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) = typecons (true (p ::: prop)) (false (p ::: Not prop)); yes (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) true; no (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) false;
- Quelle est la différence sémantique entre les deux formulations?
Aucune, à ma connaissance.
Stefan
- dans le futur (aussi proche que possible, mais je n'ai pas eu beaucoup de temps à y consacrer), Typer n'acceptera probablement que la définition
Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) = typecons (true (p ::: prop)) (false (p ::: Not prop)); yes (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) true; no (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) false;
Le changement [0] rend possible cette définition, je peux modifier typecons pour ne plus accepter d'arguments. On pourrait par contre garder un symbole pour le nom du type pour imprimer dans les messages d'erreur?
[0]: https://gitlab.com/monnier/typer/-/commit/da12222203e536730456fefc0eaa2f2464...
- dans le futur (aussi proche que possible, mais je n'ai pas eu beaucoup de temps à y consacrer), Typer n'acceptera probablement que la définition
Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) = typecons (true (p ::: prop)) (false (p ::: Not prop)); yes (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) true; no (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) false;
Le changement [0] rend possible cette définition, je peux modifier typecons pour ne plus accepter d'arguments.
Très bien.
On pourrait par contre garder un symbole pour le nom du type pour imprimer dans les messages d'erreur?
Oui, pour l'instant on va le garder, en attendant d'avoir un meilleur méchanisme pour préserver le nom donné "à l'extérieur".
Stefan
-
Génier Simon -
Stefan Monnier