coq - ejercicios - ¿Por qué los lenguajes más nuevos que se escribieron de manera dependiente no adoptaron el enfoque de SSReflect?

indices html (2)

Hay dos convenciones que he encontrado en la extensión SSReflect de Coq que parecen ser particularmente útiles pero que no he visto ampliamente adoptadas en los nuevos lenguajes de tipo dependiente (Lean, Agda, Idris).

En primer lugar, cuando los predicados posibles se expresan como funciones de retorno booleano en lugar de tipos de datos definidos por inducción. Esto brinda decidibilidad por defecto, abre más oportunidades para pruebas por cómputo y mejora el rendimiento de verificación al evitar la necesidad de que el motor de pruebas lleve consigo términos de prueba grandes. La principal desventaja que veo es la necesidad de utilizar lemas de reflexión para manipular estos predicados booleanos al probar.

En segundo lugar, los tipos de datos con invariantes se definen como registros dependientes que contienen un tipo de datos simple más una prueba del invariante. Por ejemplo, las secuencias de longitud fija se definen en SSReflect como:

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

Una secuencia y una prueba de que la longitud de esa secuencia es un valor determinado. Esto se opone a cómo, por ejemplo, Idris define este tipo:

data Vect : (len : Nat) -> (elem : Type) -> Type

Una estructura de datos de tipo dependiente en la que el invariante es parte de su tipo. Una de las ventajas del enfoque de SSReflect es que permite su reutilización, de modo que, por ejemplo, muchas de las funciones definidas para seq y las pruebas sobre ellas aún pueden usarse con la tuple (al operar en el seq subyacente), mientras que con el enfoque de Idris funciona como reverse . append y similares deben ser reescritos para Vect . Lean en realidad tiene un estilo SSReflect equivalente en su biblioteca estándar, vector , pero también tiene una array estilo Idris que parece tener una implementación optimizada en el tiempo de ejecución.

Un libro orientado a SSReflect incluso afirma que el enfoque de estilo Vect n A es un antipatrón:

Un anti-patrón común en lenguajes de tipo dependiente y Coq en particular es codificar tales propiedades algebraicas en las definiciones de los tipos de datos y las funciones en sí (un ejemplo canónico de este enfoque son las listas indexadas por longitud). Si bien este enfoque parece atractivo, ya que demuestra el poder de los tipos dependientes para capturar ciertas propiedades de tipos de datos y funciones en ellos, es inherentemente no escalable, ya que siempre habrá otra propiedad de interés, que no ha sido prevista por un diseñador. del tipo de datos / función, por lo que tendrá que codificarse como un hecho externo de todos modos. Es por eso que abogamos por el enfoque, en el que los tipos de datos y las funciones se definen de la forma en que lo definiría un programador, y todas las propiedades necesarias de los mismos se prueban por separado.

Mi pregunta es por lo tanto, ¿por qué no se han adoptado más estos enfoques? ¿Hay desventajas que me faltan, o quizás sus ventajas son menos significativas en los idiomas con mejor soporte para la coincidencia de patrones dependientes que Coq?

Esto brinda decidibilidad por defecto, abre más oportunidades para pruebas por cómputo y mejora el rendimiento de verificación al evitar la necesidad de que el motor de pruebas lleve consigo términos de prueba grandes.

No tiene que llevar términos grandes como se describe en la tesis de Edwin Brady bajo el nombre de "forzar la optimización". Agda tiene un forzado que afecta la verificación de tipos (especialmente cómo se computan los universos es relevante), pero no estoy seguro si las cosas usadas solo en el tiempo de verificación de tipos realmente se borran antes del tiempo de ejecución. De todos modos, Agda tiene dos nociones de irrelevancia:. .(eq : p ≡ q) es la irrelevancia habitual (lo que significa que eq es irrelevante en el momento de la verificación de tipo, por lo que es igual que cualquier otro término de ese tipo) y ..(x : A) es irrelevante para la columna vertebral (no estoy seguro si es un término correcto. Creo que las fuentes de Agda llaman a tal cosa "irrelevancia no estricta") que es literalmente para la eliminación de términos computacionalmente irrelevantes, pero no completamente irrelevantes. Para que puedas definir

data Vec {α} (A : Set α) : ..(n : ℕ) -> Set α where [] : Vec A 0 _∷_ : ∀ ..{n} -> A -> Vec A n -> Vec A (suc n)

y n se borrará antes del tiempo de ejecución. O al menos parece estar diseñado así, es difícil estar seguro, porque Agda tiene muchas características mal documentadas.

Y puede escribir esas pruebas de costo cero en Coq, solo porque también implementa la irrelevancia para las cosas que viven en la Prop . Pero la irrelevancia está incorporada en la teoría de Coq muy profundamente, mientras que en Agda es una característica separada, por lo que es perfectamente comprensible, por qué la gente encuentra el uso de la irrelevancia en Coq más fácilmente que en Agda.

Una de las ventajas del enfoque de SSReflect es que permite su reutilización, de modo que, por ejemplo, muchas de las funciones definidas para seq y las pruebas sobre ellas aún pueden usarse con la tuple (al operar en el seq subyacente), mientras que con el enfoque de Idris funciona como inverso. anexar y similares deben ser reescritos para Vect .

