Czy są typy typów? (Jakie są dokładnie typy?)

Dużo czytałem o systemach typów i takie i rozumiem z grubsza, dlaczego zostały wprowadzone (w celu rozwiązania paradoksu Russela). Rozumiem też z grubsza ich praktyczne znaczenie w językach programowania i systemach sprawdzających. Nie jestem jednak do końca pewien, czy moje intuicyjne wyobrażenie o typie jest prawidłowe.

Moje pytanie brzmi: czy uzasadnione jest twierdzenie, że typy są propozycjami?

Innymi słowy, wyrażenie „n jest liczbą naturalną” odpowiada stwierdzeniu „n ma typ„ liczba naturalna ””, co oznacza, że ​​wszystkie reguły algebraiczne, które dotyczą liczb naturalnych, zachowują się dla n. (Tj. Inny sposób, reguły algebraiczne są wyrażeniami. Te twierdzenia, które są prawdziwe dla liczb naturalnych, są również prawdziwe dla n.)

Czy to oznacza, że ​​obiekt matematyczny może mieć więcej niż jeden typ?

Ponadto wiem, że zestawy nie są równoważne typom, ponieważ nie możesz mieć zestawu wszystkich zestawów. Czy mogę twierdzić, że jeśli zbiór jest obiektem matematycznym podobnym do liczby lub funkcji , typ jest rodzajem obiektu meta-matematycznego i według tej samej logiki rodzaj jest obiektem meta-matematycznym? (w tym sensie, że każda „meta” wskazuje na wyższy poziom abstrakcji ...)

Czy ma to jakiś związek z teorią kategorii?

Kluczową rolą typów jest podział interesujących obiektów na różne wszechświaty, zamiast rozważania wszystkiego, co istnieje w jednym wszechświecie. Początkowo opracowano typy, aby uniknąć paradoksów, ale jak wiadomo, mają wiele innych zastosowań. Typy umożliwiają klasyfikację lub stratyfikację obiektów (patrz wpis na blogu ).

Niektóre działają z hasłem, że zdania są typami , więc twoja intuicja z pewnością ci dobrze służy, chociaż istnieją takie prace, jak Propozycje takie jak [Typy] Steve'a Awodeya i Andreja Bauera, które twierdzą inaczej, a mianowicie, że każdy typ ma powiązaną propozycję. Rozróżnia się to, ponieważ typy mają treść obliczeniową, podczas gdy zdania nie.

Obiekt może mieć więcej niż jeden typ z powodu podtypu i koercji typu .

Typy są na ogół zorganizowane w hierarchię, w której rodzaje odgrywają rolę typów, ale nie posunąłbym się do stwierdzenia, że ​​typy są meta-matematyczne. Wszystko dzieje się na tym samym poziomie - dotyczy to zwłaszcza typów zależnych .

Istnieje bardzo silny związek między typami a teorią kategorii. Rzeczywiście, Bob Harper (cytując Lambka) mówi, że Logika, Języki (tam, gdzie mieszkają typy) i Kategorie tworzą świętą trójcę . Cytowanie:

Te trzy aspekty prowadzą do powstania trzech sekt kultu: logiki, która daje pierwszeństwo dowodom i twierdzeniom; Języki, które dają pierwszeństwo programom i typom; Kategorie, które dają pierwszeństwo mapowaniom i strukturom.

Powinieneś spojrzeć na Korespondencję Curry-Howarda, aby zobaczyć związek między logiką a językami programowania (typy są propozycjami) i kartezjańskimi kategoriami zamkniętymi , aby zobaczyć związek między teorią kategorii.