Quels sont les cas d'utilisation convaincants des types de méthodes dépendantes?

Les types de méthode dépendants, qui étaient auparavant une fonctionnalité expérimentale, ont maintenant été activés par défaut dans le coffre , et apparemment cela semble avoir créé une certaine excitation dans la communauté Scala.

À première vue, il n'est pas immédiatement évident à quoi cela pourrait être utile. Heiko Seeberger a posté un exemple simple de types de méthodes dépendant ici , qui , comme on peut voir dans le commentaire , on peut facilement reproduire avec des paramètres de type sur les méthodes. Ce n'était donc pas un exemple très convaincant. (Il se peut qu'il me manque quelque chose d'évident. Veuillez me corriger si oui.)

Quels sont des exemples pratiques et utiles de cas d'utilisation pour les types de méthodes dépendants où ils sont clairement avantageux par rapport aux alternatives?

Quelles choses intéressantes pouvons-nous faire avec eux qui n'étaient pas possibles / faciles auparavant?

Que nous achètent-ils par rapport aux fonctionnalités existantes du système de type?

En outre, les types de méthodes dépendantes sont-ils analogues ou s'inspirent-ils de toutes les fonctionnalités trouvées dans les systèmes de types d'autres langages typés avancés tels que Haskell, OCaml?

Plus ou moins toute utilisation de types membres (c'est-à-dire imbriqués) peut donner lieu à un besoin de types de méthodes dépendantes. En particulier, je maintiens que sans types de méthode dépendants, le modèle de gâteau classique est plus proche d'un anti-modèle.

Donc quel est le problème? Les types imbriqués dans Scala dépendent de leur instance englobante. Par conséquent, en l'absence de types de méthodes dépendantes, les tentatives de les utiliser en dehors de cette instance peuvent être extrêmement difficiles. Cela peut transformer des designs qui semblent initialement élégants et attrayants en monstruosités qui sont d'une rigidité cauchemardesque et difficiles à refactoriser.

Je vais illustrer cela avec un exercice que je donne pendant mon cours de formation Advanced Scala ,

trait ResourceManager {
  type Resource <: BasicResource
  trait BasicResource {
    def hash : String
    def duplicates(r : Resource) : Boolean
  }
  def create : Resource

  // Test methods: exercise is to move them outside ResourceManager
  def testHash(r : Resource) = assert(r.hash == "9e47088d")  
  def testDuplicates(r : Resource) = assert(r.duplicates(r))
}

trait FileManager extends ResourceManager {
  type Resource <: File
  trait File extends BasicResource {
    def local : Boolean
  }
  override def create : Resource
}

class NetworkFileManager extends FileManager {
  type Resource = RemoteFile
  class RemoteFile extends File {
    def local = false
    def hash = "9e47088d"
    def duplicates(r : Resource) = (local == r.local) && (hash == r.hash)
  }
  override def create : Resource = new RemoteFile
}

C'est un exemple du modèle de gâteau classique: nous avons une famille d'abstractions qui sont progressivement affinées à travers une hiérarchie ( ResourceManager/ Resourcesont raffinées par FileManager/ Filequi sont à leur tour affinées par NetworkFileManager/ RemoteFile). C'est un exemple de jouet, mais le modèle est réel: il est utilisé dans tout le compilateur Scala et a été largement utilisé dans le plugin Scala Eclipse.

Voici un exemple de l'abstraction utilisée,

val nfm = new NetworkFileManager
val rf : nfm.Resource = nfm.create
nfm.testHash(rf)
nfm.testDuplicates(rf)

Notez que la dépendance de chemin signifie que le compilateur garantira que les méthodes testHashet on ne peuvent être appelées qu'avec des arguments qui y correspondent, c'est-à-dire. c'est propre , et rien d'autre.testDuplicatesNetworkFileManagerRemoteFiles

C'est indéniablement une propriété souhaitable, mais supposons que nous voulions déplacer ce code de test vers un autre fichier source? Avec les types de méthodes dépendantes, il est très facile de redéfinir ces méthodes en dehors de la ResourceManagerhiérarchie,

def testHash4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.hash == "9e47088d")

def testDuplicates4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.duplicates(r))

Notez ici les utilisations des types de méthode dépendants: le type du deuxième argument ( rm.Resource) dépend de la valeur du premier argument ( rm).

Il est possible de le faire sans types de méthodes dépendantes, mais c'est extrêmement gênant et le mécanisme est assez peu intuitif: j'enseigne ce cours depuis près de deux ans maintenant, et pendant ce temps, personne n'a trouvé une solution de travail sans invitation.

Essayez-le par vous-même ...

