Prawidłowa terminologia w teorii typów: typy, konstruktory typów, rodzaje / rodzaje i wartości

W odpowiedzi na poprzednie pytanie rozpoczęła się krótka debata na temat poprawnej terminologii dla niektórych konstruktów. Ponieważ nie znalazłem pytania (innego niż to lub tamto , co nie jest całkiem właściwe), aby odpowiedzieć na to jasno, tworzę to nowe.

Wątpliwe terminy i ich relacje to: typ, konstruktor typu, parametr typu, rodzaje lub sortowania oraz wartości .

Sprawdziłem także wikipedię pod kątem teorii typów, ale to też nie wyjaśniło zbyt wiele.

Dlatego w celu uzyskania dobrej odpowiedzi referencyjnej i sprawdzenia własnego zrozumienia:

• Jak te rzeczy są właściwie zdefiniowane?
• Jaka jest różnica między każdą z tych rzeczy?
• Jak są ze sobą powiązane?

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 : boolw czasie kompilacji, a ja będę wiedział, że ejest to truealbo w falseczasie 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 ei e'kiedy e : inti 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 Somethingbyć? 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, fodwzorowuje ana a”. Wykorzystajmy to fbardziej 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 -> truewtedy 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 sortdla liczb całkowitych jest prawie jak sortdla 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 Listjest funkcja, która mapuje typ ana 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 atak jak List aparametr 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 Listmusi być zastosowany do konkretnego typu, aby mógł być używany w ten sposób! Jeśli spojrzymy na ich rodzaje List : Boxed -> Boxedi 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.

Jak te rzeczy są właściwie zdefiniowane?

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. Lefti Rightsą symbolami wyliczenia Handedness(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 + goatto naprawdę nie ma sensu.

W tym miejscu wchodzą typy. Typy to metadane, które definiują podzbiory wartości. Powyższy Handednesswyliczenie jest dobrym przykładem. Ten typ mówi „tylko Lefti Rightmoż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 typ Type, 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 z IEnumerable<int>”. Ta-da! Rodzaje

Wię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 rodzajami T: 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ślasz 4konstruktor typów, który wykorzystuje tę wartość do zbudowania tablicy intz 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 -> Rktóry buduje typ reprezentujący funkcję, która przyjmuje typ Pi zwraca typ R.

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]lub Type<param>.