Czy jest jakiś powód, dla którego scala nie obsługuje jawnie typów zależnych?

Istnieją typy zależne od ścieżki i myślę, że można wyrazić prawie wszystkie cechy takich języków jak Epigram czy Agda w Scali, ale zastanawiam się, dlaczego Scala nie obsługuje tego bardziej dosłownie, tak jak robi to bardzo ładnie w innych obszarach (powiedzmy , DSL)? Brakuje mi czegoś takiego jak „to nie jest konieczne”?

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.

Przypuszczam, że dzieje się tak dlatego, że (jak wiem z doświadczenia, korzystając z typów zależnych w asystencie Coq proof, który w pełni je obsługuje, ale nadal nie w bardzo wygodny sposób) typy zależne są bardzo zaawansowaną funkcją języka programowania, którą naprawdę trudno racja - i może w praktyce spowodować gwałtowny wzrost złożoności. Nadal są tematem badań informatycznych.

Uważam, że typy zależne od ścieżki Scali mogą reprezentować tylko typy Σ, ale nie typy Π. To:

trait Pi[T] { type U }

nie jest dokładnie typu Π. Z definicji typ Π, czyli iloczyn zależny, jest funkcją, której typ wyniku zależy od wartości argumentu, reprezentując uniwersalny kwantyfikator, czyli ∀x: A, B (x). W powyższym przypadku zależy to jednak tylko od typu T, a nie od jakiejś wartości tego typu. Sama cecha Pi jest typem Σ, egzystencjalnym kwantyfikatorem, czyli ∃x: A, B (x). Odniesienie do obiektu w tym przypadku działa jako zmienna ilościowa. Jednak po przekazaniu jako niejawny parametr ogranicza się do funkcji typu zwykłego, ponieważ jest rozpoznawany według typu. Kodowanie produktu zależnego w Scali może wyglądać następująco:

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U 

Brakującym elementem jest tutaj możliwość statycznego ograniczenia pola x do wartości oczekiwanej t, skutecznie tworząc równanie reprezentujące własność wszystkich wartości zamieszkujących typ T. Wraz z naszymi typami Σ, używanymi do wyrażenia istnienia obiektu o danej właściwości, powstaje logika, w której nasze równanie jest twierdzeniem do udowodnienia.

Na marginesie, w rzeczywistych przypadkach twierdzenie może być wysoce nietrywialne, aż do punktu, w którym nie można go automatycznie wyprowadzić z kodu lub rozwiązać bez znacznego wysiłku. Można nawet w ten sposób sformułować hipotezę Riemanna, tylko po to, aby znaleźć sygnaturę niemożliwą do zaimplementowania bez faktycznego jej udowodnienia, zapętlenia się w nieskończoność lub rzucenia wyjątku.

Pytanie dotyczyło bardziej bezpośredniego korzystania z funkcji pisania na klawiaturze zależnej i, moim zdaniem, skorzystanie z bardziej bezpośredniego podejścia do pisania zależnego od tego, co oferuje Scala.
Obecne odpowiedzi starają się uargumentować pytanie na poziomie teoretycznym. Chcę nadać temu bardziej pragmatyczny charakter. To może wyjaśniać, dlaczego ludzie są podzieleni co do poziomu wsparcia typów zależnych w języku Scala. Możemy mieć na myśli nieco inne definicje. (nie mówiąc, że jeden ma rację, a drugi się myli).

To nie jest próba odpowiedzi na pytanie, jak łatwo byłoby zamienić Scalę w coś takiego jak Idris (wyobrażam sobie bardzo trudne) lub napisać bibliotekę oferującą bardziej bezpośrednie wsparcie dla takich możliwości Idrisa (jak singletonspróby bycia w Haskell).

Zamiast tego chcę podkreślić pragmatyczną różnicę między Scalą a językiem takim jak Idris.
Co to są bity kodu dla wyrażeń na poziomie wartości i typu? Idris używa tego samego kodu, Scala używa zupełnie innego kodu.

Scala (podobnie jak Haskell) może być w stanie zakodować wiele obliczeń na poziomie typu. Pokazują to biblioteki takie jak shapeless. Te biblioteki robią to, używając naprawdę imponujących i sprytnych sztuczek. Jednak ich kod poziomu typu jest (obecnie) zupełnie inny niż wyrażenia poziomu wartości (uważam, że ta luka jest nieco bliższa w Haskell). Idris pozwala na użycie wyrażenia na poziomie wartości na poziomie typu AS IS.

Oczywistą korzyścią jest ponowne wykorzystanie kodu (nie ma potrzeby kodowania wyrażeń na poziomie typu oddzielnie od poziomu wartości, jeśli potrzebujesz ich w obu miejscach). Pisanie kodu poziomu wartości powinno być dużo łatwiejsze. Powinno być łatwiej nie mieć do czynienia z hackami, takimi jak singletony (nie wspominając o kosztach wydajności). Nie musisz uczyć się dwóch rzeczy, uczysz się jednej rzeczy. Na poziomie pragmatycznym w końcu potrzebujemy mniej koncepcji. Wpisz synonimy, rodziny typów, funkcje, ... a co powiesz na same funkcje? Moim zdaniem te jednoczące korzyści sięgają znacznie głębiej i są czymś więcej niż wygodą składniową.

Rozważ zweryfikowany kod. Zobacz:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Sprawdzanie typów weryfikuje dowody monadycznych / funktorów / obowiązujących praw, a dowody są zgodne z rzeczywistymi implementacje monad / functor / application, a nie jakiś ekwiwalent zakodowanego typu, który może być taki sam lub inny. Najważniejsze pytanie brzmi: co udowadniamy?

To samo mogę zrobić, używając sprytnych sztuczek kodowania (patrz poniżej dla wersji Haskell, nie widziałem jednej dla Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https: // github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
poza tym, że typy są tak skomplikowane, że trudno jest zobaczyć prawa, wyrażenia poziomu wartości są konwertowane (automatycznie, ale nadal) na rzeczy z poziomu i musisz również ufać tej konwersji . W tym wszystkim jest miejsce na błąd, co jest sprzeczne z celem kompilatora działającego jako pomocnik dowodu.

(EDYTOWANE 2018.8.10) Mówiąc o pomocy dowodowej, oto kolejna duża różnica między Idrisem a Scalą. W Scali (czy Haskellu) nie ma nic, co mogłoby przeszkodzić w pisaniu rozbieżnych dowodów:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

podczas gdy Idris ma totalsłowo kluczowe zapobiegające kompilacji takiego kodu.

Biblioteka Scali, która próbuje ujednolicić kod poziomu wartości i typu (jak Haskell singletons), byłaby interesującym testem dla obsługi typów zależnych przez Scala. Czy taka biblioteka może być znacznie lepsza w Scali z powodu typów zależnych od ścieżki?

Jestem zbyt nowy w Scali, by samemu odpowiedzieć na to pytanie.