tipos - ¿Por qué la inferencia de tipo F#es tan voluble?

inferencia de tipos c# (5)

¿Hay algo intrínsecamente diferente en el diseño o la ideología de F # que está causando esto?

Sí. F # usa el tipado nominal en lugar del estructural porque es más simple y, por lo tanto, más fácil de usar por simples mortales.

Considere este ejemplo F #:

let lengths (xss: _ [] []) = Array.map (fun xs -> xs.Length) xss let lengths (xss: _ [] []) = xss |> Array.map (fun xs -> xs.Length)

El primero no compila porque el tipo de xs dentro de la función anónima no se puede inferir porque F # no puede expresar el tipo "alguna clase con un miembro de Length ".

Por el contrario, OCaml puede expresar el equivalente directo:

let lengths xss = Array.map (fun xs -> xs#length) xss

porque OCaml puede expresar ese tipo (está escrito <length: ''a ..> ). Tenga en cuenta que esto requiere una inferencia de tipo más poderosa que la que tienen actualmente F # o Haskell, por ejemplo OCaml puede inferir tipos de suma.

Sin embargo, se sabe que esta característica es un problema de usabilidad. Por ejemplo, si te equivocas en otro lugar del código, entonces el compilador aún no ha inferido que se suponía que el tipo de xs era una matriz, por lo que cualquier mensaje de error que pueda proporcionar solo puede proporcionar información como "algún tipo con un miembro de longitud" y no "una matriz". Con solo un código un poco más complicado, esto rápidamente se sale de control ya que tiene tipos masivos con muchos miembros estructuralmente inferidos que no se unifican del todo, lo que lleva a mensajes de error incomprensibles (como C ++ / STL).

El compilador F # parece realizar una inferencia de tipo de una manera (bastante) estricta de arriba a abajo, de izquierda a derecha. Esto significa que debe hacer cosas como poner todas las definiciones antes de su uso, el orden de compilación de archivos es significativo y tiende a tener que reorganizar cosas (vía |> o lo que tenga) para evitar tener anotaciones de tipo explícito.

¿Qué tan difícil es hacerlo más flexible, y es eso planeado para una versión futura de F #? Obviamente se puede hacer, ya que Haskell (por ejemplo) no tiene tales limitaciones con una inferencia igualmente poderosa. ¿Hay algo intrínsecamente diferente en el diseño o la ideología de F # que está causando esto?

F # utiliza la compilación de un solo paso de modo que solo puede hacer referencia a los tipos o funciones que se han definido anteriormente en el archivo en el que se encuentra actualmente o que aparecen en un archivo que se especificó anteriormente en el orden de compilación.
Recientemente le pregunté a Don Syme acerca de hacer múltiples pases de fuente para mejorar el proceso de inferencia tipo. Su respuesta fue "Sí, es posible hacer una inferencia de tipo de paso múltiple. También hay variaciones de paso único que generan un conjunto finito de restricciones.
Sin embargo, estos enfoques tienden a dar malos mensajes de error y pobres resultados intellisense en un editor visual ".

http://www.markhneedham.com/blog/2009/05/02/f-stuff-i-get-confused-about/#comment-16153

Creo que el algoritmo utilizado por F # tiene el beneficio de que es fácil (al menos aproximadamente) explicar cómo funciona, por lo que una vez que lo entiendes, puedes tener algunas expectativas sobre el resultado.

El algoritmo siempre tendrá algunas limitaciones. Actualmente, es bastante fácil de entender. Para algoritmos más complicados, esto podría ser difícil. Por ejemplo, creo que podría encontrarse con situaciones en las que piense que el algoritmo debería ser capaz de deducir algo, pero si fuera lo suficientemente general como para cubrir el caso, sería no decidible (por ejemplo, podría seguir girando por siempre).

Otro pensamiento sobre esto es que revisar el código de arriba hacia abajo corresponde a cómo leemos el código (al menos algunas veces). Entonces, tal vez el hecho de que tendemos a escribir el código de una manera que permite la inferencia de tipos también hace que el código sea más legible para las personas ...

En cuanto a la "inferencia igualmente poderosa de Haskell", no creo que Haskell tenga que lidiar con

Subtipo dinámico tipo OO (las clases tipo pueden hacer cosas similares, pero las clases tipo son más fáciles de escribir / inferir)
sobrecarga de métodos (las clases de tipos pueden hacer cosas similares, pero las clases de tipos son más fáciles de escribir / inferir)

Es decir, creo que F # tiene que lidiar con algunas cosas duras que Haskell no tiene. (Casi con seguridad, Haskell tiene que lidiar con cosas difíciles que F # no tiene).

Como se menciona en otras respuestas, la mayoría de los principales lenguajes .NET tienen las herramientas de Visual Studio como una importante influencia en el diseño del lenguaje (ver, por ejemplo, cómo LINQ tiene "de ... seleccionar" en lugar de la selección de SQL-y ... de ", motivado por obtener intellisense de un prefijo de programa). Intellisense, garabatos de error y comprensibilidad de mensajes de error son todos factores de herramientas que informan el diseño de F #.

Puede ser posible mejorar e inferir más (sin sacrificar otras experiencias), pero no creo que esté entre nuestras principales prioridades para las versiones futuras del lenguaje. (Los Haskeller pueden ver la inferencia tipo F # como algo débil, pero probablemente son superados en número por los C # ers que ven la inferencia tipo F # como muy fuerte :))

También podría ser difícil extender la inferencia tipo sin interrupción; está bien cambiar los programas ilegales por legales en una versión futura, pero debe tener mucho cuidado para asegurar que los programas legales anteriores no cambien la semántica según las nuevas reglas de inferencia, y la resolución de nombres (una terrible pesadilla en todos los idiomas) es probable interactuar con cambios de inferencia de tipos de maneras sorprendentes.

La respuesta corta es que F # se basa en la tradición de SML y OCaml, mientras que Haskell proviene de un mundo ligeramente diferente de Miranda, Gofer y similares. Las diferencias en la tradición histórica son sutiles, pero omnipresentes. Esta distinción también es paralela en otros lenguajes modernos, como el Coq de tipo ML que tiene las mismas restricciones de ordenamiento que el Agda similar a Haskell que no lo hace.

Esta diferencia está relacionada con la evaluación perezosa vs estricta. El lado Haskell del universo cree en la pereza, y una vez que ya crees en la pereza, la idea de agregar holgazanería a cosas como la inferencia de tipo es una obviedad. Mientras que en el lado ML del universo siempre que sea necesaria la pereza o recursión mutua, debe señalarse explícitamente mediante el uso de palabras clave como with , y , rec , etc. Prefiero el enfoque de Haskell porque da como resultado un código menos repetitivo, pero hay mucha gente que piensa que es mejor hacer que estas cosas sean explícitas.