No es una reutilización real si tiene que probar las propiedades de todos modos y esas pruebas tienen la misma complejidad que las funciones definidas sobre los datos indexados. También es un inconveniente hacer el trabajo de una maquinaria de unificación y pasar pruebas explícitas y aplicar lemas para obtener la length xs ≡ n de suc (length xs) ≡ n (y también sym , trans , subst y todos los demás lemas que una maquinaria de unificación puede salvarte de en muchos casos). Además, pierdes algo de claridad al abusar de la igualdad proposicional: tener xs : List A; length xs ≡ n + m xs : List A; length xs ≡ n + m lugar de xs : Vec A (n + m) no mejora la legibilidad de sus contextos, especialmente si son enormes, lo que suele ser el caso. Y hay otro problema: a veces es más difícil definir una función utilizando el enfoque de SSReflect: usted mencionó el reverse para Vect , lo desafío a definir esta función desde cero (con el reverse para la List como una parte "reutilizada" debajo del capó) y luego compare su solución con la definición en Data.Vec de la biblioteca estándar de Agda. Y si no tiene la irrelevancia habilitada para las proposiciones de forma predeterminada (como es el caso de Agda), también deberá probar las propiedades de las pruebas si quiere probar, por ejemplo, reverse (reverse xs) ≡ xs que es Un montón de repetitivo no trivial.

Así que el enfoque de SSReflect no es perfecto. El otro es también. ¿Hay algo que mejore en ambos? Sí, Ornamentos (ver Álgebras ornamentales, Ornamentos algebraicos y La esencia de los ornamentos ). Puede obtener fácilmente Vec de List mediante la aplicación del álgebra ornamental correspondiente, pero no puedo decir cuánta reutilización de código obtendrá de ella y si los tipos lo volverán loco o no. Oí que la gente en realidad usa adornos en alguna parte.

Entonces, no es que tengamos una solución ideal de SSReflect y otros se nieguen a adoptarla. Solo hay una esperanza para una forma más adecuada de reutilizar el código real.

ACTUALIZAR

En su comentario, Anton Trunov me hizo darme cuenta de que soy demasiado agde-minded y que la gente en Coq tiene tácticas que pueden simplificar mucho las pruebas, por lo que demostrar en Coq es generalmente más fácil (siempre que tenga armas como crush del libro de CPDT ) que Definiendo funciones sobre datos. Bueno, entonces supongo que la irrelevancia de la prueba por defecto y la maquinaria de tácticas pesadas es lo que hace que el enfoque de SSReflect sea efectivo en Coq.

Puedo dar algunas ideas sobre el primer punto (definir predicados como funciones de retorno booleano). Mi mayor problema con este enfoque es: entonces, por definición, es imposible que la función tenga errores, incluso si resulta que lo que está calculando no es lo que usted pretendía calcular. En muchos casos, también ocultaría lo que realmente quiere decir con el predicado si tiene que incluir los detalles de implementación del procedimiento de decisión para el predicado en su definición.

En aplicaciones matemáticas, también habrá problemas si desea definir un predicado que sea una especialización de algo que no es decidible en general, incluso si resulta ser decidible en su caso específico. Un ejemplo de lo que estoy hablando aquí sería definir el grupo con una presentación dada: en Coq, una forma común de definir esto sería el setoide con el conjunto subyacente como expresiones formales en los generadores, y la igualdad dada por "word equivalencia". En general, esta relación no es decidible, aunque en muchos casos específicos lo es. Sin embargo, si está restringido a definir grupos con presentaciones en las que el problema de la palabra es decidible, entonces pierde la capacidad de definir el concepto unificador que une todos los diferentes ejemplos, y demuestra cosas genéricamente sobre presentaciones finitas o sobre grupos presentados de manera definitiva. Por otro lado, definir la relación de equivalencia de la palabra como una Prop abstracta o equivalente es sencillo (si es un poco largo).

Personalmente, prefiero dar primero la definición más transparente posible del predicado, y luego proporcionar procedimientos de decisión cuando sea posible (las funciones que devuelven valores de tipo {P} + {~P} son mis preferencias aquí, aunque las funciones de retorno booleano funcionarán bien también). El mecanismo de clase de Coq podría proporcionar una manera conveniente de registrar tales procedimientos de decisión; por ejemplo:

Class Decision (P : Prop) : Set := decide : {P} + {~P}. Arguments decide P [Decision]. Instance True_dec : Decision True := left _ I. Instance and_dec (P Q : Prop) `{Decision P} `{Decision Q} : Decision (P // Q) := ... (* Recap standard library definition of Forall *) Inductive Forall {A : Type} (P : A->Prop) : list A -> Prop := | Forall_nil : Forall P nil | Forall_cons : forall h t, P h -> Forall P t -> Forall P (cons h t). (* Or, if you prefer: Fixpoint Forall {A : Type} (P : A->Prop) (l : list A) : Prop := match l with | nil => True | cons h t => P h // Forall P t end. *) Program Fixpoint Forall_dec {A : Type} (P : A->Prop) `{forall x:A, Decision (P x)} (l : list A) : Decision (Forall P l) := match l with | nil => left _ _ | cons h t => if decide (P h) then if Forall_dec P t then left _ _ else right _ _ else right _ _ end. (* resolve obligations here *) Existing Instance Forall_dec.