Pourquoi l'inférence de type de F# est-elle si inconstante ?

Question

Le compilateur F# semble effectuer l'inférence de type d'une manière (assez) stricte de haut en bas et de gauche à droite. Cela signifie que vous devez faire des choses comme mettre toutes les définitions avant leur utilisation, l'ordre de compilation des fichiers est significatif, et vous avez tendance à avoir besoin de réarranger les choses (par l'intermédiaire de |> ou ce que vous voulez) pour éviter d'avoir des annotations de type explicites.

Est-il difficile de rendre ce système plus flexible et cela est-il prévu pour une future version de F# ? Il est évident que cela peut être fait, puisque Haskell (par exemple) n'a pas de telles limitations avec une inférence aussi puissante. Y a-t-il quelque chose d'intrinsèquement différent dans la conception ou l'idéologie de F# qui cause ce problème ?

Answer 1

Y a-t-il quelque chose d'intrinsèquement différent dans la conception ou l'idéologie de F# qui en est la cause ?

Oui. F# utilise le typage nominal plutôt que structurel parce qu'il est plus simple et, par conséquent, plus facile à utiliser pour les simples mortels.

Considérez cet exemple F# :

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

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

La première ne compile pas car le type de l'élément xs à l'intérieur de la fonction anonyme ne peut pas être déduite parce que F# ne peut pas exprimer le type "une classe avec une fonction anonyme". Length membre".

En revanche, OCaml peut exprimer l'équivalent direct :

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

car OCaml peut exprimer ce type (il est écrit <length: 'a ..> ). Notez que cela nécessite une inférence de type plus puissante que celle dont disposent actuellement F# ou Haskell, par exemple, OCaml peut inférer des types de somme.

Cependant, cette fonctionnalité est connue pour être un problème d'utilisation. Par exemple, si vous faites une erreur ailleurs dans le code, le compilateur n'a pas encore déduit que le type de l'élément xs était censé être un tableau, donc tout message d'erreur qu'il peut donner ne peut fournir que des informations comme "un type avec un membre Length" et non "un tableau". Avec un code à peine plus compliqué, cela devient rapidement incontrôlable car vous avez des types massifs avec de nombreux membres structurellement inférés qui ne sont pas tout à fait unifiés, ce qui conduit à des messages d'erreur incompréhensibles (de type C++/STL).

Answer 2

En ce qui concerne "l'inférence tout aussi puissante de Haskell", je ne pense pas que Haskell doive s'occuper de

• sous-typage dynamique de type OO (les classes de type peuvent faire des choses similaires, mais les classes de type sont plus faciles à typer/inférer)
• surcharge des méthodes (les classes de type peuvent faire des choses similaires, mais les classes de type sont plus faciles à typer/inférer)

C'est-à-dire que je pense que F# doit faire face à des choses difficiles que Haskell ne fait pas. (Presque certainement, Haskell doit faire face à des choses difficiles que F# ne fait pas).

Comme l'ont mentionné d'autres réponses, la plupart des principaux langages .NET sont influencés par l'outillage de Visual Studio (voir par exemple comment LINQ a "from ... select" plutôt que le "select ... from" de SQL, motivé par l'obtention de l'intellisense d'un préfixe de programme). L'intellisense, les gribouillis d'erreurs et la compréhensibilité des messages d'erreur sont autant de facteurs d'outillage qui influencent la conception de F#.

Il est peut-être possible de faire mieux et d'inférer davantage (sans sacrifier d'autres expériences), mais je ne pense pas que cela fasse partie de nos priorités pour les futures versions du langage. (Les Haskellers peuvent considérer que l'inférence de type F# est quelque peu faible, mais ils sont probablement moins nombreux que les C#ers qui considèrent l'inférence de type F# comme très forte. :) )

Il pourrait également être difficile d'étendre l'inférence de type d'une manière non cassante ; il est acceptable de changer les programmes illégaux en programmes légaux dans une version future, mais vous devez faire très attention à ce que les programmes précédemment légaux ne changent pas de sémantique sous les nouvelles règles d'inférence, et la résolution de noms (un affreux cauchemar dans chaque langage) est susceptible d'interagir avec les changements d'inférence de type de manière surprenante.

Answer 3

Je pense que l'algorithme utilisé par F# présente l'avantage d'être facile à expliquer (au moins grossièrement), de sorte qu'une fois que vous l'avez compris, vous pouvez avoir quelques attentes quant au résultat.

L'algorithme aura toujours certaines limites. Actuellement, il est assez facile de les comprendre. Pour un algorithme plus compliqué, cela pourrait être difficile. Par exemple, je pense que vous pourriez rencontrer des situations où vous pensez que l'algorithme devrait être capable de déduire quelque chose - mais s'il était suffisamment général pour couvrir le cas, il serait indécidable (par exemple, il pourrait continuer à tourner en boucle).

Une autre réflexion à ce sujet est que vérifier le code du haut vers le bas correspond à la façon dont nous lisons le code (du moins parfois ). Donc, peut-être le fait que nous ayons tendance à écrire le code de manière à permettre l'inférence de type rend également le code plus lisible pour les gens...

Answer 4

F# utilise une compilation en une seule passe, de sorte que vous ne pouvez référencer que des types ou fonctions qui ont été définis définis soit plus tôt dans le fichier dans lequel vous fichier dans lequel vous vous trouvez, soit dans un fichier est spécifié plus tôt dans la directive ordre de compilation.

J'ai récemment demandé à Don Syme comment faire plusieurs passages de sources pour améliorer le processus d'inférence de type. Sa réponse a été la suivante "Oui, il est possible de faire une inférence de type d'inférence de type. Il existe également variations à passage unique qui génèrent un ensemble fini de contraintes.

Cependant, ces approches ont tendance à donner de mauvais messages d'erreur et de mauvais résultats intellisense dans une éditeur visuel".

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

Answer 5

En bref, F# est basé sur la tradition de SML et d'OCaml, tandis que Haskell vient d'un monde légèrement différent de Miranda, Gofer et autres. Les différences de tradition historique sont subtiles, mais omniprésentes. Cette distinction se retrouve également dans d'autres langages modernes, comme le Coq, proche de ML, qui a les mêmes restrictions d'ordre que l'Agda, proche de Haskell, qui ne les a pas.

Cette différence est liée à l'évaluation paresseuse ou stricte. Le côté Haskell de l'univers croit en la paresse, et une fois que vous croyez déjà en la paresse, l'idée d'ajouter la paresse à des choses comme l'inférence de type est une évidence. Alors que dans la partie ML de l'univers, chaque fois que la paresse ou la récursion mutuelle est nécessaire, elle doit être explicitement notée par l'utilisation de mots-clés tels que avec , y , rec etc. Je préfère l'approche Haskell parce qu'elle donne lieu à moins de code passe-partout, mais il y a beaucoup de gens qui pensent qu'il vaut mieux rendre ces choses explicites.