Zasoby programowania typu Scala

102

Zgodnie z tym pytaniem system typów Scali jest kompletny w Turingu . Jakie zasoby są dostępne, aby nowicjusz mógł skorzystać z możliwości programowania na poziomie typu?

Oto zasoby, które do tej pory znalazłem:

Te zasoby są świetne, ale wydaje mi się, że brakuje mi podstaw, więc nie mam solidnych podstaw, na których można by budować. Na przykład, gdzie jest wprowadzenie do definicji typów? Jakie operacje mogę wykonywać na typach?

Czy są jakieś dobre materiały wprowadzające?

scala types dsg
źródło
Osobiście uważam założenie, że ktoś, kto chce programować na poziomie typu w Scali, już wie, jak programować w Scali, całkiem rozsądne. Nawet jeśli oznacza to, że nie rozumiem ani słowa z tych artykułów, do których linkowałeś :-)
Jörg W Mittag

Odpowiedzi:

140

Przegląd

Programowanie na poziomie typu ma wiele podobieństw z tradycyjnym programowaniem na poziomie wartości. Jednak w przeciwieństwie do programowania na poziomie wartości, w którym obliczenia są wykonywane w czasie wykonywania, w programowaniu na poziomie typu obliczenia są wykonywane w czasie kompilacji. Spróbuję narysować podobieństwa między programowaniem na poziomie wartości a programowaniem na poziomie typu.

Paradygmaty

Istnieją dwa główne paradygmaty programowania na poziomie typu: „obiektowy” i „funkcjonalny”. Większość przykładów, do których prowadzą linki, jest zgodnych z paradygmatem zorientowanym obiektowo.

Dobry, dość prosty przykład programowania na poziomie typu w paradygmacie zorientowanym obiektowo można znaleźć w implementacji rachunku lambda w apokalisie , zreplikowanym tutaj:

// Abstract trait
trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

Jak widać na przykładzie, paradygmat zorientowany obiektowo w programowaniu na poziomie typu przebiega następująco:

  • Po pierwsze: zdefiniuj cechę abstrakcyjną za pomocą różnych pól typu abstrakcyjnego (zobacz poniżej, czym jest pole abstrakcyjne). Jest to szablon gwarantujący, że określone typy pól istnieją we wszystkich implementacjach bez wymuszania implementacji. Na przykład rachunek lambda, ten odpowiada trait Lambda, że gwarancje, że istnieją następujące typy: subst, apply, i eval.
  • Następnie: zdefiniuj cechy podrzędne, które rozszerzają cechę abstrakcyjną i implementują różne pola typu abstrakcyjnego
    • Często te cechy są parametryzowane za pomocą argumentów. W przykładzie rachunku lambda podtypy są trait App extends Lambdasparametryzowane za pomocą dwóch typów ( Si Toba muszą być podtypami Lambda), trait Lam extends Lambdasparametryzowane za pomocą jednego typu ( T) i trait X extends Lambda(które nie są sparametryzowane).
    • pola typu są często implementowane poprzez odwoływanie się do parametrów typu cechy podrzędnej, a czasami odwoływanie się do ich pól typu za pomocą operatora skrótu: #(który jest bardzo podobny do operatora kropki: .dla wartości). W cechy Appprzykładu lambda nazębnego, rodzaju evalrealizowana jest w następujący sposób: type eval = S#eval#apply[T]. Zasadniczo jest to wywołanie evaltypu parametru cechy Si wywołanie wyniku applyz parametrem T. Uwaga, Sna pewno ma evaltyp, ponieważ parametr określa, że ​​jest to podtyp Lambda. Podobnie, wynik evalmusi mieć applytyp, ponieważ jest określony jako podtyp Lambda, zgodnie z definicją cechy abstrakcyjnej Lambda.

Paradygmat funkcjonalny polega na definiowaniu wielu sparametryzowanych konstruktorów typów, które nie są zgrupowane razem w cechy.

