programacion - Conversión de OCaml a F#: diferencias entre tipeo e inferencia de tipo
inferencia de tipos c# (3)
Al investigar las diferencias de tipo de inferencia entre F # y OCaml, descubrí que tendían a centrarse en el sistema de tipo nominativo frente a estructural . Luego, encontré rasgos distintivos de los lenguajes de programación funcionales que enumeran la tipificación y la inferencia de tipos como rasgos diferentes.
Dado que el artículo del rasgo dice OCaml y F # ambos usan la inferencia tipo Damas-Milner, que pensé que era un algoritmo estándar, es decir, un algoritmo que no permite variaciones, ¿cómo se relacionan los dos rasgos? ¿Es que Damas-Milner es la base sobre la cual se construyen ambos tipos de sistemas de inferencia, pero que cada uno modifica a Damas-Milner en base a la tipificación?
También verifiqué el código fuente de F # para las palabras Damas, Milner y Hindley y no encontré ninguna. Una búsqueda de la inferencia de palabra apareció el código para la inferencia de tipo.
Si es así, ¿hay documentos que discutan los detalles de cada tipo de algoritmo de inferencia para el idioma en particular, o tengo que mirar el código fuente de OCaml y F # .
EDITAR
Aquí hay una página que destaca algunas diferencias relacionadas con la inferencia de tipo entre OCaml y F #.
Creo que cuando hablan de tipado estructural en OCaml, probablemente se están refiriendo al sistema de objetos (la parte "O" de "OCaml"). Las partes no objeto de OCaml son bastante estándar sistema de tipo ML; es el sistema de objetos que es inusual.
El sistema de objetos en OCaml es muy diferente del sistema de objetos basado en clase .NET en F #. En OCaml, puede crear objetos directamente sin usar una clase. Y las clases son básicamente una función de conveniencia para crear objetos. Un objeto después de la creación (ya sea creado directamente usando un literal o usando una clase) no tiene ningún concepto de su clase.
Mira lo que sucede cuando escribes una función que toma un objeto y llama a un método particular sobre él:
# let foo x = x#bar;;
val foo : < bar : ''a; .. > -> ''a = <fun>
El tipo de argumento se infiere como un tipo abstracto que incluye un método llamado bar . Por lo tanto, puede tomar cualquier objeto con dicho método y tipo.
Eso es lo que significa cuando dicen que el sistema de objetos está estructuralmente tipado. Lo único que importa de un objeto es su conjunto de métodos, que determina dónde se puede usar. Entonces, la compatibilidad solo se basa en la "estructura" de los métodos. Y no en cualquier idea de "clase".
En cuanto a su pregunta de DM, tiene razón. Tanto para F # como para OCaml, el algoritmo DM es solo un patrón. Los verificadores de tipo se amplían para admitir funciones personalizadas. En OCaml estas características incluyen objetos con tipos de fila, variantes de poli, módulos de primera clase. En F # - tipo de intercalación de sistema .NET (clases, interfaces, estructuras, subtipificación, sobrecargas de métodos), unidades de medida. Creo que la inferencia del tipo F # también está sesgada de izquierda a derecha para permitir una comprobación interactiva más eficiente, por lo tanto, es sorprendente que algún código necesite anotaciones.
En lo que respecta a la verificación de tipos y la inferencia, OCaml es más expresivo e intuitivo que F #. SML estaría más cerca que cualquiera de ellos de un HM de vainilla, pero SML también tiene algunas extensiones para algunos polimorfismos del operador y soporte de grabación.
Dado que el artículo del rasgo dice OCaml y F # ambos usan la inferencia tipo Damas-Milner, que pensé que era un algoritmo estándar, es decir, un algoritmo que no permite variaciones, ¿cómo se relacionan los dos rasgos?
El algoritmo de Damas-Milner (también conocido como Algoritmo W) se puede extender y, de hecho, todas las implementaciones prácticas de él han agregado muchas extensiones, incluyendo tanto OCaml como F #.
¿Es que Damas-Milner es la base sobre la cual se construyen ambos tipos de sistemas de inferencia, pero que cada uno modifica a Damas-Milner en base a la tipificación?
Exactamente sí. En particular, OCaml tiene una gran cantidad de extensiones experimentales diferentes para un núcleo Damas-Milner que incluye variantes polimórficas, objetos, módulos de primera clase. F # es más simple pero también tiene algunas extensiones que OCaml no tiene, sobre todo la sobrecarga (principalmente operadores).
No creo que haya documentos de resumen que describan los sistemas de tipos completos de OCaml o de F #. De hecho, no conozco un documento que describa el sistema actual de tipo F #. Para OCaml, tiene muchos documentos diferentes que cubren diferentes aspectos. Empezaría por las publicaciones de Jacques Garrigue y luego seguiría las referencias allí.