Une raison pour laquelle scala ne prend pas explicitement en charge les types dépendants?

Il existe des types dépendant des chemins et je pense qu'il est possible d'exprimer presque toutes les fonctionnalités de langages tels que Epigram ou Agda dans Scala, mais je me demande pourquoi Scala ne prend pas en charge cela plus explicitement comme il le fait très bien dans d'autres domaines (par exemple , DSL)? Quelque chose me manque comme "ce n'est pas nécessaire"?

Mis à part la commodité syntaxique, la combinaison de types singleton, de types dépendants du chemin et de valeurs implicites signifie que Scala a un support étonnamment bon pour le typage dépendant, comme j'ai essayé de le démontrer dans informe .

Le support intrinsèque de Scala pour les types dépendants se fait via les types dépendant du chemin . Celles-ci permettent à un type de dépendre d'un chemin de sélecteur à travers un graphique objet (c'est-à-dire valeur) comme ceci,

scala> class Foo { class Bar }
defined class Foo

scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658

scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757

scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>

scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
              implicitly[foo1.Bar =:= foo2.Bar]

À mon avis, ce qui précède devrait suffire à répondre à la question "Scala est-il un langage typé de manière dépendante?" dans le positif: il est clair que nous avons ici des types qui se distinguent par les valeurs qui sont leurs préfixes.

Cependant, on objecte souvent que Scala n'est pas un langage de type "entièrement" dépendant car il n'a pas de somme et de types de produit dépendants comme ceux trouvés dans Agda ou Coq ou Idris comme intrinsèques. Je pense que cela reflète dans une certaine mesure une fixation sur la forme sur les fondamentaux, néanmoins, je vais essayer de montrer que Scala est beaucoup plus proche de ces autres langues que ce qui est généralement admis.

Malgré la terminologie, les types de somme dépendants (également appelés types Sigma) sont simplement une paire de valeurs où le type de la deuxième valeur dépend de la première valeur. Ceci est directement représentable dans Scala,

scala> trait Sigma {
     |   val foo: Foo
     |   val bar: foo.Bar
     | }
defined trait Sigma

scala> val sigma = new Sigma {
     |   val foo = foo1
     |   val bar = new foo.Bar
     | }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

et en fait, c'est une partie cruciale de l' encodage des types de méthode dépendants qui est nécessaire pour échapper à la 'Bakery of Doom' dans Scala avant la version 2.10 (ou plus tôt via l'option du compilateur Scala expérimentale -Ydependent-method types).

Les types de produits dépendants (aka types Pi) sont essentiellement des fonctions allant des valeurs aux types. Ils sont essentiels à la représentation des vecteurs de taille statique et des autres enfants de l'affiche pour les langages de programmation typés de manière dépendante. Nous pouvons encoder des types Pi dans Scala en utilisant une combinaison de types dépendants du chemin, de types singleton et de paramètres implicites. On définit d'abord un trait qui va représenter une fonction d'une valeur de type T à un type U,

scala> trait Pi[T] { type U }
defined trait Pi

On peut que définir une méthode polymorphe qui utilise ce type,

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

(notez l'utilisation du type dépendant du chemin pi.Udans le type de résultat List[pi.U]). Étant donné une valeur de type T, cette fonction renverra une liste (n vide) de valeurs du type correspondant à cette valeur T particulière.

Définissons maintenant quelques valeurs appropriées et témoins implicites pour les relations fonctionnelles que nous voulons entretenir,

scala> object Foo
defined module Foo

scala> object Bar
defined module Bar

scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11

scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

Et maintenant, voici notre fonction utilisant le type Pi en action,

scala> depList(Foo)
res2: List[fooInt.U] = List()

scala> depList(Bar)
res3: List[barString.U] = List()

scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>

scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
              implicitly[res2.type <:< List[String]]
                    ^

scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>

scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
              implicitly[res3.type <:< List[Int]]

(notez que nous utilisons ici l' <:<opérateur témoin de sous-type de Scala plutôt que =:=parce que res2.typeet res3.typesont des types singleton et donc plus précis que les types que nous vérifions sur le RHS).

En pratique, cependant, dans Scala, nous ne commencerions pas par encoder les types Sigma et Pi pour ensuite procéder à partir de là comme nous le ferions dans Agda ou Idris. Au lieu de cela, nous utiliserions des types dépendant du chemin, des types singleton et des implicits directement. Vous pouvez trouver de nombreux exemples de la façon dont cela se joue dans l'informe: types de taille , enregistrements extensibles , HLists complètes , abandonnez votre passe-partout , Zippers génériques , etc. etc.

La seule objection restante que je peux voir est que dans le codage ci-dessus des types Pi, nous avons besoin que les types singleton des valeurs dépendantes soient exprimables. Malheureusement, dans Scala, cela n'est possible que pour les valeurs de types référence et non pour les valeurs de types non-référence (en particulier par exemple Int). C'est une honte, mais pas une difficulté intrinsèque: le vérificateur de type Scala représente les types singleton de valeurs non-référence en interne, et il y a eu quelques des expériences en les rendant directement exprimable. En pratique, nous pouvons contourner le problème avec un codage au niveau du type assez standard des nombres naturels .

Dans tous les cas, je ne pense pas que cette légère restriction de domaine puisse être utilisée comme une objection au statut de Scala en tant que langage typé de manière dépendante. Si c'est le cas, alors la même chose pourrait être dite pour le ML dépendant (qui n'autorise que les dépendances sur les valeurs des nombres naturels), ce qui serait une conclusion bizarre.

Je suppose que c'est parce que (comme je le sais par expérience, après avoir utilisé des types dépendants dans l'assistant de preuve Coq, qui les prend entièrement en charge mais toujours pas de manière très pratique) les types dépendants sont une fonctionnalité de langage de programmation très avancée qui est vraiment difficile à bien faire - et peut provoquer une explosion exponentielle de la complexité dans la pratique. Ils font toujours l'objet de recherches en informatique.

Je crois que les types dépendant du chemin de Scala ne peuvent représenter que des Σ-types, mais pas des Π-types. Ce:

trait Pi[T] { type U }

n'est pas exactement de type Π. Par définition, le type Π, ou produit dépendant, est une fonction dont le type de résultat dépend de la valeur de l'argument, représentant le quantificateur universel, c'est-à-dire ∀x: A, B (x). Dans le cas ci-dessus, cependant, cela dépend uniquement du type T, mais pas d'une valeur de ce type. Le trait Pi lui-même est un type Σ, un quantificateur existentiel, c'est-à-dire ∃x: A, B (x). L'auto-référence de l'objet dans ce cas agit comme une variable quantifiée. Lorsqu'il est passé en tant que paramètre implicite, cependant, il se réduit à une fonction de type ordinaire, car il est résolu par type. Le codage du produit dépendant dans Scala peut ressembler à ceci:

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U 

La pièce manquante ici est une capacité à contraindre statiquement le champ x à la valeur attendue t, formant effectivement une équation représentant la propriété de toutes les valeurs habitant le type T.Avec nos Σ-types, utilisés pour exprimer l'existence d'un objet avec une propriété donnée, le la logique se forme, dans laquelle notre équation est un théorème à prouver.

Sur une note latérale, dans le cas réel, le théorème peut être très non trivial, au point où il ne peut pas être automatiquement dérivé du code ou résolu sans effort significatif. On peut même formuler l'hypothèse de Riemann de cette façon, seulement pour trouver la signature impossible à implémenter sans la prouver, en boucle pour toujours ou en lançant une exception.

La question portait sur l'utilisation plus directe de la fonction de typage dépendant et, à mon avis, il y aurait un avantage à avoir une approche de typage dépendante plus directe que ce que propose Scala.
Les réponses actuelles tentent d'argumenter la question au niveau théorique de type. Je veux lui donner une tournure plus pragmatique. Cela peut expliquer pourquoi les gens sont divisés sur le niveau de prise en charge des types dépendants dans le langage Scala. Nous pouvons avoir des définitions quelque peu différentes à l'esprit. (pour ne pas dire que l'on a raison et que l'on a tort).

Ce n'est pas une tentative pour répondre à la question de savoir dans quelle mesure il serait facile de transformer Scala en quelque chose comme Idris (j'imagine très difficile) ou d'écrire une bibliothèque offrant un support plus direct pour les capacités Idris (comme les singletonstentatives d'être dans Haskell).