Porównanie między programowaniem na poziomie wartości a programowaniem na poziomie typu

  • Klasa abstrakcyjna
    • poziom wartości: abstract class C { val x }
    • poziom typu: trait C { type X }
  • typy zależne od ścieżki
    • C.x (odniesienie do wartości pola / funkcji x w obiekcie C)
    • C#x (odnoszący się do pola typu x w cechy C)
  • podpis funkcji (bez implementacji)
    • poziom wartości: def f(x:X) : Y
    • poziom typu: type f[x <: X] <: Y(nazywa się to „konstruktorem typu” i zwykle występuje w cechy abstrakcyjnej)
  • implementacja funkcji
    • poziom wartości: def f(x:X) : Y = x
    • poziom typu: type f[x <: X] = x
  • warunki warunkowe
  • sprawdzanie równości
    • poziom wartości: a:A == b:B
    • poziom typu: implicitly[A =:= B]
    • poziom wartości: dzieje się w JVM poprzez test jednostkowy w czasie wykonywania (tzn. brak błędów w czasie wykonywania):
      • w istocie jest twierdzeniem: assert(a == b)
    • poziom typu: dzieje się w kompilatorze poprzez sprawdzenie typu (tj. brak błędów kompilatora):
      • w istocie jest to porównanie typów: np implicitly[A =:= B]
      • A <:< B, kompiluje się tylko wtedy, gdy Ajest podtypemB
      • A =:= B, kompiluje się tylko wtedy, gdy Ajest podtypem Bi Bjest podtypemA
      • A <%< B, („widoczny jako”) kompiluje się tylko wtedy, gdy Ajest widoczny jako B(tj. istnieje niejawna konwersja z Ana podtyp B)
      • przykład
      • więcej operatorów porównania

Konwersja między typami i wartościami

  • W wielu przykładach typy zdefiniowane za pomocą cech są często zarówno abstrakcyjne, jak i zapieczętowane, w związku z czym nie można ich utworzyć bezpośrednio ani za pośrednictwem anonimowej podklasy. Dlatego często używa się go nulljako wartości zastępczej podczas wykonywania obliczeń na poziomie wartości przy użyciu pewnego rodzaju zainteresowania:

    • np. val x:A = nullgdzie Ajest typ , na którym Ci zależy

  • Ze względu na wymazywanie typów sparametryzowane typy wyglądają tak samo. Ponadto (jak wspomniano powyżej) wartości, z którymi pracujesz, zwykle są null, więc warunkowanie typu obiektu (np. Za pomocą instrukcji match) jest nieskuteczne.

Sztuczka polega na użyciu niejawnych funkcji i wartości. Przypadek podstawowy jest zwykle wartością niejawną, a przypadek rekurencyjny jest zwykle funkcją niejawną. Rzeczywiście, programowanie na poziomie typu w dużym stopniu wykorzystuje implikacje.

Rozważmy ten przykład ( zaczerpnięty z metascala i apocalisp ):

sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat

Tutaj masz kodowanie peano liczb naturalnych. Oznacza to, że masz typ dla każdej nieujemnej liczby całkowitej: specjalny typ dla 0, a mianowicie _0; a każda liczba całkowita większa od zera ma typ formularza Succ[A], gdzie Ajest typem reprezentującym mniejszą liczbę całkowitą. Na przykład typem reprezentującym 2 byłby: Succ[Succ[_0]](następca zastosowany dwukrotnie do typu reprezentującego zero).

Możemy aliasować różne liczby naturalne dla wygodniejszego odniesienia. Przykład:

type _3 = Succ[Succ[Succ[_0]]]

(To jest bardzo podobne do definiowania a valjako wyniku funkcji).

Teraz przypuśćmy, że chcemy zdefiniować funkcję na poziomie wartości, def toInt[T <: Nat](v : T)która przyjmuje wartość argumentu v, która jest zgodna z Nati zwraca liczbę całkowitą reprezentującą liczbę naturalną zakodowaną w vtypie. Na przykład, jeśli mamy wartość val x:_3 = null( nulltypu Succ[Succ[Succ[_0]]]), chcielibyśmy toInt(x)zwrócić 3.

Aby zaimplementować toInt, wykorzystamy następującą klasę:

class TypeToValue[T, VT](value : VT) { def getValue() = value }

Jak zobaczymy poniżej, TypeToValuedla każdego z klas Natod _0do (np.) Powstanie obiekt zbudowany z klasy _3, a każdy z nich będzie przechowywać reprezentację wartości odpowiedniego typu (tj. TypeToValue[_0, Int]Będzie przechowywać wartość 0, TypeToValue[Succ[_0], Int]będzie przechowywać wartość 1itp.). Uwaga, TypeToValuejest parametryzowana przez dwa typy: Ti VT. Todpowiada typowi, do którego próbujemy przypisać wartości (w naszym przykładzie Nat) i VTodpowiada typowi wartości, który mu przypisujemy (w naszym przykładzie Int).

