Jakie są atrakcyjne przypadki użycia dla zależnych typów metod?

127

Zależne typy metod, które wcześniej były funkcją eksperymentalną, zostały teraz domyślnie włączone w linii głównej i najwyraźniej wywołało to pewne podekscytowanie w społeczności Scala.

Na pierwszy rzut oka nie jest od razu oczywiste, do czego może to być przydatne. Heiko Seeberger napisali prosty przykład zależnych rodzaju metody tutaj , które, jak można zobaczyć w komentarzu nie mogą być łatwo reprodukowane z parametrami typu na metodach. Nie był to więc zbyt przekonujący przykład. (Mogę pominąć coś oczywistego. Popraw mnie, jeśli tak).

Jakie są praktyczne i przydatne przykłady przypadków użycia dla zależnych typów metod, w których są one wyraźnie lepsze od alternatyw?

Jakie ciekawe rzeczy możemy z nimi zrobić, które wcześniej nie były możliwe / łatwe?

Co kupują nam w porównaniu z istniejącymi funkcjami systemu typów?

Ponadto, czy zależne typy metod są analogiczne lub czerpią inspirację z jakichkolwiek cech występujących w systemach czcionek innych zaawansowanych języków, takich jak Haskell, OCaml?

missingfaktor
źródło
Możesz być zainteresowany przeczytaniem haskell.org/haskellwiki/Dependent_type
Dan Burton
Dzięki za link, Dan! Ogólnie znam typy zależne, ale pojęcie typów metod zależnych jest dla mnie stosunkowo nowe.
missingfaktor
Wydaje mi się, że „zależne typy metod” to po prostu typy, które są zależne od jednego lub kilku typów danych wejściowych metody (w tym typu obiektu, dla którego metoda jest wywoływana); nic szalonego poza ogólną ideą typów zależnych. Może czegoś mi brakuje?
Dan Burton
Nie, nie zrobiłeś tego, ale najwyraźniej tak. :-) Nie widziałem wcześniej powiązania między nimi. Teraz jest jednak krystalicznie czysty.
missingfaktor

Odpowiedzi:

112

Mniej więcej jakiekolwiek użycie typów składowych (tj. Zagnieżdżonych) może spowodować potrzebę zastosowania zależnych typów metod. W szczególności uważam, że bez metod zależnych klasyczny wzór ciasta jest bliżej bycia anty-wzorem.

Więc w czym problem? Zagnieżdżone typy w Scali zależą od otaczającej je instancji. W konsekwencji, przy braku zależnych typów metod, próby użycia ich poza tym wystąpieniem mogą być frustrująco trudne. Może to zmienić projekty, które początkowo wydają się eleganckie i atrakcyjne, w potworności, które są koszmarnie sztywne i trudne do zreformowania.

Zilustruję to ćwiczeniem, które wykonuję na moim kursie 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
}

To przykład klasycznego wzoru ciasta: mamy rodzinę abstrakcji, które są stopniowo udoskonalane przez hierarchię ( ResourceManager/ Resourcesą udoskonalane przez FileManager/ Filektóre z kolei są udoskonalane przez NetworkFileManager/RemoteFile ). To przykład zabawki, ale wzorzec jest prawdziwy: jest używany w całym kompilatorze Scala i był szeroko stosowany we wtyczce Scala Eclipse.

Oto przykład używanej abstrakcji,

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

Zauważ, że zależność od ścieżki oznacza, że ​​kompilator zagwarantuje, że metody testHashi testDuplicateson NetworkFileManagermożna wywołać tylko z argumentami, które im odpowiadają, tj. jest własny RemoteFilesi nic więcej.

Jest to niezaprzeczalnie pożądana właściwość, ale załóżmy, że chcielibyśmy przenieść ten kod testowy do innego pliku źródłowego? Z zależnymi typami metod bardzo łatwo jest przedefiniować te metody poza ResourceManagerhierarchią,

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

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

