“Una prueba es un programa; la fórmula que demuestra es un tipo para el programa "

37

Esta podría ser una pregunta filosófica, pero creo que hay una respuesta objetiva.

Si lees el artículo de Wikipedia sobre Haskell, puedes encontrar lo siguiente:

El lenguaje se basa en las observaciones de Haskell Curry y sus descendientes intelectuales, que "una prueba es un programa; la fórmula que prueba es un tipo para el programa"

Ahora, lo que pregunto es: ¿esto realmente no se aplica a casi todos los lenguajes de programación? ¿Qué característica (o conjunto de características) de Haskell hace que cumpla con esta declaración? En otras palabras, ¿cuáles son las formas notables en que esta declaración afectó el diseño del lenguaje?


fuente
44
¿Alguien quiere explicar por qué los votos de "cierre", por favor?
1
@Grigory Javadyan: No voté para cerrar, pero probablemente sea porque la pregunta está fuera del tema para SO - las preguntas filosóficas, objetivamente respondibles o no, generalmente no son apropiadas aquí. Sin embargo, en este caso creo que es justificable, porque la respuesta tiene profundas implicaciones prácticas sobre cómo se usa realmente Haskell.
2
@Grigory: si esta pregunta fue un problema real con una solución real (en código), entonces puede permanecer en SO. Votado para cerrar y pasar a Programadores.
99
Solo para agregar a eso porque estoy un poco confuso: las respuestas a estas preguntas están repletas de referencias a la investigación de CS y, en ese sentido, son más "objetivas" que el 90% de SO. Además, el criterio de sixlettervariable (que la solución necesita código) es increíblemente limitado para una amplia gama de preguntas de programación genuinas que no son subjetivas ni fuera de tema. Realmente hubiera gustado ver el resurgir inclusionista / deletionist debate sobre SO, pero si programación claramente hilos como este ser golpeada, entonces me preocupe ...
SCLV
2
Soy ambivalente acerca de dónde termina esto, principalmente porque no tengo muy claro qué tipo de contenido se supone que debe estar en Programmers.SE vs. SO. Pero diré que los Programadores se describen en varios lugares como "preguntas subjetivas", lo que esta pregunta enfáticamente no es . Mi respuesta es tan informal y ondulada como podría ser, y todavía podría respaldar la mayor parte fácilmente con referencias que incluso los editores de Wikipedia aceptarían.
CA McCann

Respuestas:

38

El concepto esencial se aplica universalmente de alguna manera, sí, pero rara vez de manera útil.

Para comenzar, desde la perspectiva de la teoría de tipos, esto supone que los lenguajes "dinámicos" se consideran mejor como que tienen un solo tipo, que contiene (entre otras cosas) metadatos sobre la naturaleza del valor que ve el programador, incluido lo que estos lenguajes dinámicos llamarían un "tipo" en sí (que no es lo mismo, conceptualmente). Es probable que cualquier prueba de este tipo no sea interesante, por lo que este concepto es principalmente relevante para los lenguajes con sistemas de tipo estático.

Además, muchos lenguajes que supuestamente tienen un "sistema de tipos estático" deben considerarse dinámicos en la práctica, en este contexto, porque permiten la inspección y conversión de tipos en tiempo de ejecución. En particular, esto significa cualquier lenguaje con soporte incorporado por defecto para "reflexión" o similar. C #, por ejemplo.

Haskell es inusual en la cantidad de información que espera que proporcione un tipo, en particular, las funciones no pueden depender de ningún valor que no sean los especificados como sus argumentos. En un lenguaje con variables globales mutables, por otro lado, cualquier función puede (potencialmente) inspeccionar esos valores y cambiar el comportamiento en consecuencia. Por lo tanto, una función Haskell con tipo A -> Bpuede considerarse como un programa en miniatura que demuestra que Aimplica B; una función equivalente en muchos otros idiomas solo nos dirá eso Ay lo que sea que sea ​​el estado global en el alcance combinado implica B.

Tenga en cuenta que si bien Haskell tiene soporte para cosas como la reflexión y los tipos dinámicos, el uso de tales características debe indicarse en la firma de tipo de una función; igualmente para el uso del estado global. Ninguno de los dos está disponible por defecto.

También hay formas de romper las cosas en Haskell, por ejemplo, permitiendo excepciones de tiempo de ejecución, o usando operaciones primitivas no estándar proporcionadas por el compilador, pero éstas tienen la gran expectativa de que solo se usarán con plena comprensión de formas que ganaron ' No dañar el significado del código externo. En teoría, se podría decir lo mismo de otros idiomas, pero en la práctica con la mayoría de los otros idiomas es más difícil lograr cosas sin "hacer trampa" y menos mal visto "hacer trampa". Y, por supuesto, en verdaderos lenguajes "dinámicos" todo el asunto sigue siendo irrelevante.

El concepto también puede llevarse mucho más lejos de lo que está en Haskell.

