Y a-t-il une raison pour laquelle Scala ne supporte pas explicitement les types dépendants ?

Question

Il existe des types dépendants du chemin et je pense qu'il est possible d'exprimer presque toutes les caractéristiques de langages tels qu'Epigram ou Agda en Scala, mais je me demande pourquoi Scala ne supporte pas ce plus explicitement comme il le fait très bien dans d'autres domaines (par exemple, les DSL) ? Quelque chose qui m'échappe, comme "ce n'est pas nécessaire" ?

Answer 1

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

Le support intrinsèque de Scala pour les types dépendants se fait par le biais de types dépendants du chemin . Ils permettent à un type de dépendre d'un chemin de sélection à travers un graphe d'objets (c'est-à-dire de valeurs) comme suit,

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 positivement à la question "Scala est-il un langage typé de manière dépendante ?": 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 dépendant "complet" parce qu'il ne dispose pas de somme dépendante et types de produits comme on en trouve dans Agda ou Coq ou Idris comme intrinsèques. Je pense que cela reflète dans une certaine mesure une fixation sur la forme plutôt que sur les fondamentaux, néanmoins, je vais essayer de montrer que Scala est beaucoup plus proche de ces autres langages que ce qui est généralement reconnu.

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. Ceci est directement représentable en 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, il s'agit d'une partie cruciale de la l'encodage des types de méthodes dépendantes qui est nécessaire pour échapper à la "boulangerie du destin". dans Scala avant la version 2.10 (ou avant via l'option de compilation Scala expérimentale -Ydependent-method types).

Les types de produits dépendants (alias types Pi) sont essentiellement des fonctions de valeurs à types. Ils sont essentiels à la représentation des vecteurs statiquement dimensionnés et les autres enfants-vedettes des langages de programmation typés de manière dépendante. Nous pouvons encoder les types Pi en Scala en utilisant une combinaison de types dépendants du chemin, de types singleton et de paramètres implicites. Tout d'abord, nous définissons un trait qui va représenter une fonction d'une valeur de type T vers un type U,

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

Nous pouvons ensuite 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 d'accès pi.U dans le type de résultat List[pi.U] ). Étant donné une valeur de type T, cette fonction renvoie une liste (n vide) de valeurs de type correspondant à cette valeur T particulière.

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

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 d'utilisation du 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 qu'ici, nous utilisons l'option <:< opérateur de sous-type-témoin plutôt que =:= parce que res2.type et res3.type sont des types singuliers et donc plus précis que les types que nous vérifions sur la droite).

En pratique, cependant, en Scala, nous ne commencerions pas par coder les types Sigma et Pi pour ensuite procéder à partir de là comme nous le ferions en Agda ou Idris. Nous utiliserions plutôt directement les types dépendants du chemin, les types singleton et les implicites. Vous pouvez trouver de nombreux exemples de la façon dont cela se passe dans shapeless : types dimensionnés , enregistrements extensibles , listes complètes de HL , supprimez votre modèle standard , Fermetures à glissière génériques etc. etc.

La seule objection restante que je vois est que dans l'encodage des types Pi ci-dessus, nous avons besoin que les types singleton des valeurs dépendantes soient exprimables. Malheureusement, en Scala, cela n'est possible que pour les valeurs de types de référence et non pour les valeurs de types non-référence (par exemple, Int). C'est dommage, mais ce n'est pas une difficulté intrinsèque : Le vérificateur de type de Scala représente les types singletons des valeurs de non-référence en interne, et il y a eu un certain nombre de cas où le vérificateur de type de Scala n'a pas été en mesure d'exprimer les valeurs de référence. couple de expériences en les rendant directement exprimables. Dans la pratique, nous pouvons contourner le problème avec un encodage assez standard au niveau du type 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é dépendant. Si c'est le cas, alors on pourrait dire la même chose de Dependent ML (qui n'autorise les dépendances que sur les valeurs des nombres naturels), ce qui serait une conclusion bizarre.

Answer 2

Je suppose que c'est parce que (comme je le sais d'expérience, ayant utilisé les types dépendants dans l'assistant de preuve Coq, qui les supporte entièrement mais pas encore de manière très pratique) les types dépendants sont une fonctionnalité très avancée du langage de programmation qui est vraiment difficile à mettre en place - et peut causer une explosion exponentielle de la complexité dans la pratique. Ils sont toujours un sujet de recherche en informatique.