Zauważ tutaj zastosowania zależnych typów metod: typ drugiego argumentu ( rm.Resource) zależy od wartości pierwszego argumentu ( rm).

Można to zrobić bez zależnych typów metod, ale jest to niezwykle niewygodne, a mechanizm jest dość nieintuicyjny: prowadzę ten kurs od prawie dwóch lat i przez ten czas nikt nie wymyślił działającego rozwiązania bez sugestii.

Wypróbuj sam ...

// 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)

Po krótkiej chwili zmagania się z tym prawdopodobnie odkryjesz, dlaczego ja (a może to był David MacIver, nie pamiętamy, który z nas ukuł ten termin) nazywam to Piekarnią Zagłady.

Edycja: konsensus jest taki, że Bakery of Doom była monetą Davida MacIvera ...

Na dodatek: forma typów zależnych Scali w ogóle (i zależne typy metod jako jej część) została zainspirowana językiem programowania Beta ... wynikają one naturalnie ze spójnej semantyki zagnieżdżania Beta. Nie znam żadnego innego, nawet słabo głównego języka programowania, który ma zależne typy w tej formie. Języki takie jak Coq, Cayenne, Epigram i Agda mają inną formę pisania zależnego, która jest pod pewnymi względami bardziej ogólna, ale różni się znacznie tym, że jest częścią systemów typów, które w przeciwieństwie do Scala nie mają podtypów.

Miles Sabin
źródło
2
To David MacIver ukuł ten termin, ale w każdym razie jest on dość opisowy. To fantastyczne wyjaśnienie, dlaczego metody zależne są tak ekscytujące. Dobra robota!
Daniel Spiewak
Pojawiło się to w rozmowie między nami dwojgiem na #scala jakiś czas temu ... tak jak powiedziałem, nie pamiętam, który z nas powiedział to pierwszy.
Miles Sabin
Wygląda na to, że moja pamięć płatała mi figle ... konsensus jest taki, że to pomysł Davida MacIvera.
Miles Sabin
Tak, wtedy mnie tam nie było (na #scala), ale był tam Jorge i właśnie tam zbierałem informacje.
Daniel Spiewak
Korzystając z doprecyzowania składowej typu abstrakcyjnego, byłem w stanie dość bezboleśnie zaimplementować funkcję testHash4. def testHash4[R <: ResourceManager#BasicResource](rm: ResourceManager { type Resource = R }, r: R) = assert(r.hash == "9e47088d")Przypuszczam jednak, że można to uznać za inną formę typów zależnych.
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]
}

Gdzie indziej możemy statycznie zagwarantować, że nie pomieszamy węzłów z dwóch różnych wykresów, np .:

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

Oczywiście to już zadziałało, jeśli zostało zdefiniowane w środku Graph, ale powiedzmy, że nie możemy modyfikować Graphi piszemy dla niego rozszerzenie „pimp my library”.

O drugim pytaniu: typy włączane przez tę funkcję są znacznie słabsze niż kompletne typy zależne (zobacz programowanie zależne z typami w Agdzie, aby poznać smak tego). Nie sądzę, że widziałem wcześniej analogię.

Alexey Romanov
źródło
6

Ta nowa funkcja jest potrzebna, gdy zamiast parametrów typu są używane konkretne elementy członkowskie typu abstrakcyjnego . Gdy używane są parametry typu, zależność typu polimorfizmu rodziny można wyrazić w najnowszej i niektórych starszych wersjach Scala, jak w poniższym uproszczonym przykładzie.

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
źródło
To nie ma związku. W przypadku członków typu możesz użyć 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}
zawężeń wyszukiwania
W każdym razie nie ma to nic wspólnego z zależnymi typami metod. Weźmy na przykład przykład Alexeya ( stackoverflow.com/a/7860821/333643 ). Korzystanie z twojego podejścia (w tym wersji udoskonalonej, którą skomentowałem) nie prowadzi do osiągnięcia celu. Zapewni to, że n1.Node =: = n2.Node, ale nie zapewni, że oba znajdują się na tym samym wykresie. IIUC DMT zapewnia to.
nafg
@nafg Dzięki za wskazanie tego. Dodałem słowo konkretny, aby było jasne, że nie odnoszę się do przypadku uściślenia dla członków typu. O ile widzę, jest to nadal ważny przypadek użycia dla zależnych typów metod, pomimo twojego punktu (którego byłem świadomy), że mogą one mieć większą moc w innych przypadkach użycia. A może przegapiłem zasadniczą istotę twojego drugiego komentarza?
Shelby Moore III
3

