Typ dolny - Bottom type
W teorii typów , teorii w ramach logiki matematycznej , dolny typ to typ, który nie ma wartości. Jest również nazywany typem zerowym lub pustym i jest czasami oznaczany symbolem pinezki w górę (⊥).
Funkcja, której typ zwracany to bottom, nie może zwrócić żadnej wartości, nawet typu jednostki o zerowym rozmiarze . Dlatego funkcja, której typ zwracany jest typem dolnym, nie może zwrócić. W korespondencji Curry-Howard dolny typ odpowiada fałszowi.
Aplikacje informatyczne
W systemach podtypów typ dolny jest podtypem wszystkich typów. (Jednak odwrotność nie jest prawdą — podtyp wszystkich typów niekoniecznie jest typem dolnym.) Jest używany do reprezentowania typu zwracanego funkcji, która nie zwraca wartości: na przykład taka, która zapętla się w nieskończoność, sygnalizuje wyjątek lub wyjścia.
Ponieważ typ dolny jest używany do wskazania braku normalnego zwrotu, zazwyczaj nie ma wartości. Kontrastuje z typem top , który obejmuje wszystkie możliwe wartości w systemie, oraz typem jednostki , który ma dokładnie jedną wartość.
Typ dna jest często używany do następujących celów:
- Aby zasygnalizować, że funkcja lub obliczenie są rozbieżne ; innymi słowy, nie zwraca wyniku dzwoniącemu. (Nie musi to oznaczać, że program się nie kończy; podprogram może zakończyć się bez powrotu do swojego wywołującego lub zakończyć za pomocą innych środków, takich jak kontynuacja .)
- W połączeniu z interpretacją korespondencji Curry'ego-Howarda dna jako „fałszu”, daje to obliczeniową interpretację logiki niekonstruktywnej w zakresie operatorów przepływu sterowania .
- Jako wskazanie błędu; to użycie występuje głównie w językach teoretycznych, w których rozróżnienie błędów jest nieistotne. Produkcyjne języki programowania zwykle używają innych metod, takich jak typy opcji (w tym oznakowane wskaźniki ) lub obsługa wyjątków .
W Bounded Quantification with Bottom Pierce mówi, że „Bot” ma wiele zastosowań:
- W języku z wyjątkami naturalnym typem konstrukcji podbicia jest podniesienie ∈ wyjątek -> Bot , podobnie dla innych struktur kontrolnych. Intuicyjnie, Bot jest tutaj rodzajem 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 zera.
- Bot jest naturalnym typu na „ zerowy wskaźnik wartości” (wskaźnik, który nie jest skierowany do każdego obiektu) języków takich jak Java: w Javie , typ zerowy jest uniwersalnym podtyp typów referencyjnych .
nulljest jedyną wartością typu null; i może być rzutowany na dowolny typ referencyjny. Jednak typ null nie spełnia wszystkich właściwości typu dolnego, jak opisano powyżej, ponieważ typy dolne nie mogą mieć żadnych możliwych wartości, a typ null ma valuenull. - System typów obejmujący zarówno Top, jak i Bot wydaje się być naturalnym celem dla wnioskowania o typie , umożliwiając przechwycenie ograniczeń dotyczących pominiętego parametru typu przez parę granic: piszemy S<:X<:T jako „wartość X musi leżeć gdzieś pomiędzy S i T”. W takim schemacie całkowicie nieograniczony parametr jest ograniczony poniżej przez Bot, a powyżej przez Top.
W językach programowania
Najczęściej używane języki nie mają możliwości wyraźnego oznaczenia pustego typu. Jest kilka godnych uwagi wyjątków.
Od Haskell2010 Haskell obsługuje puste typy danych. W ten sposób pozwala na definicję data Empty(bez konstruktorów). Typ Emptynie jest całkiem pusty, ponieważ zawiera programy niekończące i undefinedstałą. undefinedStała jest często używany, gdy chcesz coś mieć pustą typu, ponieważ undefinedpasuje do każdego typu (tak jest rodzajem „podtyp” wszystkich typów) i próbując ocenić undefinedspowoduje program, aby anulować, dlatego nigdy nie zwraca odpowiedź .
W Common Lisp symbol NIL, oprócz innych zastosowań, jest również nazwą typu, który nie ma wartości. Jest uzupełnieniem, Tktórego jest topowym typem. Typ named NILjest czasami mylony z typem named NULL, który ma jedną wartość, a mianowicie NILsam symbol .
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 sparametryzowanych typów kowariantnych . Na przykład Scala's List jest konstruktorem typu kowariantnego, więc jest to podtyp dla wszystkich typów A. Tak więc Scala's , obiekt do oznaczania końca listy dowolnego typu, należy do typu .
List[Nothing]List[A]NilList[Nothing]
W Rust typ dolny nazywany jest typem Never i jest oznaczony przez !. Jest obecny w sygnaturze typu funkcji, które gwarantują, że nigdy nie zwrócą, na przykład przez wywołanie panic!()lub zapętlenie w nieskończoność. Jest to również typ pewnych słów kluczowych przepływu sterowania, takich jak breaki return, które nie generują wartości, ale mimo to są użyteczne jako wyrażenia.
Na Cejlonie typ dolny to Nothing. Jest porównywalna do NothingScali i reprezentuje przecięcie wszystkich innych typów, a także pusty zbiór.
W Julii typ dolny to Union{}.
W TypeScript dolny typ to never.
W języku JavaScript z adnotacjami Closure Compiler dolny typ to !Null(dosłownie niepusty element członkowski Null typu unit ).
W PHP dolny typ to never.
W Pythonie dolny typ to typing.NoReturn.
W Kotlinie dolny typ to Nothing.
W Elm dolny typ to Never.