// Reimplement the testHash and testDuplicates methods outside
// the ResourceManager hierarchy without using dependent method types
def testHash        // TODO ... 
def testDuplicates  // TODO ...

testHash(rf)
testDuplicates(rf)

Après un court moment, vous découvrirez probablement pourquoi moi (ou peut-être que c'était David MacIver, nous ne pouvons pas nous rappeler lequel d'entre nous a inventé le terme) appelle cela la Bakery of Doom.

Edit: le consensus est que Bakery of Doom était la monnaie de David MacIver ...

Pour le bonus: la forme de Scala des types dépendants en général (et des types de méthodes dépendants en tant que partie de celui-ci) a été inspirée par le langage de programmation Beta ... ils proviennent naturellement de la sémantique d'imbrication cohérente de Beta. Je ne connais aucun autre langage de programmation, même faiblement courant, qui a des types dépendants sous cette forme. Des langages comme Coq, Cayenne, Epigram et Agda ont une forme différente de typage dépendant qui est à certains égards plus générale, mais qui diffère considérablement en faisant partie de systèmes de types qui, contrairement à Scala, n'ont pas de sous-typage.

trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}

Quelque part ailleurs, nous pouvons garantir statiquement que nous ne mélangeons pas les nœuds de deux graphes différents, par exemple:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 

Bien sûr, cela a déjà fonctionné si défini à l'intérieur Graph, mais disons que nous ne pouvons pas modifier Graphet que nous écrivons une extension "pimp my library" pour cela.

À propos de la deuxième question: les types activés par cette fonctionnalité sont beaucoup plus faibles que les types dépendants complets (voir Programmation à typage dépendant dans Agda pour une idée de cela.) Je ne pense pas avoir vu d'analogie auparavant.

Cette nouvelle fonctionnalité est nécessaire lorsque des membres de type abstrait concrets sont utilisés au lieu de paramètres de type . Lorsque des paramètres de type sont utilisés, la dépendance de type de polymorphisme de famille peut être exprimée dans la dernière et certaines versions plus anciennes de Scala, comme dans l'exemple simplifié suivant.

trait C[A]
def f[M](a: C[M], b: M) = b
class C1 extends C[Int]
class C2 extends C[String]

f(new C1, 0)
res0: Int = 0
f(new C2, "")
res1: java.lang.String = 
f(new C1, "")
error: type mismatch;
 found   : C1
 required: C[Any]
       f(new C1, "")
         ^

Je développe un modèle pour l'interoption d'une forme de programmation déclarative avec l'état environnemental. Les détails ne sont pas pertinents ici (par exemple, des détails sur les rappels et la similitude conceptuelle avec le modèle Actor combiné avec un sérialiseur).

Le problème pertinent est que les valeurs d'état sont stockées dans une carte de hachage et référencées par une valeur de clé de hachage. Les fonctions entrent des arguments immuables qui sont des valeurs de l'environnement, peuvent appeler d'autres fonctions de ce type et écrire l'état dans l'environnement. Mais les fonctions ne sont pas autorisées à lire les valeurs de l'environnement (donc le code interne de la fonction ne dépend pas de l'ordre des changements d'état et reste donc déclaratif dans ce sens). Comment taper ceci dans Scala?

La classe d'environnement doit avoir une méthode surchargée qui entre une telle fonction à appeler et entre les clés de hachage des arguments de la fonction. Ainsi, cette méthode peut appeler la fonction avec les valeurs nécessaires à partir de la carte de hachage, sans fournir un accès public en lecture aux valeurs (donc selon les besoins, en refusant aux fonctions de lire les valeurs de l'environnement).

Mais si ces clés de hachage sont des chaînes ou des valeurs de hachage entières, le typage statique du type d'élément de mappe de hachage se résume à Any ou AnyRef (code de mappe de hachage non illustré ci-dessous), et donc une incompatibilité d'exécution pourrait se produire, c'est-à-dire qu'il serait possible pour mettre n'importe quel type de valeur dans une carte de hachage pour une clé de hachage donnée.

trait Env {
...
  def callit[A](func: Env => Any => A, arg1key: String): A
  def callit[A](func: Env => Any => Any => A, arg1key: String, arg2key: String): A
}

Bien que je n'ai pas testé ce qui suit, en théorie, je peux obtenir les clés de hachage à partir des noms de classe au moment de l'exécution classOf, donc une clé de hachage est un nom de classe au lieu d'une chaîne (en utilisant les backticks de Scala pour incorporer une chaîne dans un nom de classe).

trait DependentHashKey {
  type ValueType
}
trait `the hash key string` extends DependentHashKey {
  type ValueType <: SomeType
}

Ainsi, la sécurité de type statique est obtenue.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A