¿Cuál es la "pregunta" que la teoría del lenguaje de programación está tratando de responder?

10

He estado interesado en varios temas como Combinatory Logic, Lambda Calculus, Functional Programming por un tiempo y los he estado estudiando. Sin embargo, a diferencia de la "Teoría de la computación", que se esfuerza por responder a la pregunta de "computabilidad", es decir, cosas que pueden / no pueden computarse con varias restricciones, estoy luchando por encontrar el análogo de "Teoría de la programación".

Wikipedia lo describe como:

La teoría del lenguaje de programación (PLT) es una rama de la informática que se ocupa del diseño, implementación, análisis, caracterización y clasificación de lenguajes de programación y sus características individuales.

Esto es como decir "todo" que no es realmente específico.

La progresión común de los temas suele ser así:

Lógica combinatoria> Cálculo de Lambda> Teoría de tipos de Martin Lof> Cálculo de Lambda tipado> (Algo sucede aquí)> Desarrollados lenguajes de programación, que tienen muy poca conexión con CL /λ

Puedo ver las "matemáticas" subyacentes involucradas con CL / y las pruebas interesantes que surgen como resultado, incluido el teorema de Church-Rosser y eso está bien. Sin embargo, ¿me cuesta entender el "objetivo final" de toda esta empresa? ¿Cuál es el santo grial de PLT si quieres? Por ahora parece estar rascando una picazón intelectual, pero realmente no puedo cruzar el puente de la investigación / teoría a nada práctico.λ

Nota: Lo obtengo hasta usar el -calc para pruebas de indecidibilidad. Pero más allá de su aplicabilidad a la "computabilidad", simplemente no lo entiendo y me está costando entender incluso la necesidad de investigar en PLT a partir de este POV estrecho. ¿Algún libro existente, referencias que puedan arrojar luz sobre el "panorama general" de PLT?λ

Doctor
fuente
1
Estás ignorando totalmente franjas enteras de PLT en tu "progresión común". Por alguna razón, su punto de vista parece estar sesgado por el cálculo de y la teoría de tipos. Echemos un vistazo a los documentos aceptados por POPL 2019 : programación aleatoria concurrente, programación probabilística, ensamblaje verificable, efectos algebraicos, redes neuronales de certificación, modelos de memoria débil PL y hardware, programación cuántica, etc. Muchas cosas que no son "solo teoría de los tipos ", ¿no dirías? λ
Andrej Bauer
Estás 100% correcto. Por eso llamé a mi "POV estrecho". Estoy familiarizado con los "otros temas" solo leyendo por aquí y revisando los procedimientos de SIGPLAN / POPL. Todavía no he encontrado una "referencia / libro holístico" que ofrezca una visión general amplia de PLT que incluya los temas que mencionó. El bit de teoría de tipos es solo de "mi" POV de (¿creando?) Lenguajes de programación. ¿Tendría algunos consejos que podrían proporcionar introducciones de alto nivel a las diversas áreas de PLT para obtener una visión general? Tengo curiosidad por saber qué "modelos" subyacentes usan y cómo. todas partes? λ
PhD
2
π

Respuestas:

13

El propósito general de PLT es hacer que la ingeniería de software industrial (en un sentido general) sea más barata (también en un sentido general), mediante la optimización de la herramienta más importante (lenguajes de programación) y el ecosistema de herramientas asociado.

