haskell - que - programacion funcional desventajas

¿Cuál es el motivo de ''let rec'' para el lenguaje funcional impuro OCaml? (6)

¿Cuáles son las razones técnicas que obliga a dejar de rec mientras que los lenguajes funcionales puros no?

La recursividad es una bestia extraña. Tiene una relación con la pureza, pero es un poco más oblicua que esto. Para ser claros, podrías escribir "alterna-Haskell" que conserva su pureza, su pereza pero no tiene ataduras recursivas de manera predeterminada y exige algún tipo de marcador de rec como lo hace OCaml. Algunos incluso preferirían esto.

En esencia, hay muchos tipos diferentes de "let" s posibles. Si comparamos let y let rec en OCaml veremos una pequeña diferencia. En semántica formal estática, podríamos escribir

Γ ⊢ E : A Γ, x : A ⊢ F : B ----------------------------- Γ ⊢ let x = E in F : B

que dice que si podemos demostrar en un entorno variable Γ que E tiene el tipo A y si podemos demostrar en el mismo entorno variable Γ aumentado con x : A que F : B entonces podemos demostrar que en el entorno variable Γ let x = E in F tiene tipo B

Lo que hay que vigilar es el argumento Γ . Esta es solo una lista de pares ("nombre de variable", "valor") como [(x, 3); (y, "hello")] [(x, 3); (y, "hello")] y aumentar la lista como Γ, x : A solo significa consing (x, A) en ella (siento que la sintaxis esté volteada).

En particular, vamos a escribir el mismo formalismo para let rec

Γ, x : A ⊢ E : A Γ, x : A ⊢ F : B ------------------------------------- Γ ⊢ let rec x = E in F : B

En particular, la única diferencia es que ninguna de nuestras instalaciones funciona en el entorno simple; ambos pueden asumir la existencia de la variable x .

En este sentido, let y let rec son simplemente bestias diferentes.

Entonces, ¿qué significa ser puro? En la definición más estricta , de la que Haskell ni siquiera participa, debemos eliminar todos los efectos, incluida la no terminación. La única forma de lograr esto es eliminar nuestra capacidad para escribir recursiones sin restricciones y reemplazarlas solo con cuidado.

Existen muchos idiomas sin recurrencia. Quizás el más importante es el cálculo Lambda Simply Typed. En su forma básica es el cálculo lambda regular, pero aumentada con una disciplina de tipeo donde los tipos son algo así como

type ty = | Base | Arr of ty * ty

Resulta que STLC no puede representar recursión --- el combinador Y, y todos los otros combinadores de primos de punto fijo, no pueden ser tipados. Por lo tanto, STLC no es Turing completo.

Sin embargo, es inflexiblemente puro . Sin embargo, logra esa pureza con el más triste de los instrumentos al prohibir por completo la recursión. Lo que realmente nos gustaría es algún tipo de recursión balanceada y cuidadosa que no conduzca a la no terminación --- todavía seremos Turing Incompleto, pero no tan paralizado.

Algunos idiomas prueban este juego. Hay maneras inteligentes de agregar recursividad tipeada a lo largo de una división entre data y codata que asegura que no se pueden escribir funciones no terminadas. Si estás interesado, sugiero aprender un poco de Coq.

Pero el objetivo de OCaml (y el de Haskell también) no es ser delicado aquí. Ambos lenguajes son inflexiblemente Turing Complete (y por lo tanto "prácticos"). Así que analicemos algunas formas más contundentes de aumentar el STLC con recurrencia.

El más sombrío del grupo es agregar una sola función incorporada llamada fix

val fix : (''a -> ''a) -> ''a

o, en una notación OCaml-y más genuina que requiere expansión eta

val fix : ((''a -> ''b) -> (''a -> ''b)) -> (''a -> ''b)

Ahora, recuerde que solo estamos considerando un STLC primitivo con una fix añadida. De hecho, podemos escribir una fix (la última al menos) en OCaml, pero eso es hacer trampa en este momento. ¿Qué fix comprar el STLC como primitivo?

Resulta que la respuesta es: "todo". STLC + Fix (básicamente un lenguaje llamado PCF ) es impuro y Turing completo. También es simplemente tremendamente difícil de usar.

Así que este es el último obstáculo para saltar: ¿cómo hacemos que la fix sea más fácil de trabajar? ¡Al agregar enlaces recursivos!

Ya, STLC tiene una construcción let . Puedes pensar que es solo azúcar sintáctica:

let x = E in F ----> (fun x -> F) (E)

