pigworker donne une excellente discussion des raisons pour lesquelles nous devrions être dirigés vers des types dépendants: (a) ils sont super; (b) ils seraient en fait de simplifier beaucoup de ce que Haskell déjà fait.
Comme pour le "pourquoi pas?", il y a un couple de points je pense. Le premier point est que, bien que l'idée de base derrière types de charge est facile (autoriser les types reposent sur des valeurs), les ramifications de cette notion fondamentale sont à la fois subtile et profonde. Par exemple, la distinction entre les valeurs et les types est toujours vivant et bien; mais de discuter de la différence entre eux devient beaucoup plus nuancée que dans yer Hindley--Milner ou Système F. dans une certaine mesure, cela est dû au fait que les types de charge sont fondamentalement dur (par exemple, la logique du premier ordre est indécidable). Mais je pense que le plus gros problème c'est vraiment ce qu'il nous manque un bon vocabulaire pour la capture et expliquer ce qui se passe. Comme de plus en plus de gens apprennent à propos des types dépendants, nous allons développer un meilleur vocabulaire et donc, les choses deviendront plus faciles à comprendre, même si les problèmes sous-jacents sont encore mal.
Le deuxième point a à voir avec le fait que Haskell est croissante vers des types dépendants. Parce que nous faisons réaliser des progrès vers cet objectif, mais sans faire réellement de là, nous sommes coincés avec une langue qui a différentiels des taches sur le dessus de l'accroissement des patchs. Le même genre de chose s'est passé dans d'autres langues que de nouvelles idées, est devenu populaire. Java n'utilisez pas d'avoir (paramétrique) polymorphisme; et quand ils ont enfin ajouté, il était de toute évidence une amélioration progressive avec un peu d'abstraction fuites et les infirmes de la puissance. S'avère, mélange de sous-typage et polymorphisme est par nature difficile; mais ce n'est pas la raison pourquoi Java Génériques fonctionnent de la manière dont ils le font. Ils fonctionnent de la manière dont ils le font en raison de la contrainte à une amélioration progressive dans les anciennes versions de Java. Idem, pour de plus amples retour dans la journée quand la programmation orientée objet a été inventé et les gens ont commencé l'écriture de "l'objectif" C (à ne pas confondre avec Objective-C), etc. Rappelez-vous, C++ qui a commencé sous le couvert d'être un sur-ensemble strict de C. l'Ajout de nouveaux paradigmes toujours exige de définir la langue à nouveau, ou bien de se retrouver avec quelques bazar compliqué. Mon point dans tout cela est que, en ajoutant vrai des types dépendants à Haskell, aura besoin d'une certaine quantité de l'éviscération et la restructuration de la langue--- si nous allons le faire à droite. Mais il est vraiment difficile de s'engager à ce genre de remaniement, alors que l'augmentation progrès que nous avons fait semble moins cher à court terme. Vraiment, il n'y a pas beaucoup de gens qui hack sur GHC, mais il y a une bonne quantité de code hérité de le garder vivant. C'est en partie la raison pour laquelle il ya tellement de nombreux spin-off langues comme le DDC, le poivre de Cayenne, l'Idris, etc.
