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

25

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?

Rehno Lindeque
źródło
5
Blisko powiązane pytanie: Dowody / Programy i propozycje / Rodzaje
Marc Hamann
1
Kolejna powiązana dyskusja: Klasyfikacja Lambda Calculi
Marc Hamann
Znalazłem kolejny fajny artykuł tutaj scientopia.org/blogs/goodmath/2009/11/17/…
Rehno Lindeque
1
W pewnym sensie sprowadza się to do kwestii ontologii. Co to jest zestaw, propozycja itp. Ponadto wiele osób uważa, że ​​typy są również zestawami. Jeśli chcemy być bardziej precyzyjni, możemy rozróżnić małe typy (które są zbiorami) i typy wszechświatowe. Dla miłej lektury, która dotyczy niektórych z tych rzeczy, polecam klasyczny artykuł Martina-Löfa „Intuitionistic Type Theory”
Tobias Raski
1
Ktoś powinien napisać odpowiedź z punktu widzenia teorii typu homotopy.
Robin Green,

Odpowiedzi:

20

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.

Dave Clarke
źródło
Dziękujemy, pierwszy link był szczególnie pomocny! Mark informuje w nim, że istnieje „łączna relacja <” między typami. Czy to oznacza, że ​​wszystkie „zdania” danego typu muszą również zawierać wszystkie „zdania” w typach poniżej? Spodziewałem się, że będzie to przynajmniej „częściowa relacja <” nad typami ....
Rehno Lindeque
1
Kiedy czytam, istnieje całkowity porządek nad atomami, który został wprowadzony jedynie po to, aby zapewnić, że istnieje nieskończona liczba atomów.
Dave Clarke
Och, widzę, że pomyliłem się między „Aksjomatem zrozumienia” i „Aksjomatem nieskończoności” ... Czy typ „nat” (typ wszystkich liczb naturalnych) byłby „typem nieskończonego poziomu 0”?
Rehno Lindeque,
3
„Święta Trójca” naprawdę należy do Lambka. Por. omówienie teorii typów w Lambek i Scott (1986). Słyszałem, że w McGill mówi się o korespondencji Curry-Howarda-Lambka.
Charles Stewart,
@Charles: Zgadzam się, że Lambek jest niedoceniany za swój ogromny wkład, nawet jeśli, o ironio, czytał książkę Lambek i Scott, która przekonała mnie, że „święta trójca” jest fałszywa: rozpada się w obecności potencjalnego nie -zakończenie.
Marc Hamann,