pero una vez que hemos agregado la fix , también tenemos el poder de introducir ligaduras para let rec

let rec x a = E in F ----> (fun x -> F) (fix (fun x a -> E))

En este punto, nuevamente debería estar claro: let y let rec sean bestias muy diferentes. Incorporan diferentes niveles de poder lingüístico y let rec es una ventana que permite la impureza fundamental a través de la integridad de Turing y la no terminación de efecto de socio.

Por lo tanto, al final del día, es un poco divertido que Haskell, el más puro de los dos idiomas, haya tomado la interesante decisión de abolir las uniones planas. Esa es realmente la única diferencia: no hay sintaxis para representar un enlace no recursivo en Haskell.

En este punto, es esencialmente solo una decisión de estilo. Los autores de Haskell determinaron que los enlaces recursivos eran tan útiles que uno podría suponer que cada enlace es recursivo (y mutuamente, una lata de gusanos ignorada en esta respuesta hasta el momento).

Por otro lado, OCaml te da la capacidad de ser totalmente explícito sobre el tipo de enlace que eliges, let o let rec ¡ let rec !

En el libro Real World OCaml , los autores explican por qué OCaml usa let rec para definir funciones recursivas.

OCaml distingue entre definiciones no recursivas (usando let) y definiciones recursivas (usando let rec) en gran medida por razones técnicas: el algoritmo de inferencia de tipos necesita saber cuándo un conjunto de definiciones de funciones son mutuamente recursivas y por razones que no se aplican a un lenguaje puro como Haskell, estos deben ser marcados explícitamente por el programador.

¿Cuáles son las razones técnicas que obliga a let rec mientras que los lenguajes funcionales puros no?

Creo que esto no tiene nada que ver con ser puramente funcional, es solo una decisión de diseño que en Haskell no tiene permitido hacer

let a = 0;; let a = a + 1;;

mientras que puedes hacerlo en Caml.

En Haskell, este código no funcionará porque let a = a + 1 se interpreta como una definición recursiva y no terminará. En Haskell no tiene que especificar que una definición es recursiva simplemente porque no puede crear una no recursiva (por lo que la palabra clave rec está en todas partes pero no está escrita).

Cuando define una semántica de definición de función, como diseñador de lenguaje, tiene opciones: o bien hacer que el nombre de la función sea visible en el ámbito de su propio cuerpo, o no. Ambas opciones son perfectamente legales, por ejemplo, los lenguajes de la familia C están lejos de ser funcionales, todavía tienen nombres de definiciones visibles en su alcance (esto también se extiende a todas las definiciones en C, lo que hace que int x = x + 1 legal). El lenguaje OCaml decide darnos flexibilidad adicional para hacer la elección por nosotros mismos. Y eso es realmente genial. Decidieron hacerlo invisible de forma predeterminada, una solución bastante descendente, ya que la mayoría de las funciones que escribimos no son recursivas.

Lo que concierne a la cita, en realidad no se corresponde con las definiciones de funciones, el uso más común de la palabra clave rec . Se trata principalmente de "por qué el alcance de la definición de la función no se extiende al cuerpo del módulo". Esta es una pregunta completamente diferente. Después de algunas investigaciones, he encontrado una pregunta muy similar , que tiene una answer , que podría satisfacerte, una cita de ella:

Entonces, dado que el verificador de tipos necesita saber qué conjuntos de definiciones son mutuamente recursivas, ¿qué puede hacer? Una posibilidad es simplemente hacer un análisis de dependencia en todas las definiciones en un alcance y reordenarlas en los grupos más pequeños posibles. Haskell realmente hace esto, pero en idiomas como F # (y OCaml y SML) que tienen efectos secundarios sin restricciones, esta es una mala idea porque también podría reordenar los efectos secundarios . Por lo tanto, le pide al usuario que marque explícitamente qué definiciones son mutuamente recursivas, y por lo tanto, por extensión, donde debe darse la generalización.

Incluso sin ningún reordenamiento, con expresiones no puras arbitrarias, que pueden ocurrir en la definición de la función (un efecto secundario de definición, no evaluación) es imposible construir el gráfico de dependencia. Considere demarshaling y ejecutar la función desde el archivo.

Para resumir, tenemos dos usos de let rec construct, uno es crear una función auto recursiva, como

let rec seq acc = function | 0 -> acc | n -> seq (acc+1) (n-1)

Otra es definir funciones mutuamente recursivas:

let rec odd n = if n = 0 then true else if n = 1 then false else even (n - 1) and even n = if n = 0 then false else if n = 1 then true else odd (n - 1)

