programming languages - programing - ¿Qué es la "Programación funcional total"?
functional programming vs oop (3)
Si entendí eso correctamente, la Programación Funcional Total significa exactamente eso: Programación con Funciones Totales. Si recuerdo correctamente mis cursos de matemática, una función total es una función que se define en todo su dominio, una función parcial es aquella que tiene "agujeros" en su definición.
Ahora, si tiene una función que para un valor de entrada v
entra en una recursión infinita o un ciclo infinito o en general no termina de otra manera, entonces su función no está definida para v
, y por lo tanto parcial, es decir, no total.
La Programación Funcional Total no le permite escribir tal función. Todas las funciones siempre devuelven un resultado para todas las entradas posibles; y el verificador de tipos asegura que este es el caso.
Creo que esto simplifica enormemente el manejo de errores: no hay ninguno.
El inconveniente ya se menciona en su presupuesto: no es Turing-completo. Por ejemplo, un sistema operativo es esencialmente un bucle infinito gigante. De hecho, no queremos que un sistema operativo finalice, llamamos a este comportamiento un "crash" y gritamos en nuestras computadoras al respecto.
Wikipedia tiene esto que decir:
La programación funcional total (también conocida como programación funcional fuerte, que debe contrastarse con la programación funcional ordinaria o débil) es un paradigma de programación que restringe el rango de programas a aquellos que están probando la terminación.
y
Estas restricciones significan que la programación funcional total no es Turing-completa. Sin embargo, el conjunto de algoritmos que se pueden utilizar sigue siendo enorme. Por ejemplo, cualquier algoritmo que haya tenido un límite superior asintótico calculado para él se puede transformar trivialmente en una función de terminación provable utilizando el límite superior como un argumento adicional que se decrementa en cada iteración o recursión.
También hay un Lambda The Ultimate Post sobre un artículo sobre Programación Funcional Total .
No me había encontrado con eso hasta la semana pasada en una lista de correo.
¿Hay más recursos, referencias o implementaciones de ejemplo que conozcas?
La caridad es otro idioma que garantiza la terminación:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html
Hume es un lenguaje con 4 niveles. El nivel exterior está completo y la capa más interna garantiza la terminación:
http://www-fp.cs.st-andrews.ac.uk/hume/report/
Si bien esta es una vieja pregunta, creo que ninguna de las respuestas hasta ahora menciona la verdadera motivación para la programación funcional total, que es la siguiente:
Si los programas son pruebas y las pruebas son programas, entonces los programas que tienen "agujeros" no tienen ningún sentido como pruebas e introducen incoherencias lógicas.
Básicamente, si una prueba es un programa, se puede usar un ciclo infinito para probar algo . Esto es realmente malo y proporciona gran parte de la motivación de por qué es posible que deseemos programar totalmente. Otras respuestas tienden a no dar cuenta de la otra cara del papel. Si bien los idiomas no están técnicamente completos, puede recuperar una gran cantidad de programas interesantes mediante el uso de definiciones y funciones co-inductivas. Somos muy propensos a pensar en datos inductivos , pero codata tiene un propósito importante en estos lenguajes, donde puedes definir totalmente una definición que es infinita (y cuando realizas una computación real que termina, posiblemente usarás solo una parte finita de esto , o tal vez no, si estás escribiendo un sistema operativo!).
También es de notar que la mayoría de los asistentes de pruebas trabajan en base a este principio, Coq, por ejemplo.