Le système de typage de Scala est complet. Preuve? Exemple? Avantages?

Il y a des affirmations selon lesquelles le système de type Scala est complet. Mes questions sont:

  1. Y a-t-il une preuve formelle à cela?

  2. À quoi ressemblerait un simple calcul dans le système de type Scala?

  3. Est-ce un avantage pour Scala – la langue? Est-ce que cela rend Scala plus “puissante” en quelque sorte comparée à des langues sans un système de type complet Turing?

Je suppose que cela s’applique aux langues et aux systèmes de caractères en général.

Il y a un article de blog quelque part avec une implémentation au niveau du type du calculateur de combinaison SKI, connue pour être Turing-complete.

Les systèmes de type Turing-complete ont fondamentalement les mêmes avantages et inconvénients que les langages complets de Turing: vous pouvez faire n’importe quoi, mais vous pouvez prouver très peu. En particulier, vous ne pouvez pas prouver que vous finirez par faire quelque chose.

Un exemple de calcul au niveau du type est celui des nouveaux transformateurs de collection préservant la qualité de Scala 2.8. Dans Scala 2.8, les méthodes comme map , filter , etc. renvoient une collection du même type qu’elles ont été appelées. Donc, si vous filter un Set[Int] , vous récupérez un Set[Int] et si vous map une List[Ssortingng] vous recevez une List[Whatever the return type of the anonymous function is] .

Maintenant, comme vous pouvez le voir, la map peut réellement transformer le type d’élément. Alors, que se passe-t-il si le nouveau type d’élément ne peut pas être représenté avec le type de collection d’origine? Exemple: un BitSet ne peut contenir que des entiers à largeur fixe. Alors, que se passe-t-il si vous avez un BitSet[Short] et que vous BitSet[Short] chaque numéro à sa représentation sous forme de chaîne?

 someBitSet map { _.toSsortingng() } 

Le résultat serait un BitSet[Ssortingng] , mais c’est impossible. Scala choisit donc le supertype le plus dérivé de BitSet , qui peut contenir une Ssortingng , dans ce cas, un Set[Ssortingng] .

Tout ce calcul se déroule pendant la compilation , ou plus précisément lors de la vérification du type , en utilisant des fonctions de type. Ainsi, il est garanti statiquement qu’il est sécurisé, même si les types sont en réalité calculés et donc inconnus au moment de la conception.

Mon article sur l’encodage du calcul SKI dans le système de type Scala montre la complétude de Turing.

Pour certains calculs simples au niveau du type, il existe également des exemples sur la façon d’encoder les nombres naturels et l’addition / multiplication .

Enfin, il y a une grande série d’articles sur la programmation au niveau du type sur le blog d’Apocalisp.