Answer 3

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

trait Pi[T] { type U }

n'est pas exactement un Π-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, il ne dépend que du type T, mais pas d'une valeur quelconque de ce type. Le trait Pi lui-même est un type Σ, un quantificateur existentiel, c'est-à-dire ∃x : A, B(x). L'autoréférence de l'objet dans ce cas agit comme une variable quantifiée. Lorsqu'elle est passée en paramètre implicite, cependant, elle se réduit à une fonction de type ordinaire, puisqu'elle est résolue en fonction du type. Le codage du produit dépendant en Scala peut ressembler à ce qui suit :

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 la capacité de 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, la logique est formée, dans laquelle notre équation est un théorème à prouver.

Par ailleurs, dans un cas réel, le théorème peut être hautement non trivial, à tel point qu'il ne peut pas être automatiquement dérivé du code ou résolu sans un effort significatif. On peut même formuler l'Hypothèse de Riemann de cette manière, pour se rendre compte que la signature est impossible à mettre en œuvre sans la prouver réellement, en bouclant indéfiniment ou en levant une exception.

Answer 4

La question portait sur l'utilisation plus directe de la fonction typée dépendante et, à mon avis, il y aurait un avantage à avoir une approche de typage dépendant plus directe que ce que Scala offre.
Les réponses actuelles tentent d'argumenter la question sur un niveau théorique de type. Je veux donner une tournure plus pragmatique à la question. Cela peut expliquer pourquoi les gens sont divisés sur le niveau de support des types dépendants dans le langage Scala. Nous avons peut-être des définitions quelque peu différentes à l'esprit. (sans vouloir dire que l'un a raison et l'autre tort).

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

Je veux plutôt souligner la différence pragmatique entre Scala et un langage comme Idris.
Quels 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 (tout comme Haskell) peut être capable d'encoder de nombreux calculs au niveau du type. C'est ce que montrent des bibliothèques comme shapeless . Ces bibliothèques le font en utilisant des astuces vraiment impressionnantes et intelligentes. Cependant, leur code au niveau des types est (actuellement) assez différent des expressions au niveau des valeurs (je trouve que l'écart est un peu plus étroit en Haskell). Idris permet d'utiliser les expressions de niveau valeur au niveau du type AS IS.

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 des valeurs si vous en avez besoin aux deux endroits). Il devrait être beaucoup plus facile de d'écrire du code au niveau des valeurs. Il devrait être plus facile de ne pas avoir à gérer des bidouillages comme les singletons (sans parler du coût en termes de performances). Vous n'avez pas besoin d'apprendre deux choses, vous n'en apprenez qu'une. D'un point de vue pragmatique, nous finissons par avoir besoin de moins de concepts. Les synonymes de type, les familles de types, les fonctions, ... et pourquoi pas simplement les fonctions ? À mon avis, ces avantages unificateurs sont beaucoup plus profonds et vont au-delà de la commodité syntaxique.

Tenez compte du 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/foncteurs/applicatives et les preuves concernent des implémentations réelles de monade/functeur/applicatif et non un équivalent codé au niveau du type. équivalent au niveau du type qui peut être identique ou non. La grande question est de savoir ce que nous prouvons.

La même chose peut être faite en utilisant des astuces d'encodage (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, la valeur valeur sont converties (automatiquement mais quand même) en choses de niveau type et vous devez vous devez également faire confiance à cette conversion. Il y a de la place pour l'erreur dans tout cela, ce qui va à l'encontre de l'objectif du compilateur en tant qu'assistant de preuve. un assistant de preuve.

(EDITION 2018.8.10) En parlant d'aide à la preuve, voici une autre grande différence entre Idris et Scala. Il n'y a rien en Scala (ou en 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 total empêchant la compilation d'un tel code.

Une bibliothèque Scala qui tente d'unifier le code au niveau des valeurs et des types (comme Haskell singletons ) serait un test intéressant pour la prise en charge des types dépendants par Scala. Une telle bibliothèque peut-elle être bien mieux réalisée en Scala grâce aux types dépendants du chemin ?

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