Dlaczego typ pustki C nie jest analogiczny do typu pusta / dolna?

Wikipedia, jak również inne źródła, które znalazłem, wskazują voidtyp C jako typ jednostki, a nie typ pusty. Uważam to za mylące, ponieważ wydaje mi się, że voidlepiej pasuje do definicji typu pustego / dolnego.

• voidO ile wiem, nie zamieszkują żadnych wartości .
• Funkcja z typem zwracanym void określa, że ​​funkcja nic nie zwraca, a zatem może wywołać tylko pewien efekt uboczny.
• Wskaźnik typu void*jest podtypem wszystkich innych typów wskaźników. Również konwersje do iz void*C są niejawne.

Nie jestem pewien, czy ostatni punkt ma jakąkolwiek wartość jako argument za voidbyciem pustym typem, ponieważ void*jest to mniej więcej szczególny przypadek z niewielkim stosunkiem void.

Z drugiej strony voidsam nie jest podtypem wszystkich innych typów, co, o ile wiem, jest wymogiem, aby typ był typem dolnym.

W C voidjest używany do wielu niepowiązanych rzeczy. W zależności od tego, do czego jest używany, może to oznaczać typ jednostki, typ pusty lub coś innego.

Gdy voidjest używany samodzielnie (w przeciwieństwie do void*wskaźnika do pustki), jest to typ jednostki, tj. Typ z jedną wartością. voidMówi się, że funkcje, które zwracają , „nic nie zwracają”, ale tak naprawdę oznacza to, że nie zwracają żadnych informacji. Zwracają bitów informacji, co oznacza, że ​​zwracają wartość typu, który zawiera odrębne wartości, tj. Typ jednostki.$0$$2^0 = 1$

To nie jest pusty typ: funkcja zwracająca pusty typ nie może zwrócić wartości, ponieważ nie ma żadnej wartości tego typu. Funkcja, której typ zwracany jest pusty, może zapętlać na zawsze, przerywać program lub zgłaszać wyjątek ( longjmp) (lub w inny sposób zapewniać brak powrotu, np. Poprzez przeniesienie kontroli do innego wątku lub procesu przy użyciu funkcjonalności wykraczającej poza standardowy C). Aby utrzymać zamieszanie, w C zwykle używa się voidzamiast pustego typu (C nie ma pustego typu).

voidTen wymaga bitów przechowywania. Ponieważ C nalega, aby każdy obiekt zajmował całą niezerową liczbę bajtów pamięci, zabronione jest tworzenie obiektu typu i istnieje specjalna składnia zwracająca wartość ( instrukcja z pominiętą wartością). Nie ma składni, która daje wartość typu , ale ta wartość jest dostępna za każdym razem, gdy zwraca funkcję, której typ zwracany jest .$0$voidvoidreturnvoidvoid

C nie ma typu dolnego w tym sensie, że dopuszcza dowolny możliwy typ. Nawet niekompletne typy określają ogólny charakter jego wartości, np. Wskaźniki, struktury, związki lub funkcje. Ale void*jest wskaźnikiem do każdego typu non-funkcyjny: to najmniejszy element algebry typów obiektów wskaźnik, czyli jest to dolna typ obiektu wskaźnik. W przeciwieństwie do ogólnego przypadku T*, gdzie Tjest jakiś zakaz typ void, void*nie jest typem wskaźników do wartości typu void, ale rodzaj wskaźników do wartości nieokreślonego typu.

Nazwa „pusty typ” może być myląca. Oznacza to, jak sam twierdzisz, że typ nie zawiera żadnych wartości . „Pusty” nie odnosi się do żadnych indywidualnych wartości typu, odnosi się do typu jako całości, traktowanego jako zbiór możliwych wartości. Więc to nie nie powiedzieć coś w stylu „funkcja powrocie voidnie zwraca informacji”, ale „nie istnieje żadnej wartości typu ⊥”.

Oznacza to funkcję, której typ wyniku nigdy nie⊥ może zostać zakończony. Gdyby się skończyło, musiałbym zwrócić wartość , ale cóż, taka wartość nie istnieje.⊥

Oznacza to również, że nie można nawet omówić, ile informacji zawiera wartość pustego typu, ponieważ nie ma takiej wartości. (Lub, jeśli wolisz, bezsensowne stwierdzenie, takie jak: „każda wartość pustego typu zawiera dokładnie 35093658 bitów informacji” jest bez wątpienia prawdziwe.) Przydatne (choć niezupełnie poprawne) jest myślenie o ⊥wartościach zawierających nieskończoną ilość informacji.

Podczas gdy funkcja C z „typem zwrotu” voidwyraźnie może zwrócić, ale nie daje żadnych informacji w jej wartości zwracanej. Cóż, właśnie to charakteryzuje typ jednostki: jego wartości nie zawierają żadnych informacji, ponieważ istnieje tylko jedna taka wartość (stąd zawsze możesz powiedzieć, jaka będzie wartość zwracana, nawet bez zawracania głowy wywołaniem funkcji).

Cytując Conora McBride'a (w transliteracji do C):

voidoznacza „nudne”. Oznacza nudny typ, który zawiera jedną rzecz, także nudną. Porównując jeden element nudnego typu z innym, nie można nic ciekawego zyskać, ponieważ nie można się niczego nauczyć o elemencie nudnym, poświęcając mu trochę uwagi.

To bardzo różni się od pustego typu [...]. Pusty typ jest bardzo ekscytujący, ponieważ jeśli ktoś kiedykolwiek da ci wartość należącą do niego, wiesz, że już nie żyjesz w Niebie i że wszystko, czego chcesz, jest twoje.