¿Qué no puede hacer Idris al renunciar a la integridad de Turing?

Sé que Idris tiene tipos dependientes pero no está completo. ¿Qué no puede hacer al renunciar a la integridad de Turing, y esto está relacionado con tener tipos dependientes?

Supongo que esta es una pregunta bastante específica, pero no sé mucho sobre los tipos dependientes y los sistemas de tipos relacionados.

Idris está Turing completo! Verifica la totalidad (terminación cuando se programa con datos, productividad cuando se programa con codatos) pero no requiere que todo sea total.

Curiosamente, tener datos y codatos es suficiente para modelar la integridad de Turing, ya que puede escribir una mónada para funciones parciales. Hice esto, hace años, en Coq, probablemente ya está bitrotado, pero aquí está, sin embargo: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

Necesitas un escape para ejecutar tales cosas, pero Idris te permite hacer eso.

Idris no reducirá las funciones parciales a nivel de tipo, para mantener la verificación de tipo decidible. Además, solo los programas totales se pueden creer razonablemente como pruebas.

Primero, supongo que ya has oído hablar del tesis de Church-Turing , que establece que cualquier cosa que llamamos "cálculo" es algo que se puede hacer con una máquina de Turing (o cualquiera de los muchos otros modelos equivalentes). Por lo tanto, un lenguaje completo de Turing es aquel en el que se puede expresar cualquier cálculo. Por el contrario, un lenguaje incompleto de Turing es aquel en el que hay algún cálculo que no se puede expresar.

Ok, eso no fue muy informativo. Déjame dar un ejemplo. Hay una cosa que no puede hacer en ningún lenguaje incompleto de Turing: no puede escribir un simulador de máquina de Turing (de lo contrario, podría codificar cualquier cálculo en la máquina de Turing simulada).

Ok, eso todavía no fue muy informativo. la verdadera pregunta es qué programa útil no se puede escribir en un lenguaje incompleto de Turing? Bueno, a nadie se le ocurrió una definición de "programa útil" que incluye todos los programas que alguien ha escrito en algún lugar con un propósito útil, y que no incluye todos los cálculos de la máquina Turing. Por lo tanto, diseñar un lenguaje incompleto de Turing en el que pueda escribir todos los programas útiles sigue siendo un objetivo de investigación a muy largo plazo.

Ahora hay varios tipos muy diferentes de lenguajes incompletos de Turing, y difieren en lo que no pueden hacer. Sin embargo, hay un tema común: los lenguajes completos de Turing deben incluir alguna forma de terminar condicionalmente o continuar durante un tiempo que no esté limitado por el tamaño del programa, y ​​una forma para que el programa use una cantidad de memoria que depende de la entrada . Concretamente, la mayoría de los lenguajes de programación imperativos brindan estas capacidades mediante bucles while y asignación de memoria dinámica, respectivamente. La mayoría de los lenguajes de programación funcionales proporcionan estas capacidades a través de la recursión y el anidamiento de la estructura de datos.

Idris está fuertemente inspirado por Agda . Agda es un lenguaje diseñado para probar teoremas . Ahora los teoremas de prueba y los programas en ejecución están muy relacionados , por lo que puede escribir programas en Agda tal como demuestra un teorema. Intuitivamente, una prueba del teorema "A implica B" es una función que toma una prueba del teorema A como argumento y devuelve una prueba del teorema B.

Dado que el objetivo del sistema es probar teoremas, no puede dejar que el programador escriba funciones arbitrarias. Imagina que el lenguaje te permite escribir una función recursiva tonta que se llama a sí misma:

oops : A -> B
oops x = oops x

¡No puedes dejar que la existencia de tal función te convenza de que A implica B, o de lo contrario serías capaz de probar cualquier cosa y no solo verdaderos teoremas! Entonces Agda (y los probadores de teoremas similares) prohíben la recurrencia arbitraria. Cuando escribe una función recursiva, debe demostrar que siempre termina , de modo que cada vez que la ejecuta en una prueba del teorema A sabe que construirá una prueba del teorema B.

La limitación práctica inmediata de Agda es que no puede escribir funciones recursivas arbitrarias. Dado que el sistema debe ser capaz de rechazar todas las funciones que no son de terminación, la indecidibilidad del problema de detención (o, más generalmente, el teorema de Rice ) garantiza que también haya funciones de terminación que se rechacen. Una dificultad práctica adicional es que debe ayudar al sistema a demostrar que su función termina.

Hay mucha investigación en curso sobre cómo hacer que los sistemas de prueba sean más parecidos al lenguaje de programación sin comprometer su garantía de que si tiene una función de A a B, es tan bueno como una prueba matemática que A implica B. Extender el sistema para aceptar más Terminar funciones es uno de los temas de investigación. Otras instrucciones de extensión incluyen hacer frente a preocupaciones del "mundo real" como entrada / salida y concurrencia. Otro desafío es hacer que estos sistemas sean accesibles a los simples mortales (o quizás convencer a los simples mortales de que en realidad son accesibles).

No estoy familiarizado con Idris. Es una toma de los desafíos que acabo de mencionar. Por lo que entiendo por una mirada superficial al preprint de 2013 , Idris está completo de Turing, pero incluye un verificador de totalidad. El verificador de totalidad verifica que cada función anotada con la palabra clave totaltermina. El fragmento de lenguaje que solo contiene programas Idris donde cada función es total es similar en poder expresivo a Arda (probablemente no sea una coincidencia exacta debido a las diferencias en la teoría de tipos, pero lo suficientemente cerca como para que no lo note a menos que lo intente deliberadamente).

Para ver otros ejemplos de idiomas que no son completos en Turing de diferentes maneras, consulte ¿Cuáles son las limitaciones prácticas de un lenguaje completo que no es Turing como Coq? (que esta respuesta es en gran medida tomada de).