Pourquoi ne pas être typé de manière dépendante?

J'ai vu plusieurs sources faire écho à l'opinion selon laquelle "Haskell est en train de devenir progressivement une langue typée de manière dépendante". L'implication semble être qu'avec de plus en plus d'extensions de langage, Haskell dérive dans cette direction générale, mais n'y est pas encore.

Il y a essentiellement deux choses que j'aimerais savoir. La première est, tout simplement, que signifie réellement «être une langue à typage dépendant» ? (Espérons sans être trop technique à ce sujet.)

La deuxième question est ... quel est l'inconvénient? Je veux dire, les gens savent que nous allons dans cette direction, donc il doit y avoir un avantage à cela. Et pourtant, nous n'en sommes pas encore là, il doit donc y avoir un inconvénient qui empêche les gens d'aller jusqu'au bout. J'ai l'impression que le problème est une forte augmentation de la complexité. Mais, ne comprenant pas vraiment ce qu'est le typage dépendant, je ne sais pas avec certitude.

Ce que je fais savoir est que chaque fois que je commence la lecture d'un langage de programmation dépendamment typé, le texte est tout à fait incompréhensible ... On peut supposer que c'est le problème. (?)

Le typage dépendant n'est en réalité que l'unification des niveaux de valeur et de type, vous pouvez donc paramétrer les valeurs sur les types (déjà possible avec les classes de types et le polymorphisme paramétrique dans Haskell) et vous pouvez paramétrer les types sur les valeurs (pas, à proprement parler, encore possible dans Haskell , bien DataKindsque très proche).

Edit: Apparemment, à partir de maintenant, je me suis trompé (voir le commentaire de @ pigworker). Je vais conserver le reste comme un enregistrement des mythes que j'ai nourris. : P

Le problème avec le passage au typage entièrement dépendant, d'après ce que j'ai entendu, est que cela briserait la restriction de phase entre les niveaux de type et de valeur qui permet à Haskell d'être compilé en un code machine efficace avec des types effacés. Avec notre niveau actuel de technologie, un langage typé de manière dépendante doit passer par un interpréteur à un moment donné (soit immédiatement, soit après avoir été compilé en bytecode de type dépendant ou similaire).

Ce n'est pas nécessairement une restriction fondamentale, mais je ne suis personnellement au courant d'aucune recherche actuelle qui semble prometteuse à cet égard, mais qui n'a pas déjà été intégrée au GHC. Si quelqu'un d'autre en sait plus, je serais heureux d'être corrigé.

Haskell typiquement dépendant, maintenant?

Haskell est, dans une petite mesure, un langage typé de manière dépendante. Il existe une notion de données au niveau du type, désormais plus judicieusement typées grâce à DataKinds, et il existe des moyens ( GADTs) pour donner une représentation à l'exécution aux données au niveau du type. Par conséquent, les valeurs des éléments d'exécution apparaissent effectivement dans les types , ce que signifie pour un langage d'être typé de manière dépendante.

Les types de données simples sont promus au niveau kind, afin que les valeurs qu'ils contiennent puissent être utilisées dans les types. D'où l'exemple archétypal

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
  VNil   :: Vec Z x
  VCons  :: x -> Vec n x -> Vec (S n) x

devient possible, et avec elle, des définitions telles que

vApply :: Vec n (s -> t) -> Vec n s -> Vec n t
vApply VNil         VNil         = VNil
vApply (VCons f fs) (VCons s ss) = VCons (f s) (vApply fs ss)

ce qui est sympa. Notez que la longueur nest une chose purement statique dans cette fonction, garantissant que les vecteurs d'entrée et de sortie ont la même longueur, même si cette longueur ne joue aucun rôle dans l'exécution de vApply. En revanche, il est beaucoup plus délicat (c'est-à-dire impossible) d'implémenter la fonction qui fait des ncopies d'unx ( ce qui serait pureà vApplyl » <*>)

vReplicate :: x -> Vec n x

car il est essentiel de savoir combien de copies effectuer au moment de l'exécution. Entrez les singletons.

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

Pour tout type promouvable, nous pouvons créer la famille singleton, indexée sur le type promu, habitée par des doublons d'exécution de ses valeurs. Natty nest le type de copies d'exécution du niveau type n :: Nat. Nous pouvons maintenant écrire

vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy     x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)

