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

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?

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.

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ę.

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, "")
         ^

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