Typy nie są zestawami.
Widzisz, teoria mnogości ma wiele cech, które po prostu nie dotyczą typów i odwrotnie . Na przykład obiekt ma jeden typ kanoniczny. Może to być wystąpienie kilku różnych typów, ale tylko jeden z tych typów został użyty do jego utworzenia. Teoria zbiorów nie ma pojęcia zbiorów „kanonicznych”.
Teoria zbiorów pozwala tworzyć podzestawy w locie , jeśli masz regułę opisującą, co należy do tego podzbioru. Teoria typów na ogół na to nie pozwala. Chociaż większość języków ma Number
typ lub coś podobnego, nie ma takiego EvenNumber
typu, a jego utworzenie nie byłoby proste. To znaczy, dość łatwo jest zdefiniować sam typ, ale wszelkie istniejące, Number
które się zdarzają, nie zostaną magicznie przekształcone w EvenNumber
s.
W rzeczywistości powiedzenie, że można „tworzyć” podzbiory, jest nieco nieuczciwe, ponieważ zestawy są zupełnie innym rodzajem zwierząt. W teorii zbiorów te podzbiory już istnieją , na wszystkie nieskończone sposoby, jak je zdefiniować. W teorii typów zwykle oczekujemy, że będziemy mieć do czynienia ze skończoną (jeśli dużą) liczbą typów w danym momencie. Jedynymi typami, o których mówi się, że istnieją, są te, które faktycznie zdefiniowaliśmy, nie każdy typ, który moglibyśmy zdefiniować.
Zestawy nie mogą zawierać się bezpośrednio lub pośrednio . Niektóre języki, takie jak Python, zapewniają typy o mniej regularnych strukturach (w Pythonie type
typem kanonicznym jest type
i object
jest uważany za przykład object
). Z drugiej strony większość języków nie pozwala typom zdefiniowanym przez użytkownika angażować się w tego rodzaju oszustwa.
Zestawy zwykle mogą się nakładać, ale nie są ze sobą powiązane. Jest to rzadkie w teorii typów, chociaż niektóre języki obsługują ją w postaci wielokrotnego dziedziczenia. Inne języki, takie jak Java, dopuszczają tylko ograniczoną formę tego lub całkowicie go zabraniają.
Pusty typ istnieje (nazywany jest typem dolnym ), ale większość języków go nie obsługuje lub nie uważa go za typ pierwszej klasy. „Typ zawierający wszystkie inne typy” również istnieje (nazywany jest typem górnym ) i jest szeroko obsługiwany, w przeciwieństwie do teorii mnogości.
Uwaga : Jak zauważyli wcześniej niektórzy komentatorzy (zanim wątek został przeniesiony na czat), możliwe jest modelowanie typów za pomocą teorii mnogości i innych standardowych konstrukcji matematycznych. Na przykład można modelować członkostwo typu jako relację, a nie modelować typy jako zestawy. Ale w praktyce jest to o wiele prostsze, jeśli użyjesz teorii kategorii zamiast teorii mnogości. Tak na przykład Haskell modeluje swoją teorię typów.
Pojęcie „podtypu” naprawdę różni się od pojęcia „podzbioru”. Jeśli X
jest podtypem Y
, oznacza to, że możemy zastąpić wystąpienia Y
wystąpieniami, X
a program nadal będzie w pewnym sensie „działał”. Jest to raczej behawioralne niż strukturalne, chociaż niektóre języki (np. Go, Rust, prawdopodobnie C) wybrały ten drugi ze względów wygody, albo dla programisty, albo dla implementacji języka.
a
ib
są członkami tego typu, jak wspomina Killian Forth. Myclass jest izomorficzny w stosunku do rekordów z polamia
ib
typuint
idouble
- możesz wziąć taki rekord i przekształcić go w instancjąmyclass
.