Teraz tworzymy następujące dwie niejawne definicje:

implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = 
     new TypeToValue[Succ[P], Int](1 + v.getValue())

I realizujemy toIntw następujący sposób:

def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()

Aby zrozumieć, jak to toIntdziała, zastanówmy się, co robi na kilku wejściach:

val z:_0 = null
val y:Succ[_0] = null

Kiedy wywołujemy toInt(z), kompilator szuka niejawnego argumentu ttvtypu TypeToValue[_0, Int](ponieważ zjest typu _0). Znajduje obiekt _0ToInt, wywołuje getValuemetodę tego obiektu i wraca 0. Ważną kwestią, na którą należy zwrócić uwagę, jest to, że nie wskazaliśmy programowi, którego obiektu użyć, kompilator znalazł to niejawnie.

Rozważmy teraz toInt(y). Tym razem kompilator szuka niejawnego argumentu ttvtypu TypeToValue[Succ[_0], Int](ponieważ yjest typu Succ[_0]). Znajduje funkcję succToInt, która może zwrócić obiekt odpowiedniego typu ( TypeToValue[Succ[_0], Int]) i ocenia ją. Ta funkcja sama przyjmuje niejawny argument ( v) typu TypeToValue[_0, Int](to znaczy, TypeToValuegdzie pierwszy parametr typu ma o jeden mniej Succ[_]). Kompilator dostarcza _0ToInt(tak jak zostało to zrobione przy ocenie toInt(z)powyżej) i succToIntkonstruuje nowy TypeToValueobiekt z wartością 1. Ponownie, należy zauważyć, że kompilator udostępnia wszystkie te wartości w sposób niejawny, ponieważ nie mamy do nich jawnego dostępu.

Sprawdzam twoją pracę

Istnieje kilka sposobów sprawdzenia, czy obliczenia na poziomie typu działają zgodnie z oczekiwaniami. Oto kilka podejść. Zrób dwa typy Ai B, które chcesz zweryfikować, są równe. Następnie sprawdź, czy następująca kompilacja:

Alternatywnie możesz przekonwertować typ na wartość (jak pokazano powyżej) i sprawdzić wartości w czasie wykonywania. Np. assert(toInt(a) == toInt(b)), Gdzie ajest typu Ai bjest typu B.

Dodatkowe zasoby

Pełny zestaw dostępnych konstrukcji można znaleźć w sekcji typów podręcznika referencyjnego skali (pdf) .

Adriaan Moors ma kilka artykułów naukowych na temat konstruktorów typów i powiązanych tematów z przykładami ze scala:

Apocalisp to blog z wieloma przykładami programowania na poziomie typów w scali.

ScalaZ to bardzo aktywny projekt, który zapewnia funkcjonalność rozszerzającą interfejs API Scala przy użyciu różnych funkcji programowania na poziomie typu. To bardzo ciekawy projekt, który cieszy się dużym zainteresowaniem.

MetaScala jest biblioteką na poziomie typów dla Scali, zawierającą metatypy dla liczb naturalnych, wartości logicznych, jednostek, HList itp. Jest to projekt Jespera Nordenberga (jego blog) .

Michid (blog) ma kilka świetnych przykładów programowania typu poziom w Scali (z drugiej odpowiedź):

Debasish Ghosh (blog) również ma kilka odpowiednich postów:

(Prowadziłem badania na ten temat i oto czego się dowiedziałem. Nadal jestem w tym nowy, więc proszę wskazać wszelkie nieścisłości w tej odpowiedzi.)

dsg
źródło
12

Oprócz innych linków tutaj, są też moje posty na blogu na temat programowania meta na poziomie typu w Scali:

michid
źródło
Chciałem tylko podziękować za interesujący blog; Śledzę to od jakiegoś czasu, a zwłaszcza ostatni wspomniany powyżej post pogłębił moje zrozumienie ważnych właściwości, jakie powinien mieć system typów dla języka zorientowanego obiektowo. Więc dziękuję!
Zach Snow