Typ dolny
W teorii typów , teorii w ramach logiki matematycznej , dolnym typem systemu typów jest typ, który jest podtypem wszystkich innych typów.
Tam, gdzie taki typ istnieje, jest często przedstawiany za pomocą symbolu przyczepności do góry (⊥).
Gdy typ bottom jest pusty, funkcja, której typem zwracanym jest bottom, nie może zwrócić żadnej wartości, nawet pojedynczej wartości typu jednostki . W takim języku dolny typ może być zatem znany jako zero lub nigdy . W korespondencji Curry – Howard pusty typ odpowiada fałszowi.
Aplikacje informatyczne
W systemach podtypów dolny typ jest podtypem wszystkich typów. Jest dualny w stosunku do typu top , który obejmuje wszystkie możliwe wartości w systemie.
Jeśli system typów jest prawidłowy , typ dolny jest niezamieszkany, a termin typu dolnego reprezentuje logiczną sprzeczność. W takich systemach zazwyczaj nie ma rozróżnienia między typem dolnym a typem pustym , a terminy mogą być używane zamiennie.
Jeśli dolny typ jest zamieszkały, jego terminy zwykle odpowiadają warunkom błędu, takim jak niezdefiniowane zachowanie, nieskończona rekurencja lub nienaprawialne błędy.
W Bounded Quantification with Bottom Pierce mówi, że „Bot” ma wiele zastosowań:
- W języku z wyjątkami , naturalnym typem dla konstrukcji podbicia jest podniesienie ∈ wyjątek -> Bot i podobnie dla innych struktur sterujących. Intuicyjnie Bot jest typem obliczeń, które nie zwracają odpowiedzi.
- Bot jest przydatny do wpisywania „węzłów liści” polimorficznych struktur danych. Na przykład List(Bot) jest dobrym typem dla nil.
- Bot jest typem naturalnym dla wartości „ zerowego wskaźnika ” (wskaźnika, który nie wskazuje na żaden obiekt) języków takich jak Java: w Javie typ null jest uniwersalnym podtypem typów referencyjnych .
nulljest jedyną wartością typu null; i może być rzutowany na dowolny typ referencyjny. Jednak typ null nie jest typem najniższym, jak opisano powyżej, nie jest podtypeminti innych typów pierwotnych. - System typów obejmujący zarówno Top, jak i Bot wydaje się być naturalnym celem wnioskowania o typie , pozwalając na uchwycenie ograniczeń pominiętego parametru typu za pomocą pary granic: piszemy S<:X<:T, aby oznaczać „wartość X musi leżeć gdzieś pomiędzy S i T.” W takim schemacie całkowicie nieograniczony parametr jest ograniczony od dołu przez Bot, a od góry przez Top.
W językach programowania
Większość powszechnie używanych języków nie ma sposobu na oznaczenie typu dolnego. Istnieje kilka godnych uwagi wyjątków.
W Haskell niezdefiniowanej stałej lub terminom utworzonym za pomocą konstruktora błędów można przypisać dowolny typ. Próba oceny takiego wyrażenia powoduje nieodwracalne przerwanie kodu.
W Common Lisp typ NIL nie zawiera żadnych wartości i jest podtypem każdego typu. Typ o nazwie NIL jest czasami mylony z typem o nazwie NULL , który ma jedną wartość, a mianowicie sam symbol NIL .
W Scali dolny typ jest oznaczony jako Nothing . Oprócz zastosowania do funkcji, które po prostu zgłaszają wyjątki lub w inny sposób nie zwracają normalnie, jest również używany do kowariantnych typów sparametryzowanych . Na przykład List w Scali jest konstruktorem typu kowariantnego, więc List[Nothing] jest podtypem List[A] dla wszystkich typów A. Zatem Nil w Scali , obiekt oznaczający koniec listy dowolnego typu, należy do typu Lista [Nic] .
W Rust dolny typ nazywany jest typem nigdy i jest oznaczony przez ! . Jest obecny w sygnaturze typu funkcji, które gwarantują, że nigdy nie powrócą, na przykład przez wywołanie panic!() lub zapętlenie w nieskończoność. Jest to również rodzaj niektórych słów kluczowych przepływu sterowania, takich jak break i return , które nie generują wartości, ale mimo to można ich używać jako wyrażeń.
Na Cejlonie dolny typ to Nothing . Jest porównywalny do Nothing w Scali i reprezentuje przecięcie wszystkich innych typów, a także pusty zbiór.
W Julii dolny typ to Union{} .
W TypeScript najniższym typem jest nigdy .
W JavaScript z adnotacjami Closure Compiler najniższym typem jest !Null (dosłownie, inny niż null element typu jednostki Null ).
W PHP najniższym typem jest nigdy .
W Pythonie najniższym typem jest typing.NoReturn ( typing.Never od wersji 3.11).
W Kotlinie dolny typ to Nothing .
W D dolny typ to noreturn
W Dart , od wersji 2.12 z dźwiękową aktualizacją bezpieczeństwa , typ Never został wprowadzony jako typ dolny. Wcześniej typem bottom był Null .