Jestem opracowanie modelu dla interoption w formie deklaratywnej programowania ze stanem środowiska. Szczegóły nie są tutaj istotne (np. Szczegóły dotyczące wywołań zwrotnych i koncepcyjnego podobieństwa do modelu Actor w połączeniu z Serializatorem).

Istotnym problemem jest to, że wartości stanu są przechowywane w mapie skrótów i odwołują się do wartości klucza skrótu. Funkcje wprowadzają niezmienne argumenty, które są wartościami ze środowiska, mogą wywoływać inne takie funkcje i zapisywać stan do środowiska. Ale funkcje nie mogą odczytywać wartości ze środowiska (więc wewnętrzny kod funkcji nie jest zależny od kolejności zmian stanu i dlatego pozostaje deklaratywny w tym sensie). Jak to wpisać w Scali?

Klasa środowiska musi mieć przeciążoną metodę, która wprowadza taką funkcję do wywołania i wprowadza klucze skrótu argumentów funkcji. W ten sposób ta metoda może wywołać funkcję z niezbędnymi wartościami z mapy skrótów, bez zapewniania publicznego dostępu do odczytu wartości (w ten sposób zgodnie z wymaganiami, odmawiając funkcjom możliwości odczytu wartości ze środowiska).

Ale jeśli te klucze skrótu są ciągami lub całkowitymi wartościami skrótu, statyczne wpisywanie typu elementu mapy skrótów obejmuje Any lub AnyRef (kod mapy skrótów nie jest pokazany poniżej), a zatem może wystąpić niezgodność w czasie wykonywania, tj. Byłoby to możliwe aby umieścić dowolny typ wartości w mapie skrótów dla danego klucza mieszającego.

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
}

Chociaż nie testowałem następujących elementów, teoretycznie mogę uzyskać klucze skrótu z nazw klas w środowisku classOfuruchomieniowym, więc klucz skrótu jest nazwą klasy zamiast ciągu (przy użyciu odwrotnych apostrofów Scali do osadzenia ciągu w nazwie klasy).

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

W ten sposób uzyskuje się bezpieczeństwo typu statycznego.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A
Shelby Moore III
źródło
Kiedy musimy przekazać klucze argumentów w pojedynczej wartości, nie testowałem, ale założyłem, że możemy użyć krotki, np. Dla przeciążenia 2 argumentami def callit[A](argkeys: Tuple[DependentHashKey,DependentHashKey])(func: Env => argkeys._0.ValueType => argkeys._1.ValueType => A): A. Nie używalibyśmy kolekcji kluczy argumentów, ponieważ typy elementów byłyby podliczane (nieznane w czasie kompilacji) w typie kolekcji.
Shelby Moore III
„statyczne wpisywanie typu elementu mapy hashowej obejmuje Any lub AnyRef” - nie nadążam. Kiedy mówisz typ elementu, czy masz na myśli typ klucza czy typ wartości (tj. Pierwszy lub drugi argument typu w HashMap)? I dlaczego miałby zostać podciągnięty?
Robin Green
@RobinGreen Typ wartości w tabeli skrótów. Afair, podciągnięte, ponieważ nie możesz umieścić więcej niż jednego typu w kolekcji w Scali, chyba że podciągniesz do ich wspólnego nadtypu, ponieważ Scala nie ma typu unii (rozłączenia). Zobacz moje pytania i odpowiedzi dotyczące subskrypcji w Scali.
Shelby Moore III