Algunas razones por las cuales las matemáticas están involucradas:

  • Los PL son altamente no triviales, y no está claro que hagan lo correcto sin pruebas. Las matemáticas dan un modelo simplificado de lenguajes de programación reales. Este modelo nos permite estudiar lenguajes de programación reales en una configuración mucho más simplificada, eliminando (con suerte) la mayoría de los problemas que ya existen a nivel de modelo. Los lenguajes de programación reales son actualmente matemáticamente intratables. En otras palabras: el cálculo lambda es la mosca de la fruta, el E. Coli, la vaca esférica del PLT.

  • PLT carece de métodos empíricos adecuados, lo cual sería bueno / mejor tener, por lo que las matemáticas se realizan como un sustituto.

  • Las matemáticas son hermosas y profundas.

  • Las matemáticas brindan una metodología de investigación simple, probada y de prueba, que es importante para ayudar a los estudiantes de doctorado a graduarse. Típicamente, alguna variante de, por ejemplo: Investigar la función PL XYZ mediante su adición al cálculo lambda. Agregue tipos simples para XYZ y pruebe la solidez de los tipos. Agregue genéricos para XYZ y pruebe la solidez del tipo. Probar un teorema de parametricidad para genéricos XYZ. Agregue tipos dependientes para XYZ y pruebe la solidez de los tipos. Desarrolle una inferencia de tipo parcial para los tipos dependientes de XYZ. Agregue tipos graduales para XYZ y pruebe la solidez de los tipos. Agregar contratos para XYZ. Cada uno de esos es un papel. Puede detenerse si su estudiante de doctorado o postdoctorado se queda sin tiempo. Cada uno de los anteriores es interesante y proporcionará información sobre genéricos, paramétrica, inferencia de tipos, etc. Esta tubería es una excelenteforma de navegar por las aguas difíciles de todos los lenguajes de programación posibles. Una segunda forma de aprender es implementar idiomas en un compilador, pero eso es menos manejable para un individuo.

Si se necesita PLT es una pregunta interesante. La mayoría de los programadores que trabajan parecen pensar que no lo es. Están equivocados: la mayoría de los lenguajes desarrollados por programadores que trabajan sin experiencia en PLT (por ejemplo, Javascript, PHP) comienzan terriblemente y cometen todos los errores que los teóricos de PL aprendieron durante mucho tiempo a evitar. Si un PL desarrollado por un aficionado llega a la corriente principal, los teóricos de PL necesitan una década más o menos para solucionar los defectos obvios (por ejemplo, actualizar un sistema de tipeo estático, ver Tipos de letra). Permítanme resumir esta situación:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

Aparte: este estado de cosas es completamente culpa del PLT porque, debido a que la mayoría de ellos no tienen experiencia en programación industrial, entonces realmente no sé cuáles son los puntos débiles de los ingenieros de software que trabajan. En particular, por razones sociológicas, la mayoría de los teóricos de PL piensan que la programación funcional pura en lenguajes como Agda es la solución a todos los problemas, lo que no resiste el escrutinio.

Martin Berger
fuente
1
@MartinBerger: ¿ CompCert cuenta como un ejemplo de poder manejar un lenguaje de programación del mundo real "teóricamente"? Si no es así, qué tan alto está estableciendo la barra, porque CompCert es bastante impresionante.
Andrej Bauer
2
@MartinBerger: Considere diluir "la mayoría de los teóricos de PL piensan que la programación funcional pura en lenguajes como Agda es la solución a todos los problemas" porque eso es solo su despotricar y desahogarse. Para empezar, incluso si observa los temas que están actualmente presentes en ICFP y POPL, la mayoría se trata de lenguajes de programación impuros .
Andrej Bauer
55
@PhD: hay mucho más en PLT que la teoría de tipos. Es solo que la teoría de tipos es lo primero que notas porque es una de las principales herramientas de PLT.
Andrej Bauer
1
@AndrejBauer CompCert, CakeML, etc. son impresionantes, pero están muy lejos de compiladores ampliamente utilizados como LLVM, GCC, etc. Además, los compiladores, a diferencia de cualquier software del mundo real, tienen una especificación (tipo de / tipo de) que simplemente no obtienes en la ingeniería de software industrial normal. Sin mencionar que una gran parte del trabajo inicial de Xavier en CompCert consistió en precisar la especificación.
Martin Berger
2
@PhD Con respecto a "" radicalmente más productivo "que> C / C ++ no PLT, Java, C #", tenga en cuenta que si observa esos lenguajes, más específicamente, su evolución en el tiempo, casi todo lo que han adquirido tiempo, por ejemplo, lambdas, mónadas (LINQ), coincidencia de patrones, inferencia de tipo parcial proviene de PLT. El equipo de C # tiene doctorados PLT. De hecho, trataron de contratarme en algún momento. La entrevista de trabajo fue cuando estaba tratando de convencer a Anders Heijlsberg de que C # necesita medicamentos genéricos, que no le gustaban en ese momento ...
Martin Berger