Vous avez donc une valeur au niveau du type attachée à une valeur au moment de l'exécution: l'inspection de la copie au moment de l'exécution affine la connaissance statique de la valeur au niveau du type. Même si les termes et les types sont séparés, nous pouvons travailler de manière dépendante en utilisant la construction singleton comme une sorte de résine époxy, créant des liaisons entre les phases. C'est loin d'autoriser des expressions d'exécution arbitraires dans les types, mais ce n'est rien.

Qu'est-ce qui est méchant? Qu'est-ce qui manque?

Mettons un peu de pression sur cette technologie et voyons ce qui commence à vaciller. Nous pourrions avoir l'idée que les singletons devraient être gérables un peu plus implicitement

class Nattily (n :: Nat) where
  natty :: Natty n
instance Nattily Z where
  natty = Zy
instance Nattily n => Nattily (S n) where
  natty = Sy natty

nous permettant d'écrire, disons,

instance Nattily n => Applicative (Vec n) where
  pure = vReplicate natty
  (<*>) = vApply

Cela fonctionne, mais cela signifie maintenant que notre Nattype d' origine a engendré trois copies: un genre, une famille singleton et une classe singleton. Nous avons un processus plutôt maladroit pour l'échange de Natty nvaleurs explicites et de Nattily ndictionnaires. De plus,Natty n'est pas le cas Nat: nous avons une sorte de dépendance sur les valeurs d'exécution, mais pas au type auquel nous avons pensé en premier. Aucun langage typé de manière totalement dépendante ne rend les types dépendants aussi compliqués!

Pendant ce temps, bien que Natpeut être promu, Vecne peut pas. Vous ne pouvez pas indexer par un type indexé. Plein de langues à typage dépendant n'imposent aucune telle restriction, et dans ma carrière de show-off typé de manière dépendante, j'ai appris à inclure des exemples d'indexation à deux couches dans mes discussions, juste pour enseigner aux gens qui ont fait une indexation à une couche difficile-mais-possible de ne pas s'attendre à ce que je plie comme un château de cartes. Quel est le problème? Égalité. Les GADT fonctionnent en traduisant les contraintes que vous obtenez implicitement lorsque vous donnez à un constructeur un type de retour spécifique en demandes équationnelles explicites. Comme ça.

data Vec (n :: Nat) (x :: *)
  = n ~ Z => VNil
  | forall m. n ~ S m => VCons x (Vec m x)

Dans chacune de nos deux équations, les deux côtés ont du genre Nat .

Maintenant, essayez la même traduction pour quelque chose d'indexé sur des vecteurs.

data InVec :: x -> Vec n x -> * where
  Here :: InVec z (VCons z zs)
  After :: InVec z ys -> InVec z (VCons y ys)

devient

data InVec (a :: x) (as :: Vec n x)
  = forall m z (zs :: Vec x m). (n ~ S m, as ~ VCons z zs) => Here
  | forall m y z (ys :: Vec x m). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)

et maintenant nous formons des contraintes équationnelles entre as :: Vec n x et VCons z zs :: Vec (S m) xoù les deux côtés ont des types syntaxiquement distincts (mais prouvés égaux). Le noyau GHC n'est actuellement pas équipé pour un tel concept!

Que manque-t-il d'autre? Eh bien, la plupart des Haskell sont absents du niveau de type. Le langage des termes que vous pouvez promouvoir n'a en fait que des variables et des constructeurs non GADT. Une fois que vous les avez, la type familymachinerie vous permet d'écrire des programmes au niveau du type: certains d'entre eux pourraient être tout à fait comme des fonctions que vous envisageriez d'écrire au niveau du terme (par exemple, équiper Natavec addition, afin que vous puissiez donner un bon type à ajouter pourVec ) , mais ce n'est qu'une coïncidence!

