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

127

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?

manquant
la source
Vous pourriez être intéressé à parcourir haskell.org/haskellwiki/Dependent_type
Dan Burton
Merci pour le lien, Dan! Je connais les types dépendants en général, mais le concept de types de méthode dépendants est relativement nouveau pour moi.
missingfaktor
Il me semble que les "types de méthode dépendants" sont simplement des types qui dépendent d'un ou plusieurs types d'entrée d'une méthode (y compris le type de l'objet sur lequel la méthode est invoquée); rien de fou là-bas au-delà de l'idée générale des types dépendants. Peut-être que je manque quelque chose?
Dan Burton
Non, vous ne l'avez pas fait, mais apparemment je l'ai fait. :-) Je n'ai pas vu le lien entre les deux avant. C'est clair comme du cristal maintenant.
missingfaktor

Réponses:

112

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.

Miles Sabin
la source
2
C'est David MacIver qui a inventé le terme, mais en tout cas, c'est assez descriptif. C'est une explication fantastique de la raison pour laquelle les types de méthodes dépendantes sont si excitants. Bon travail!
Daniel Spiewak
Il est apparu au départ lors d'une conversation entre nous deux sur #scala il y a un certain temps ... comme je l'ai dit, je ne me souviens plus lequel d'entre nous l'a dit en premier.
Miles Sabin
Il semble que ma mémoire me jouait des tours ... le consensus est que c'était la monnaie de David MacIver.
Miles Sabin
Ouais, je n'étais pas là (sur #scala) à l'époque, mais Jorge était et c'est là que j'ai obtenu mes informations.
Daniel Spiewak
En utilisant le raffinement de membre de type abstrait, j'ai pu implémenter la fonction testHash4 assez facilement. def testHash4[R <: ResourceManager#BasicResource](rm: ResourceManager { type Resource = R }, r: R) = assert(r.hash == "9e47088d")Je suppose que cela peut être considéré comme une autre forme de types dépendants, cependant.
Marco van Hilst
53
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.

Alexey Romanov
la source
6

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, "")
         ^
Shelby Moore III
la source
C'est sans rapport. Avec les membres de type, vous pouvez utiliser des raffinements pour le même résultat: trait C {type A}; def f[M](a: C { type A = M}, b: M) = 0;class CI extends C{type A=Int};class CS extends C{type A=String}etc.
nafg
Dans tous les cas, cela n'a rien à voir avec les types de méthodes dépendantes. Prenons l'exemple d'Alexey ( stackoverflow.com/a/7860821/333643 ). L'utilisation de votre approche (y compris la version de raffinement que j'ai commentée) n'atteint pas l'objectif. Cela garantira que n1.Node =: = n2.Node, mais cela ne garantira pas qu'ils sont tous les deux dans le même graphique. IIUC DMT garantit cela.
nafg
@nafg Merci d'avoir signalé cela. J'ai ajouté le mot concret pour préciser que je ne faisais pas référence au cas de raffinement pour les membres de type. Pour autant que je sache, il s'agit toujours d'un cas d'utilisation valide pour les types de méthodes dépendantes malgré votre point (dont j'étais conscient) qu'ils peuvent avoir plus de puissance dans d'autres cas d'utilisation. Ou ai-je manqué l'essence fondamentale de votre deuxième commentaire?
Shelby Moore III
3

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
Shelby Moore III
la source
Quand nous avons besoin de passer les clés d'argument autour d'une seule valeur, je n'ai pas testé, mais supposons que nous pouvons utiliser un Tuple, par exemple pour la surcharge à 2 arguments def callit[A](argkeys: Tuple[DependentHashKey,DependentHashKey])(func: Env => argkeys._0.ValueType => argkeys._1.ValueType => A): A. Nous n'utiliserions pas une collection de clés d'argument, car les types d'éléments seraient subsumés (inconnus au moment de la compilation) dans le type de collection.
Shelby Moore III
"le typage statique du type d'élément de carte de hachage subsume à Any ou AnyRef" - je ne suis pas. Lorsque vous dites type d'élément, voulez-vous dire type de clé ou type de valeur (c'est-à-dire premier ou deuxième argument de type à HashMap)? Et pourquoi serait-il subsumé?
Robin Green
@RobinGreen Le type des valeurs dans la table de hachage. Afair, subsumé parce que vous ne pouvez pas mettre plus d'un type dans une collection dans Scala à moins que vous ne subsumiez leur supertype commun, car Scala n'a pas de type union (disjonction). Voir mes questions / réponses sur la subsomption dans Scala.
Shelby Moore III