CA McCann
fuente
Sin embargo, tenga en cuenta que las excepciones se pueden integrar completamente en un sistema de tipos.
cabeza de jardín
18

Tienes razón en que la correspondencia Curry-Howard es algo muy general. Vale la pena familiarizarse con un poco sobre su historia: http://en.wikipedia.org/wiki/Curry-Howard_correspondence

Notarás que, tal como se formuló originalmente, esta correspondencia se aplicaba particularmente a la lógica intuicionista por un lado, y al cálculo lambda simplemente escrito (STLC) por el otro.

Haskell clásico: versiones del '98 o incluso anteriores, se acercaban mucho al STLC, y en su mayor parte había una traducción directa muy simple entre cualquier expresión dada en Haskell y un término correspondiente en el STLC (extendido con recursión y unos pocos tipos primitivos). Entonces esto hizo que Curry-Howard fuera muy explícito. Hoy, gracias a las extensiones, dicha traducción es un negocio algo más complicado.

Entonces, en cierto sentido, la pregunta es por qué Haskell se "desugará" en el STLC de manera tan directa. Se me ocurren dos cosas:

  • Tipos A diferencia de Scheme, que también es una especie de cálculo lambda azucarado (entre otras cosas), Haskell está fuertemente tipado. Esto significa que no existen términos en Haskell clásico que, por definición , no pueden ser términos bien escritos en el STLC.
  • Pureza. Una vez más, a diferencia de Scheme, pero como el STLC, Haskell es un lenguaje puro, referencialmente transparente. Esto es muy importante Los idiomas con efectos secundarios pueden integrarse en idiomas que no tienen efectos secundarios. Sin embargo, hacerlo es una transformación de todo el programa, no simplemente un desapilado local. Para tener la correspondencia directa , es necesario que comience con un lenguaje puramente funcional.

También hay una forma importante en que Haskell, como la mayoría de los idiomas, falla con respecto a una aplicación directa de la correspondencia Curry-Howard. Haskell, como lenguaje completo de turing, contiene la posibilidad de recurrencia ilimitada y, por lo tanto, de no terminación. El STLC no tiene un operador de punto fijo, no está completo y se está normalizando fuertemente , lo que significa que ninguna reducción de un término en el STLC no terminará. La posibilidad de recurrencia significa que uno puede "engañar" a Curry-Howard. Por ejemplo, let x = x in xtiene el tipoforall a. aEs decir, como nunca regresa, ¡puedo fingir que me da algo! Como siempre podemos hacer esto en Haskell, eso significa que no podemos "creer" completamente en ninguna prueba correspondiente a un programa de Haskell a menos que tengamos una prueba por separado de que el programa en sí está finalizando.

El linaje de la programación funcional anterior a Haskell (especialmente la familia ML) fue el resultado de la investigación de CS centrada en la construcción de lenguajes sobre los que fácilmente podría probar cosas (entre otras cosas), investigación muy consciente y derivada de CH para comenzar. Por el contrario, Haskell ha servido como lenguaje anfitrión y como inspiración para una serie de asistentes de pruebas en desarrollo, como Agda y Epigram, que se basan en desarrollos en la teoría de tipos muy relacionados con el linaje de CH.

sclv
fuente
1
Sería bueno enfatizar que la no determinación socava la prueba de ciertas maneras que, aunque obviamente es catastrófica desde un punto de vista lógico, preserva muchas otras propiedades. En particular, una función A -> B, dada una A, producirá una Bo nada en absoluto. Nunca producirá un C, y qué valor de tipo Bproporciona, o si diverge, todavía depende exclusivamente del Aproporcionado.
@camccann: un poco quisquilloso, pero distinguiría entre el fondo y "nada en absoluto", que es más como Void, ¿no? La pereza hace que sea más y menos complicado ambos. Yo diría que una función de A -> B siempre produce un valor de tipo B, pero ese valor puede tener menos información de la que cabría esperar.
sclv 01 de
¡Nitpicking es divertido! Cuando digo "nada" me refiero al nivel de valor en un contexto de evaluación, mientras que el fondo solo existe realmente como una abstracción, no como algo tangible. Una expresión que se está evaluando nunca "verá" un valor de fondo, solo términos que no usa (que podrían ser fondo) y términos que usa (que tienen valores no inferiores). Tratar de usar el fondo "nunca sucede" en algún sentido porque intentar hacerlo termina la evaluación de la expresión completa antes de que ocurra el uso.
12

Para una aproximación de primer orden, la mayoría de los otros idiomas (débilmente y / o tipados) no admiten la delineación estricta de nivel de idioma entre un

  • proposición (es decir, un tipo)
  • una prueba (es decir, un programa que demuestra cómo podemos construir la proposición a partir de un conjunto de primitivas y / u otras construcciones de orden superior )

y la estricta relación entre los dos. En todo caso, las mejores garantías que brindan otros idiomas son

  • dada una restricción limitada en la entrada, junto con lo que sea que esté en el entorno en ese momento, podemos producir un valor con una restricción limitada. (tipos estáticos tradicionales, cf C / Java)
  • cada construcción es del mismo tipo (tipos dinámicos, cf ruby ​​/ python)