Une autre chose qui manque, dans la pratique, est une bibliothèque qui utilise nos nouvelles capacités pour indexer les types par valeurs. Que faire Functor et que Monaddevenir dans ce nouveau monde courageux? J'y pense, mais il reste encore beaucoup à faire.

Exécution de programmes au niveau du type

Haskell, comme la plupart des langages de programmation typés de manière dépendante, a deux sémantiques opérationnelles. Il y a la façon dont le système d'exécution exécute les programmes (expressions fermées uniquement, après l'effacement du type, hautement optimisé) et puis il y a la façon dont le vérificateur de type exécute les programmes (vos familles de types, votre "classe de type Prolog", avec des expressions ouvertes). Pour Haskell, vous ne mélangez généralement pas les deux, car les programmes en cours d'exécution sont dans des langues différentes. Les langages à typage dépendant ont des modèles d'exécution séparés et statiques pour le même langage de programmes, mais ne vous inquiétez pas, le modèle d'exécution vous permet toujours de faire l'effacement de type et, en fait, l'effacement de preuve: c'est ce que l' extraction de Coqmécanisme vous donne; c'est du moins ce que fait le compilateur d'Edwin Brady (bien qu'Edwin efface les valeurs dupliquées inutilement, ainsi que les types et les preuves). La distinction de phase n'est peut-être plus une distinction de catégorie syntaxique plus, mais c'est bien vivant.

Les langues à typage dépendant, étant totales, permettent au vérificateur de type d'exécuter des programmes sans craindre rien de pire qu'une longue attente. Au fur et à mesure que Haskell devient de plus en plus typé, nous sommes confrontés à la question de savoir quel devrait être son modèle d'exécution statique? Une approche pourrait être de restreindre l'exécution statique aux fonctions totales, ce qui nous donnerait la même liberté d'exécution, mais pourrait nous forcer à faire des distinctions (au moins pour le code au niveau du type) entre les données et les codata, afin que nous puissions dire s'il faut appliquer la résiliation ou la productivité. Mais ce n'est pas la seule approche. Nous sommes libres de choisir un modèle d'exécution beaucoup plus faible qui hésite à exécuter des programmes, au prix de faire sortir moins d'équations rien que par le calcul. Et en fait, c'est ce que fait réellement GHC. Les règles de typage pour GHC core ne mentionnent pas exécution programmes, mais uniquement pour vérifier les preuves d'équations. Lors de la traduction vers le noyau, le solveur de contraintes de GHC essaie d'exécuter vos programmes au niveau du type, générant une petite trace argentée de preuves qu'une expression donnée équivaut à sa forme normale. Cette méthode de génération de preuves est un peu imprévisible et inévitablement incomplète: elle combat les récursions effrayantes, par exemple, et c'est probablement sage. Une chose dont nous n'avons pas à nous soucier est l'exécution des IO calculs dans le vérificateur de type: rappelez-vous que le vérificateur de type n'a pas à donner launchMissilesla même signification que le système d'exécution!

Culture Hindley-Milner

Le système de type Hindley-Milner réalise la coïncidence vraiment impressionnante de quatre distinctions distinctes, avec le malheureux effet secondaire culturel que beaucoup de gens ne peuvent pas voir la distinction entre les distinctions et supposent que la coïncidence est inévitable! De quoi je parle?

• termes vs types
• choses écrites explicitement vs choses écrites implicitement
• présence à l'exécution vs effacement avant l'exécution
• abstraction non dépendante vs quantification dépendante

Nous sommes habitués à écrire des termes et à laisser des types à inférer ... puis à effacer. Nous sommes habitués à quantifier des variables de type avec l'abstraction de type correspondante et l'application se déroulant de manière silencieuse et statique.

