Dobra, chodźmy jeden po drugim.
Wartości
Wartości to konkretne dane, które programy oceniają i żonglują. Nic szczególnego, niektóre przykłady mogą być
1
true
"fizz buzz foo bar"
Rodzaje
Dobrym opisem typu jest „klasyfikator wartości”. Typ to trochę informacji o tym, jaka będzie ta wartość w czasie wykonywania, ale wskazany w czasie kompilacji.
Na przykład, jeśli powiesz mi to e : bool
w czasie kompilacji, a ja będę wiedział, że e
jest to true
albo w false
czasie wykonywania, nic więcej! Ponieważ typy tak ładnie klasyfikują wartości, możemy wykorzystać te informacje do określenia podstawowych właściwości Twojego programu.
Na przykład, jeśli kiedykolwiek zobaczę, jak dodajesz e
i e'
kiedy e : int
i e' : String
, to wiem, że coś jest nie tak! W rzeczywistości mogę to oflagować i zgłosić błąd w czasie kompilacji, mówiąc: „Hej, to nie ma żadnego sensu!”.
Bardziej wydajny system typów pozwala na bardziej interesujące typy, które klasyfikują bardziej interesujące wartości. Rozważmy na przykład jakąś funkcję
f = fun x -> x
To całkiem jasne f : Something -> Something
, ale co to powinno Something
być? W systemie typu nudnego musielibyśmy określić coś arbitralnego Something = int
. W bardziej elastycznym systemie typów można by powiedzieć
f : forall a. a -> a
To znaczy „dla każdego a
, f
odwzorowuje a
na a
”. Wykorzystajmy to f
bardziej ogólnie i piszmy ciekawsze programy.
Co więcej, kompilator sprawdzi, czy rzeczywiście spełnia on podany przez nas klasyfikator, jeśli f = fun x -> true
wtedy wystąpi błąd, a kompilator to powie!
Więc jako tldr; typ jest ograniczeniem czasowym kompilacji wartości, jakie wyrażenie może mieć w czasie wykonywania.
Typ Konstruktor
Niektóre typy są powiązane. Na przykład lista liczb całkowitych jest bardzo podobna do listy ciągów znaków. To prawie tak, jak sort
dla liczb całkowitych jest prawie jak sort
dla ciągów. Możemy wyobrazić sobie rodzaj fabryki, która buduje te prawie te same typy, uogólniając ich różnice i budując je na żądanie. Taki jest konstruktor typów. To trochę jak funkcja od typów do typów, ale trochę bardziej ograniczona.
Klasycznym przykładem jest ogólna lista. Konstruktor typów dla to tylko ogólna definicja
data List a = Cons a (List a) | Nil
Teraz List
jest funkcja, która mapuje typ a
na listę wartości tego typu! Wydaje mi się, że w Javie są to „klasy ogólne”
Parametry typu
Parametr typu to typ przekazywany do konstruktora typu (lub funkcji). Podobnie jak na poziomie wartości, powiedzielibyśmy, że foo(a)
ma parametr a
tak jak List a
parametr typu a
.
Rodzaje
Rodzaje są trochę trudne. Podstawową ideą jest to, że niektóre typy są podobne. Na przykład, mamy wszystkie prymitywne typy w Javie int
, char
, float
..., które zachowują się tak, jakby one mają taką samą „typem”. Z wyjątkiem sytuacji, gdy mówimy o klasyfikatorach dla samych typów, nazywamy je klasyfikatorami. Więc int : Prim
, String : Box
, List : Boxed -> Boxed
.
Ten system podaje ładne konkretne reguły dotyczące tego, jakiego rodzaju typów możemy używać, podobnie jak typy rządzą wartościami. Bez wątpienia byłoby to nonsensowne
List<List>
lub
List<int>
W Javie List
musi być zastosowany do konkretnego typu, aby mógł być używany w ten sposób! Jeśli spojrzymy na ich rodzaje List : Boxed -> Boxed
i odtąd Boxed -> Boxed /= Boxed
, powyższy jest miłym błędem!
Przez większość czasu tak naprawdę nie myślimy o rodzajach i po prostu traktujemy je jako „zdrowy rozsądek”, ale w przypadku bardziej wyszukanych systemów typów warto o tym pomyśleć.
Mała ilustracja tego, co mówiłem do tej pory
value : type : kind : ...
true : bool : Prim : ...
new F() : Foo : Boxed : ...
Lepsze czytanie niż Wikipedia
Jeśli jesteś zainteresowany tego typu rzeczami, zdecydowanie polecam zainwestowanie dobrego podręcznika. Teoria typów i ogólnie PLT są dość rozległe i bez spójnej bazy wiedzy, którą ty (lub przynajmniej ja) możesz wędrować bez dostania się gdzieś przez miesiące.
Dwie z moich ulubionych książek to
- Rodzaje i język programowania - Ben Pierce
- Praktyczne podstawy języków programowania - Bob Harper
Obie są doskonałymi książkami, które przedstawiają to, o czym właśnie mówiłem, i wiele więcej w pięknych, dobrze wyjaśnionych szczegółach.
int
w Javie składa się z zestawu 2 ^ 64 różnych wartości. Analogia z zestawami załamuje się, gdy w grę wchodzą podtypy, ale jest to wystarczająco dobra intuicja początkowa, zwłaszcza gdy weźmie się pod uwagę algebraiczne typy danych (np. Połączenie dwóch typów może zawierać dowolny element dowolnego z tych typów; jest to połączenie tych zbiorów) .Są one właściwie zdefiniowane przez sztywne, akademickie wsparcie matematyczne, zapewniając mocne stwierdzenia na temat tego, czym są, jak działają i co jest gwarantowane.
Ale programiści w dużej mierze nie muszą tego wiedzieć. Muszą zrozumieć pojęcia.
Wartości
Zacznijmy od wartości, ponieważ wszystko buduje się stamtąd. Wartości to dane używane w obliczeniach. W zależności od podejścia są to wartości, które wszyscy znają: 42, 3.14, „Jak teraz brązowa krowa”, rekord personelu dla Jenny w księgowości itp.
Inne interpretacje wartości są symbolami . Większość programistów rozumie te symbole jako „wartości” wyliczenia.
Left
iRight
są symbolami wyliczeniaHandedness
(ignorując oburęcznych ludzi i ryby).Bez względu na implementację wartości są różnymi rzeczami, z którymi język współpracuje przy wykonywaniu obliczeń.
Rodzaje
Problem z wartościami polega na tym, że nie wszystkie obliczenia są zgodne z prawem dla wszystkich wartości.
42 + goat
to naprawdę nie ma sensu.W tym miejscu wchodzą typy. Typy to metadane, które definiują podzbiory wartości. Powyższy
Handedness
wyliczenie jest dobrym przykładem. Ten typ mówi „tylkoLeft
iRight
może być tutaj użyty”. Pozwala to programom bardzo wcześnie ustalić, że niektóre operacje spowodują błąd.Innym praktycznym zastosowaniem do rozważenia jest to, że pod maską komputery pracują z bajtami. Bajt 42 może oznaczać liczbę 42 lub znak * lub Jenny z działu księgowości. Typy również (w praktyce, nie tyle teoretyczne) pomagają zdefiniować kodowanie podstawowej kolekcji bajtów używanych przez komputery.
Rodzaje
I tutaj zaczynamy trochę tam iść. Więc jeśli język programowania ma zmienną, która odnosi się do typu, jaki on ma typ ?
Na przykład w Javie i C # ma typ
Type
(który ma typType
, który ma ... i tak dalej). Taka jest koncepcja rodzaju . W niektórych językach możesz zrobić trochę bardziej użyteczne rzeczy ze zmienną Type niż Java i C #. Gdy to się dzieje, staje się przydatna, aby powiedzieć „Chcę wartość, która jest typem, ale jest też kilka rodzaju zIEnumerable<int>
”. Ta-da! RodzajeWiększość programistów może wymyślić takie ograniczenia, jak Java i C #. Zastanów się
public class Foo<T> where T: IComparable{}
. W języku z rodzajamiT: kindOf(IComparable)
deklaracja zmiennej staje się legalna; nie tylko specjalna rzecz, którą możesz zrobić w deklaracjach klas i funkcji.Typ Konstruktory
Być może nic dziwnego, że konstruktory typów są po prostu konstruktorami typów . „Ale w jaki sposób skonstruować typ? Rodzaje prostu są .”. Eh ... nie bardzo.
Nic dziwnego, że dość trudno jest zbudować wszystkie użyteczne podzbiory wartości, których użyje każdy program komputerowy. Konstruktory typów pomagają programistom „budować” te podzbiory w znaczący sposób.
Najbardziej powszechne przykład konstruktora typ jest tablica definicji:
int[4]
. Tutaj określasz4
konstruktor typów, który wykorzystuje tę wartość do zbudowania tablicyint
z 4 wpisami. Jeśli podasz inny typ danych wejściowych, uzyskasz inny typ danych wyjściowych.Generics to kolejna forma konstruktora typów, przyjmująca inny typ danych wejściowych.
W wielu językach istnieje konstruktor typów,
P -> R
który buduje typ reprezentujący funkcję, która przyjmuje typP
i zwraca typR
.Teraz kontekst określi, czy „funkcja zwracająca typ” jest konstruktorem typów, czy nie. Z mojego (co prawda ograniczonego) doświadczenia wynika, że wiersz brzmi „czy możesz używać tego typu w czasie kompilacji?” Tak? Konstruktor typów. Nie? Po prostu funkcja.
Wpisz parametr
Pamiętasz więc parametry przekazane konstruktorom typów? Są one powszechnie znane jako parametry typu, ponieważ powszechną formą konstruktora typu jest
Type[param]
lubType<param>
.źródło
*
, a konstruktor typu (z jednym argumentem) ma rodzaj* -> *
. Ograniczenia takie jak(Num a) => a
(oznaczające „każdy typ,a
który jest instancjąNum
klasy”) same w sobie nie są rodzajami. TypekNum
nie jest sam w sobie „rodzaju”, ale ma swój* -> Constraint
. Trudno mi powiązać koncepcję „rodzaju” Haskella (która, jak zakładam, jest ściśle związana z rodzajami w teorii typów?), Z podanymi przez ciebie przykładami.:kind
polecenie ghci daje rodzajNum
as* -> Constraint
. To może być specyficzne dla GHC, nie wiem.