Au lieu de cela, je veux souligner la différence pragmatique entre Scala et un langage comme Idris.
Que sont les bits de code pour les expressions de niveau valeur et type? Idris utilise le même code, Scala utilise un code très différent.

Scala (similaire à Haskell) peut être capable d'encoder de nombreux calculs de niveau de type. Ceci est montré par des bibliothèques comme shapeless. Ces bibliothèques le font en utilisant des astuces vraiment impressionnantes et intelligentes. Cependant, leur code de niveau de type est (actuellement) assez différent des expressions de niveau valeur (je trouve que cet écart est un peu plus étroit dans Haskell). Idris permet d'utiliser l'expression de niveau de valeur au niveau de type EN L'ÉTAT.

L'avantage évident est la réutilisation du code (vous n'avez pas besoin de coder les expressions de niveau de type séparément du niveau de valeur si vous en avez besoin aux deux endroits). Il devrait être beaucoup plus facile d'écrire du code de niveau valeur. Il devrait être plus facile de ne pas avoir à faire face à des hacks comme les singletons (sans parler du coût de performance). Vous n'avez pas besoin d'apprendre deux choses, vous apprenez une chose. Sur un plan pragmatique, nous finissons par avoir besoin de moins de concepts. Saisissez des synonymes, des familles de types, des fonctions, ... que diriez-vous uniquement des fonctions? À mon avis, ces avantages unificateurs vont beaucoup plus loin et vont au-delà de la commodité syntaxique.

Considérez le code vérifié. Voir:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Le vérificateur de type vérifie les preuves des lois monadiques / fonctionnelles / applicatives et les preuves sont réelles implémentations de monade / foncteur / applicatif et non un équivalent de niveau de type codé qui peut être le même ou pas le même. La grande question est de savoir ce que nous prouvons?

La même chose peut me faire en utilisant des astuces d'encodage intelligentes (voir ce qui suit pour la version Haskell, je n'en ai pas vu pour Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https: // github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
sauf que les types sont si compliqués qu'il est difficile de voir les lois, les expressions de niveau de valeur sont converties (automatiquement mais toujours) en éléments de niveau de type et vous devez également faire confiance à cette conversion . Il y a place à l'erreur dans tout cela, ce qui défie en quelque sorte l'objectif du compilateur agissant en tant qu'assistant de preuve.

(EDITED 2018.8.10) En parlant d'aide à la preuve, voici une autre grande différence entre Idris et Scala. Il n'y a rien dans Scala (ou Haskell) qui puisse empêcher d'écrire des preuves divergentes:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

tandis qu'Idris a un totalmot clé empêchant la compilation de code comme celui-ci.

Une bibliothèque Scala qui essaie d'unifier le code de niveau de valeur et de type (comme Haskell singletons) serait un test intéressant pour la prise en charge par Scala des types dépendants. Une telle bibliothèque peut-elle être bien meilleure dans Scala en raison des types dépendant des chemins?

Je suis trop nouveau à Scala pour répondre moi-même à cette question.