Vous n'avez pas à vous éloigner trop de la vanille Hindley-Milner avant que ces distinctions ne soient désalignées, et ce n'est pas une mauvaise chose . Pour commencer, nous pouvons avoir des types plus intéressants si nous sommes prêts à les écrire à quelques endroits. En attendant, nous n'avons pas besoin d'écrire des dictionnaires de classe de type lorsque nous utilisons des fonctions surchargées, mais ces dictionnaires sont certainement présents (ou intégrés) au moment de l'exécution. Dans les langages typés de façon dépendante, nous prévoyons d'effacer plus que de simples types au moment de l'exécution, mais (comme avec les classes de types) que certaines valeurs implicitement inférées ne seront pas effacées. Par exemple, vReplicatel'argument numérique de est souvent déductible du type du vecteur souhaité, mais nous avons encore besoin de le connaître au moment de l'exécution.

Quels choix de conception de langage devrions-nous examiner parce que ces coïncidences ne tiennent plus? Par exemple, est-il exact que Haskell ne fournit aucun moyen d'instancier un forall x. tquantificateur explicitement? Si le vérificateur de type ne peut pas deviner xen unifiant t, nous n'avons pas d'autre moyen de dire ce qui xdoit être.

Plus largement, nous ne pouvons pas traiter "l'inférence de type" comme un concept monolithique dont nous avons tout ou rien. Pour commencer, nous devons séparer l'aspect "généralisation" (la règle "let" de Milner), qui repose fortement sur la restriction des types existants pour s'assurer qu'une machine stupide puisse en deviner un, de l'aspect "spécialisation" (le "var" de Milner "rule) qui est aussi efficace que votre solveur de contraintes. On peut s'attendre à ce que les types de premier niveau deviennent plus difficiles à déduire, mais que les informations de type interne resteront assez faciles à propager.

Prochaines étapes pour Haskell

Nous voyons les niveaux de type et de genre devenir très similaires (et ils partagent déjà une représentation interne dans GHC). Nous pourrions tout aussi bien les fusionner. Ce serait amusant à prendre * :: *si nous le pouvons: nous avons perdu la solidité logique il y a longtemps, lorsque nous avons permis le fond, mais la solidité du type est généralement une exigence plus faible. Il faut vérifier. Si nous devons avoir des niveaux de type, de genre, etc. distincts, nous pouvons au moins nous assurer que tout au niveau de type et au-dessus peut toujours être promu. Ce serait bien de simplement réutiliser le polymorphisme que nous avons déjà pour les types, plutôt que de réinventer le polymorphisme au niveau du genre.

Nous devrions simplifier et généraliser le système actuel de contraintes en autorisant des équations hétérogènesa ~ b où les types de aet bne sont pas syntaxiquement identiques (mais peuvent être prouvés égaux). C'est une technique ancienne (dans ma thèse, au siècle dernier) qui rend la dépendance beaucoup plus facile à gérer. Nous pourrions exprimer des contraintes sur les expressions dans les GADT, et ainsi assouplir les restrictions sur ce qui peut être promu.

Nous devons éliminer la nécessité de la construction singleton en introduisant un type de fonction dépendant, pi x :: s -> t. Une fonction avec un tel type pourrait être appliquée explicitement à toute expression de type squi vit à l' intersection des langages de type et de terme (donc, variables, constructeurs, avec d'autres à venir plus tard). Le lambda et l'application correspondants ne seraient pas effacés au moment de l'exécution, nous pourrions donc écrire

vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z     x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)

sans remplacer Natpar Natty. Le domaine de pipeut être de n'importe quel type pouvant être promu, donc si les GADT peuvent être promus, nous pouvons écrire des séquences de quantificateur dépendantes (ou "télescopes" comme les appelait de Briuijn)

pi n :: Nat -> pi xs :: Vec n x -> ...

quelle que soit la longueur dont nous avons besoin.

Le but de ces étapes est d' éliminer la complexité en travaillant directement avec des outils plus généraux, au lieu de se contenter d'outils faibles et d'encodages maladroits. L'adhésion partielle actuelle rend les avantages des types dépendants de Haskell plus chers qu'ils ne devraient l'être.

Trop dur?

