¿Qué significa el término “?T@{x:=t}”, o un tipo con un signo de interrogación y un símbolo @ que lo rodean, en Coq?
Estoy tratando de escribir una función que elimine los ceros de una lista. Aquí está el primer intento de mi implementación.
Require Import Nat.
Require Import List.
Fixpoint shrink (x : list nat) : list nat := (* ¡Error! Necesita un : list nat *)
match x with
| nil => nil
| h :: t => if h =? 0 then shrink t else (h :: shrink t)
end.
Sin embargo, obtengo este error:
Error:
En el entorno
shrink : forall (x : Datatypes.list Datatypes.nat)
(list0 : ?T) (nat : ?T0@{list:=list0}),
Datatypes.list ?T1@{x:=x; list:=list0; x1:=x}
x : list nat
list : ?T
nat : ?T0
h : Datatypes.nat
t : Datatypes.list Datatypes.nat
El término "shrink t" tiene tipo
"forall (list0 : ?T@{x:=t}) (nat : ?T0@{x:=t; list:=list0}),
Datatypes.list ?T1@{x:=t; list:=list0; x1:=t}"
mientras se espera que tenga tipo "Datatypes.list ?T1@{x1:=h :: t}".
La implementación correcta de la función es la siguiente:
Fixpoint shrink (x : list nat) : list nat :=
match x with
| nil => nil
| h :: t => if h =? 0 then shrink t else (h :: shrink t)
end.
Pero, ¿cómo se supone que interprete el error, en particular (list0 : ?T@{x:=t})? En particular,
- ¿Por qué es
list0en lugar delist? - ¿Qué significa
?antes delT? - ¿Qué significa
@{ ... }después delT?
davy.ai
El mensaje de error muestra
list0en lugar delistporquelistya es un nombre definido en la biblioteca estándar de Coq. En la primera implementación,listse incluyó accidentalmente en los argumentos en lugar de ser una variable de tipo para la salida.El
?antes deTsignifica queTes un argumento implícito, lo que significa que se puede inferir en función de los otros argumentos proporcionados.El
@{ ... }después deTcontiene información adicional para el sistema de inferencia de tipos. En este caso, especifica el contexto en el que se debe inferir el tipo. Por ejemplo,@{list:=list0}especifica quelistdebe referirse al valor delist0en este contexto.