Dans ce cas, l'unification est effectivement possible et unique, mais notre algorithme ne la trouve pas. Je ne considère pas ça comme un bug. Si tu remplaces `unit/Unit` par `true/Bool` le problème devient impossible, vu qu'il y a plein de fonctions différentes qui renvoient `Bool` lorsqu'on leur passe la valeur `true`.
D’après ce que j’ai compris, le type de `sigma` est
sigma : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (fst : A) -> (snd : B fst) -> Sigma A B;
Puisque le type de `up` a été donné explicitement, c’est à dire up : Sigma Unit (lambda _ -> Unit);
Je dirais que normalement ça devrait possible de faire l’unification entre `B` et `(lambda _ -> Unit)`?
Ici les parametres `A` et `B` passé à `sigma` devraient être redondants/inférables (grâce à l'annotation explicite du type de `isContrΠ`).
Le `A` est effectivement redondant, mais malheureusement le `B` ne l’est pas, pour la même raison que le `B` était nécessaire dans l’autre exemple avec `lambda _ -> Unit`.
James
Le 21 juill. 2023 à 17:36, Stefan Monnier monnier@iro.umontreal.ca a écrit :
On définit d’abord le type `Sigma`
Sigma = typecons (Sigma (l1 ::: TypeLevel) (l2 ::: TypeLevel) (A : Type_ l1) (B : A -> Type_ l2)) (sigma (fst : A) (snd : B fst)); sigma = datacons Sigma sigma;
Mais quand il s’agit de construire une expression de ce type, on se retrouve dans l’obligation de fournir la valeur de `B` explicitement lors de la construction même si l’information se trouve déjà dans l’annotation de type.
Ah, ça ne me surprend pas: ça nécessite de l'unification d'ordre supérieur, qui est souvent/toujours une source de problème.
up : Sigma Unit (lambda _ -> Unit);; up = sigma (B := lambda _ -> Unit) unit unit; %% ça ne marche plus si on enlève l’argument B
Si on enlève le B, on obtient l’erreur "Context expected: (?B↑0 unit) but expression has type: Unit”.
Dans ce cas, l'unification est effectivement possible et unique, mais notre algorithme ne la trouve pas. Je ne considère pas ça comme un bug. Si tu remplaces `unit/Unit` par `true/Bool` le problème devient impossible, vu qu'il y a plein de fonctions différentes qui renvoient `Bool` lorsqu'on leur passe la valeur `true`.
J’ai rencontré un autre problème avec les indices de Debruijn quand j’écrivais cette preuve
HoTT_isContr A = Sigma A (lambda (x : A) -> ((y : A) -> Eq x y));
isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x); isContrΠ h = sigma (A := (x : A) -> B x) (B := (lambda (x : ((x : A) -> B x)) -> ((y : ((x : A) -> B x)) -> Eq x y))) (lambda x -> case (h x) | sigma bx p => bx) (lambda f -> Eq_eq (f := lambda i ≡> lambda x -> case (h x) | sigma bx p => Eq_uneq (p := p (f x)) (i := i)));
Ici les parametres `A` et `B` passé à `sigma` devraient être redondants/inférables (grâce à l'annotation explicite du type de `isContrΠ`).
qui donnait l’erreur
[X] Fatal :(DEBRUIJN) DeBruijn index 2 refers to wrong name. Expected: " %gensym% no 42 “ got " %gensym% no 39 “
Hmm... sur des variables "gensym'd" :-( Ça donne bien peu d'indices. Je vais devoir y passer plus de temps pour Merci pour ces exemples.
Stefan