Les types dépendants rendent beaucoup de gens nerveux. Ils me rendent nerveux, mais j'aime être nerveux, ou du moins j'ai du mal à ne pas être nerveux de toute façon. Mais cela n'aide pas qu'il y ait un tel brouillard d'ignorance autour du sujet. Cela est dû en partie au fait que nous avons tous encore beaucoup à apprendre. Mais les partisans d'approches moins radicales sont connus pour attiser la peur des types dépendants sans toujours s'assurer que les faits sont entièrement avec eux. Je ne nommerai pas de noms. Ces mythes de «vérification de type indécidable», «Turing incomplet», «pas de distinction de phase», «pas d'effacement de type», «preuves partout», etc., persistent, même s'ils sont des bêtises.

Ce n'est certainement pas le cas que les programmes typés de manière dépendante doivent toujours être prouvés corrects. On peut améliorer l'hygiène de base de ses programmes, en imposant des invariants supplémentaires dans les types sans aller jusqu'à une spécification complète. De petits pas dans cette direction aboutissent souvent à des garanties beaucoup plus solides avec peu ou pas d'obligations de preuve supplémentaires. Il n'est pas vrai que les programmes typés de manière dépendante soient inévitablement pleins de preuves, en effet je prends généralement la présence de toutes les preuves dans mon code comme le signal pour remettre en question mes définitions .

Car, comme pour tout accroissement de l'articulation, nous devenons libres de dire de nouvelles choses immondes et justes. Par exemple, il existe de nombreuses façons minables de définir les arbres de recherche binaires, mais cela ne signifie pas qu'il n'y a pas de bonne façon . Il est important de ne pas présumer que les mauvaises expériences ne peuvent pas être améliorées, même si cela heurte l'ego de l'admettre. La conception de définitions dépendantes est une nouvelle compétence qui demande de l'apprentissage, et être un programmeur Haskell ne fait pas automatiquement de vous un expert! Et même si certains programmes sont mauvais, pourquoi refuseriez-vous à d'autres la liberté d'être juste?

Pourquoi toujours s'embêter avec Haskell?

J'apprécie vraiment les types dépendants, mais la plupart de mes projets de piratage sont toujours en Haskell. Pourquoi? Haskell a des classes de types. Haskell a des bibliothèques utiles. Haskell a un traitement pratique (bien que loin d'être idéal) de la programmation avec effets. Haskell dispose d'un compilateur de puissance industrielle. Les langages dépendamment typés sont à un stade beaucoup plus précoce dans la croissance de la communauté et de l'infrastructure, mais nous y arriverons, avec un réel changement de génération dans ce qui est possible, par exemple, au moyen de la métaprogrammation et des génériques de types de données. Mais il vous suffit de regarder autour de vous ce que font les gens à la suite des étapes de Haskell vers les types dépendants pour voir qu'il y a beaucoup d'avantages à gagner en poussant également la génération actuelle de langues vers l'avant.

John, c'est une autre idée fausse courante sur les types dépendants: ils ne fonctionnent pas lorsque les données ne sont disponibles qu'au moment de l'exécution. Voici comment vous pouvez faire l'exemple getLine:

data Some :: (k -> *) -> * where
  Like :: p x -> Some p

fromInt :: Int -> Some Natty
fromInt 0 = Like Zy
fromInt n = case fromInt (n - 1) of
  Like n -> Like (Sy n)

withZeroes :: (forall n. Vec n Int -> IO a) -> IO a
withZeroes k = do
  Like n <- fmap (fromInt . read) getLine
  k (vReplicate n 0)

*Main> withZeroes print
5
VCons 0 (VCons 0 (VCons 0 (VCons 0 (VCons 0 VNil))))

Edit: Hm, c'était censé être un commentaire à la réponse du pigworker. J'échoue clairement à SO.

pigworker donne une excellente discussion sur les raisons pour lesquelles nous devrions nous diriger vers les types dépendants: (a) ils sont géniaux; (b) ils simplifieraient en fait beaucoup de ce que fait déjà Haskell.

