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 Lambda
sparametryzowane za pomocą dwóch typów ( S
i T
oba muszą być podtypami Lambda
), trait Lam extends Lambda
sparametryzowane 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 App
przykładu lambda nazębnego, rodzaju eval
realizowana jest w następujący sposób: type eval = S#eval#apply[T]
. Zasadniczo jest to wywołanie eval
typu parametru cechy S
i wywołanie wyniku apply
z parametrem T
. Uwaga, S
na pewno ma eval
typ, ponieważ parametr określa, że jest to podtyp Lambda
. Podobnie, wynik eval
musi mieć apply
typ, 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 A
jest podtypemB
A =:= B
, kompiluje się tylko wtedy, gdy A
jest podtypem B
i B
jest podtypemA
A <%< B
, („widoczny jako”) kompiluje się tylko wtedy, gdy A
jest widoczny jako B
(tj. istnieje niejawna konwersja z A
na 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 null
jako wartości zastępczej podczas wykonywania obliczeń na poziomie wartości przy użyciu pewnego rodzaju zainteresowania:
- np.
val x:A = null
gdzie A
jest 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 A
jest 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 val
jako 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 Nat
i zwraca liczbę całkowitą reprezentującą liczbę naturalną zakodowaną w v
typie. Na przykład, jeśli mamy wartość val x:_3 = null
( null
typu 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, TypeToValue
dla każdego z klas Nat
od _0
do (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ść 1
itp.). Uwaga, TypeToValue
jest parametryzowana przez dwa typy: T
i VT
. T
odpowiada typowi, do którego próbujemy przypisać wartości (w naszym przykładzie Nat
) i VT
odpowiada 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 toInt
w następujący sposób:
def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()
Aby zrozumieć, jak to toInt
dział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 ttv
typu TypeToValue[_0, Int]
(ponieważ z
jest typu _0
). Znajduje obiekt _0ToInt
, wywołuje getValue
metodę 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 ttv
typu TypeToValue[Succ[_0], Int]
(ponieważ y
jest 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, TypeToValue
gdzie pierwszy parametr typu ma o jeden mniej Succ[_]
). Kompilator dostarcza _0ToInt
(tak jak zostało to zrobione przy ocenie toInt(z)
powyżej) i succToInt
konstruuje nowy TypeToValue
obiekt 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 A
i B
, które chcesz zweryfikować, są równe. Następnie sprawdź, czy następująca kompilacja:
Equal[A, B]
implicitly[A =:= B]
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 a
jest typu A
i b
jest 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.)