Tenga en cuenta que por tipo , nos referimos a una proposición y, por lo tanto, algo que describe mucha más información que simplemente int o bool . En Haskell, existe una cultura permeadora de una función que solo se ve afectada por sus argumentos , sin excepciones *.

Para ser un poco más riguroso, la idea general es que al aplicar un enfoque intuitivo rígido a (casi) todas las construcciones de programas (es decir, solo podemos probar lo que podemos construir), y al limitar el conjunto de construcciones primitivas en tal manera que tenemos

  • proposiciones estrictas para todas las primitivas del lenguaje
  • Un conjunto limitado de mecanismos por los cuales se pueden combinar las primitivas

Las construcciones de Haskell tienden a prestarse muy bien al razonamiento sobre su comportamiento. Si podemos construir una prueba (léase: función) que demuestre que Aimplica B, esta tiene propiedades muy útiles:

  • que siempre se lleva a cabo (siempre y cuando tenemos una A, podemos construir una B)
  • esta implicación se basa solo en A, y nada más.

lo que nos permite razonar sobre invariantes locales / globales de manera efectiva. Para volver a la pregunta original; Las características del lenguaje de Haskell que fascinan mejor esta mentalidad son:

  • Pureza / segmentación de efectos en construcciones explícitas (¡los efectos se contabilizan y se tipifican!)
  • Inferencia de tipo / Comprobación en compiladores Haskell
  • La capacidad de incrustar invariantes de control y / o flujo de datos en las propuestas / tipos que un programa se propone probar: (con polimorfismo, familias de tipos, GADT, etc.)
  • Integridad referencial

Ninguno de los cuales es exclusivo de Haskell (muchas de estas ideas son increíblemente antiguas). Sin embargo, cuando se combina con un rico conjunto de abstracciones en las bibliotecas estándar (generalmente se encuentran en clases de tipos), diversos niveles de sintaxis y un estricto compromiso con la pureza en el diseño del programa, terminamos con un lenguaje que de alguna manera logra ser ambos lo suficientemente práctico para aplicaciones del mundo real , pero al mismo tiempo resulta más fácil razonar sobre los idiomas más tradicionales.

Esta pregunta merece una respuesta suficientemente profunda, y no podría hacerle justicia en este contexto. Sugeriría leer más en wikipedia / en la literatura:

* NB: estoy pasando por alto / ignorando algunos de los aspectos más difíciles de las impurezas de Haskell (excepciones, no terminación, etc.) que solo complicarían el argumento.

Raeez
fuente
4

Que caracteristica El sistema de tipos (siendo estático, puro, polimórfico). Un buen punto de partida es "Theorems for Free" de Wadler. ¿Efecto notable en el diseño del lenguaje? El tipo IO, clases de tipo.

ja.
fuente
0

La jerarquía de Kleene nos muestra que las pruebas no son programas.

La primera relación recursiva es:

R1( Program , Iteration )  Program halts at Iteration.
R2( Theorem , Proof ) Proof proves a Theorem.

Las primeras relaciones recursivamente enumerables son:

(exists x) R1( Program , x )  Program Halts.
(exists x) R2( Theorem , x)   Theorem is provable.

De modo que un programa es un teorema y la iteración que existe en la que el programa se detiene es como la prueba que existe que prueba el teorema.

Program = Theorem
Iteration = Proof

Cuando un programa se produce correctamente a partir de una especificación, debemos ser capaces de demostrar que cumple con la especificación, y si podemos demostrar que un programa cumple con una especificación, entonces es la síntesis correcta del programa. Entonces realizamos la síntesis del programa si demostramos que el programa cumple con la especificación. El teorema de que el programa satisface la especificación es el programa en el sentido de que el teorema se refiere al programa que se sintetiza.

Las falsas conclusiones de Martin Lof nunca han producido ningún programa de computadora y es sorprendente que la gente crea que es una metodología de síntesis de programas. Nunca se han dado ejemplos completos de un programa que se sintetiza. Una especificación como "ingresar un tipo y generar un programa de ese tipo" no es una función. Existen múltiples programas de este tipo y elegir uno al azar no es una función recursiva o incluso una función. Es solo un intento tonto de mostrar la síntesis del programa con un programa tonto que no representa un programa de computadora real que calcule una función recursiva.

Charlie Volkstorf
fuente
2
¿Cómo funciona esta respuesta a la pregunta preguntó: "¿cuáles son las formas perceptibles en la que esta declaración afectado el diseño de la lengua?"
mosquito
1
@gnat: esta respuesta aborda una suposición subyacente dentro de la pregunta original, a saber: " doesn't this really apply to pretty much all the programming languages?" Esta respuesta afirma / muestra que la suposición no es válida, por lo que no tiene sentido abordar el resto de las preguntas que se basan en una premisa errónea .