Quant au "pourquoi pas?" question, il y a quelques points que je pense. Le premier point est que si la notion de base derrière les types dépendants est facile (permettre aux types de dépendre des valeurs), les ramifications de cette notion de base sont à la fois subtiles et profondes. Par exemple, la distinction entre les valeurs et les types est toujours bien vivante; mais discuter de la différence entre eux devient loinplus nuancé que dans votre Hindley - Milner ou System F. Dans une certaine mesure, cela est dû au fait que les types dépendants sont fondamentalement difficiles (par exemple, la logique du premier ordre est indécidable). Mais je pense que le plus gros problème est vraiment que nous manquons d'un bon vocabulaire pour capturer et expliquer ce qui se passe. Au fur et à mesure que de plus en plus de personnes en apprendront davantage sur les types dépendants, nous développerons un meilleur vocabulaire et ainsi les choses deviendront plus faciles à comprendre, même si les problèmes sous-jacents sont toujours difficiles.

Le deuxième point a à voir avec le fait que Haskell granditvers les types dépendants. Parce que nous progressons progressivement vers cet objectif, mais sans y parvenir, nous sommes coincés avec un langage qui a des correctifs incrémentiels en plus des correctifs incrémentiels. Le même genre de chose s'est produit dans d'autres langues à mesure que de nouvelles idées sont devenues populaires. Java n'avait pas l'habitude d'avoir un polymorphisme (paramétrique); et quand ils l'ont finalement ajouté, c'était évidemment une amélioration progressive avec quelques fuites d'abstraction et une puissance paralysée. Il s'avère que mélanger le sous-typage et le polymorphisme est intrinsèquement difficile; mais ce n'est pas la raison pour laquelle Java Generics fonctionne comme ils le font. Ils fonctionnent comme ils le font en raison de la contrainte d'être une amélioration incrémentielle des anciennes versions de Java. Idem, pour plus loin dans le temps où la POO a été inventée et où les gens ont commencé à écrire "objectif" C (à ne pas confondre avec Objective-C), etc. Rappelez-vous, C ++ a commencé sous le prétexte d'être un sur-ensemble strict de C. L'ajout de nouveaux paradigmes nécessite toujours de redéfinir le langage, ou bien de se retrouver avec un désordre compliqué. Ce que je veux dire dans tout cela, c'est que l'ajout de vrais types dépendants à Haskell va nécessiter une certaine quantité d'éviscération et de restructuration du langage - si nous voulons bien faire les choses. Mais il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. C ++ a commencé sous le prétexte d'être un sur-ensemble strict de C. L'ajout de nouveaux paradigmes nécessite toujours de définir à nouveau le langage, ou bien de se retrouver avec un désordre compliqué. Ce que je veux dire dans tout cela, c'est que l'ajout de vrais types dépendants à Haskell va nécessiter une certaine quantité d'éviscération et de restructuration du langage - si nous voulons bien faire les choses. Mais il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. C ++ a commencé sous le prétexte d'être un sur-ensemble strict de C. L'ajout de nouveaux paradigmes nécessite toujours de définir à nouveau le langage, ou bien de se retrouver avec un désordre compliqué. Ce que je veux dire dans tout cela, c'est que l'ajout de vrais types dépendants à Haskell va nécessiter une certaine quantité d'éviscération et de restructuration du langage - si nous voulons bien faire les choses. Mais il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. ou bien finir avec un désordre compliqué. Ce que je veux dire dans tout cela, c'est que l'ajout de vrais types dépendants à Haskell va nécessiter une certaine quantité d'éviscération et de restructuration du langage - si nous voulons bien faire les choses. Mais il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. ou bien finir avec un désordre compliqué. Ce que je veux dire dans tout cela, c'est que l'ajout de véritables types dépendants à Haskell va nécessiter une certaine quantité d'éviscération et de restructuration du langage - si nous voulons le faire correctement. Mais il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. Il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc. Il est vraiment difficile de s'engager dans ce genre de révision, alors que les progrès progressifs que nous avons accomplis semblent moins chers à court terme. Vraiment, il n'y a pas beaucoup de gens qui piratent GHC, mais il y a une bonne quantité de code hérité à garder en vie. C'est en partie la raison pour laquelle il existe tant de langages dérivés comme DDC, Cayenne, Idris, etc.