peta - ¿Qué es Haskell falta para la verificación de la totalidad?

if en haskell

Question

Un lenguaje total (funcional) es aquel en el que se puede demostrar que todo termina. Obviamente, hay muchos lugares en los que no quiero esto: lanzar excepciones a veces es útil, se supone que un servidor web no debe terminar, etc. Pero a veces, me gustaría una verificación de totalidad local para habilitar ciertas optimizaciones. Por ejemplo, si tengo una función probadamente total

commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...

entonces, dado que :~: tiene exactamente un habitante ( Refl ) , GHC podría optimizar

gcastWith (commutativity @n @m) someExpression
==>
someExpression

Y mi prueba de conmutatividad va de tener un costo de tiempo de ejecución O(n) a ser libre. Entonces, ahora para mi pregunta:

¿Cuáles son algunas de las dificultades sutiles para hacer un verificador de totalidad para Haskell?

Obviamente, este tipo de comprobador es conservador, por lo tanto, cuando GHC no esté seguro de que algo sea total (o de que sea flojo comprobarlo) podría suponer que no es ... Me parece que no sería demasiado difícil juntar un no- comprobador tan inteligente que aún sería muy útil (al menos debería ser sencillo eliminar todas mis pruebas aritméticas). Sin embargo, parece que no puedo encontrar ningún esfuerzo para construir tal cosa en GHC, así que obviamente me faltan algunas limitaciones bastante grandes. Adelante, aplasta mis sueños. :)

Relevante pero no reciente: Unfailing Haskell por Neil Mitchell, 2005 .

Answer 1

Liquid Haskell tiene comprobación de totalidad: https://github.com/ucsd-progsys/liquidhaskell#termination-check

Por defecto, se realiza una verificación de terminación en todas las funciones recursivas.

Use la opción de no terminación para desactivar el cheque

liquid --no-termination test.hs

En las funciones recursivas, el primer argumento algebraico o entero debería estar disminuyendo.

La medida decreciente predeterminada para las listas es la longitud y los enteros su valor.

(Incluí una captura de pantalla y una cita para la posteridad).

Al igual que en Agda u otros lenguajes con comprobación de totalidad, los argumentos para la función deben volverse estructuralmente más pequeños a lo largo del tiempo para llegar al caso base. Combinado con un comprobador de totalidad, esto permite una verificación confiable de una serie de funciones. LH también ayuda a ayudar al corrector indicando cómo disminuyen las cosas, lo que podría hacer con un tipo de datos abstractos que es opaco o de un FFI. Es realmente bastante práctico.