En el primer caso, no hay razones técnicas para apegarse a una u otra solución. Esto es solo una cuestión de gusto.

El segundo caso es más difícil. Cuando se deduce el tipo, se deben dividir todas las definiciones de funciones en grupos que consisten en definiciones mutuamente dependientes, para restringir el entorno de escritura. En OCaml es más difícil de hacer, ya que debe tener en cuenta los efectos secundarios. (O puede continuar sin dividirlo en componentes principales, pero esto dará lugar a otro problema: su sistema de tipos será más restrictivo, es decir, no permitirá más programas válidos).

Pero, volviendo a consultar la pregunta original y la cita de RWO, todavía estoy bastante seguro de que no hay razones técnicas para agregar la bandera de rec . Considere, SML que tiene los mismos problemas, pero todavía tiene habilitado de manera predeterminada. Hay una razón técnica, para let ... and ... sintaxis para definir un conjunto de funciones recursivas mutuas. En SML, esta sintaxis no requiere que pongamos el indicador de rec , en OCaml, lo que nos da más flexibilidad, como la capacidad de cambiar a valores con let x = y and y = x expresión.

Diría que en OCaml están tratando de hacer que REPL y los archivos fuente funcionen de la misma manera. Entonces, es perfectamente razonable redefinir alguna función en REPL; por lo tanto, también deben permitirlo en la fuente. Ahora, si usa la función (redefinida) en sí misma, OCaml necesita alguna forma de saber cuál de las definiciones usar: la anterior o la nueva.

En Haskell, simplemente se dieron por vencidos y aceptaron que REPL funciona de diferente manera con los archivos fuente.

No es una cuestión de pureza, se trata de especificar en qué entorno debe verificar la expresión el tipochete. De hecho, le da más poder del que tendría de lo contrario. Por ejemplo (voy a escribir Standard ML aquí porque lo sé mejor que OCaml, pero creo que el proceso de verificación de tipografía es prácticamente el mismo para los dos idiomas), te permite distinguir entre estos casos:

val foo : int = 5 val foo = fn (x) => if x = foo then 0 else 1

Ahora a partir de la segunda redefinición, foo tiene el tipo int -> int . Por otra parte,

val foo : int = 5 val rec foo = fn (x) => if x = foo then 0 else 1

no comprueba el tipo, porque el rec significa que el contador de tipos ya ha decidido que foo ha sido recuperado al tipo ''a -> int , y cuando intenta averiguar qué es lo que ''a debe ser, hay una falla de unificación porque x = foo obliga a foo a tener un tipo numérico, que no es así.

Sin duda puede "parecer" más imperativo, porque la carcasa sin rec permite hacer cosas como esta:

val foo : int = 5 val foo = foo + 1 val foo = foo + 1

y ahora foo tiene el valor 7. No es porque haya sido mutado, sin embargo --- el nombre foo ha sido rebotado 3 veces, y sucede que cada uno de esos enlaces sombreaba un enlace previo de una variable llamada foo . Es lo mismo que esto:

val foo : int = 5 val foo'' = foo + 1 val foo'''' = foo'' + 1

excepto que foo y foo'' ya no están disponibles en el entorno después de que el identificador foo ha sido rebotado. Los siguientes son también legales:

val foo : int = 5 val foo : real = 5.0

lo que deja en claro que lo que está sucediendo es el sombreado de la definición original, en lugar de un efecto secundario.

Si es estilísticamente una buena idea volver a enlazar identificadores es cuestionable, puede ser confuso. Puede ser útil en algunas situaciones (por ejemplo, volver a vincular un nombre de función a una versión de sí mismo que imprime la salida de depuración).

No soy un experto, pero lo adivinaré hasta que aparezcan los verdaderos expertos. En OCaml puede haber efectos secundarios que ocurren durante la definición de una función:

let rec f = let () = Printf.printf "hello/n" in fun x -> if x <= 0 then 12 else 1 + f (x - 1)

Esto significa que el orden de las definiciones de funciones debe conservarse en algún sentido. Ahora imagina que dos conjuntos distintos de funciones mutuamente recursivas están intercalados. No parece del todo fácil para el compilador conservar el orden mientras lo procesa como dos conjuntos separados de definiciones mutuamente recursivas.

El uso de `let rec ... and`` significa que distintos conjuntos de definiciones mutuamente recursivas de función no se pueden intercalar en OCaml como lo hacen en Haskell. Haskell no tiene efectos secundarios (en cierto sentido), por lo que las definiciones se pueden reordenar libremente.