Pomijając wygodę składniową, kombinacja typów singletonów, typów zależnych od ścieżki i wartości niejawnych oznacza, że Scala ma zaskakująco dobre wsparcie dla pisania zależnego, co próbowałem pokazać w bezkształtnym .
Wewnętrzne wsparcie Scali dla typów zależnych odbywa się za pośrednictwem typów zależnych od ścieżki . Umożliwiają one typowi zależność od ścieżki selektora przez wykres obiektu (tj. Wartość-), taki jak ten,
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]
Moim zdaniem powyższe powinno wystarczyć, aby odpowiedzieć na pytanie „Czy Scala jest językiem zależnym?” pozytywnie: jasne jest, że mamy tutaj typy, które są rozróżniane przez wartości będące ich przedrostkami.
Jednak często zarzuca się, że Scala nie jest językiem typu „w pełni” zależnego, ponieważ nie ma sum zależnych i typów produktów które można znaleźć w Agda, Coq lub Idris jako wewnętrzne. Myślę, że do pewnego stopnia odzwierciedla to fiksację na temat formy, a nie podstaw, niemniej jednak spróbuję pokazać, że Scala jest dużo bliższa tym innym językom, niż się zwykle przyznaje.
Pomimo terminologii, zależne typy sum (znane również jako typy Sigma) są po prostu parą wartości, w których typ drugiej wartości zależy od pierwszej wartości. Można to bezpośrednio przedstawić w Scali,
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
i faktycznie jest to kluczowa część kodowania zależnych typów metod, które są potrzebne, aby uciec z „Bakery of Doom” w Scali przed 2.10 (lub wcześniej poprzez eksperymentalną opcję kompilatora Scala z typami metod zależnymi -Y).
Zależne typy produktów (inaczej typy Pi) to zasadniczo funkcje od wartości do typów. Są kluczem do reprezentacji wektorów o statycznej wielkości i innych elementów potomnych plakatów dla zależnie typowanych języków programowania. Możemy kodować typy Pi w Scali, używając kombinacji typów zależnych od ścieżki, typów singletonów i niejawnych parametrów. Najpierw definiujemy cechę, która będzie reprezentować funkcję od wartości typu T do typu U,
scala> trait Pi[T] { type U }
defined trait Pi
Możemy niż zdefiniować metodę polimorficzną, która używa tego typu,
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]
(zwróć uwagę na użycie typu zależnego od ścieżki pi.U w typie wynikuList[pi.U] ). Biorąc pod uwagę wartość typu T, ta funkcja zwróci (n pustą) listę wartości typu odpowiadającego tej określonej wartości T.
Teraz zdefiniujmy odpowiednie wartości i niejawnych świadków relacji funkcjonalnych, które chcemy utrzymywać,
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
A teraz nasza funkcja używająca typu Pi w akcji,
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]]
(zwróć uwagę, że używamy tutaj <:<operatora świadka podtypu Scali, a nie =:=ponieważres2.type i res3.typesą Singleton rodzaje i tym samym bardziej precyzyjne niż typów jesteśmy weryfikujących na RHS).
W praktyce jednak w Scali nie zaczynalibyśmy od zakodowania typów Sigma i Pi, a potem stamtąd tak jak w Agdzie czy Idrisie. Zamiast tego użylibyśmy bezpośrednio typów zależnych od ścieżki, typów pojedynczych i implikacji. Możesz znaleźć wiele przykładów tego, jak to działa w bezkształtnych: typach rozmiarów , rozszerzalnych rekordach , obszernych listach HL , złomowaniu szablonu , Zamki błyskawiczne generycznych itp itd.
Jedynym pozostałym zastrzeżeniem, jaki widzę, jest to, że w powyższym kodowaniu typów Pi wymagamy, aby pojedyncze typy wartości zależnych były wyrażalne. Niestety w Scali jest to możliwe tylko dla wartości typów referencyjnych, a nie dla wartości typów niereferencyjnych (szczególnie np. Int). To wstyd, ale nie nieodłączną trudność: typ sprawdzania Scala reprezentuje typy singleton wartości niereferencyjnych wewnętrznie, a pojawiło się kilka z eksperymentów w czyniąc je bezpośrednio podlegać ekspresji. W praktyce możemy obejść ten problem za pomocą dość standardowego kodowania liczb naturalnych na poziomie typu .
W każdym razie nie sądzę, aby to drobne ograniczenie domeny mogło być wykorzystane jako sprzeciw wobec statusu Scali jako języka zależnie wpisywanego. Jeśli tak, to to samo można by powiedzieć o zależnym ML (który dopuszcza tylko zależności od wartości liczb naturalnych), co byłoby dziwnym wnioskiem.