System typów oparty na naiwnej teorii mnogości

11

Jak rozumiem, w informatyce typy danych nie są oparte na teorii zbiorów z powodu takich rzeczy jak paradoks Russella, ale tak jak w prawdziwych językach programowania nie możemy wyrazić tak złożonych typów danych jak „zestaw, który nie zawiera siebie”, czy możemy powiedzmy, że w praktyce typ jest nieskończonym zbiorem jego członków, w których członkostwo w instancji jest definiowane przez liczbę cech właściwych dla tego typu / zestawu (istnienie pewnych właściwości, metod)? Jeśli nie, jaki byłby kontrprzykład?

Nutel
źródło
1
Paradoks Russella nie ma z tym bezpośredniego związku.
Andrej Bauer,

Odpowiedzi:

11

Głównym powodem unikania zbiorów w semantyce typów jest to, że typowy język programowania pozwala nam definiować dowolne funkcje rekurencyjne. Dlatego, bez względu na znaczenie typu, musi on mieć właściwość punktu stałego. Jedynym zestawem z taką właściwością jest zestaw singletonów.

Mówiąc ściślej, rekurencyjnie zdefiniowana wartość typu (gdzie zwykle jest typem funkcji) jest zdefiniowana równaniem stałego punktu gdzie może być dowolnym programem. Jeśli jest interpretowane jako zbiór , to spodziewalibyśmy się, że każdy ma ustalony punkt. Ale jedynym zestawem z tą właściwością jest singleton.τ τ v = Φ ( v ) Φ : τ τ τ T f : T T Tvττv=Φ(v)Φ:τττTf:TTT.

Oczywiście można również zdać sobie sprawę, że winowajcą jest logika klasyczna. Jeśli pracujesz z intuicyjną teorią zbiorów, to spójne jest założenie, że istnieje wiele zbiorów z właściwością punktu stałego. W rzeczywistości zostało to wykorzystane do określenia semantyki języka programowania, patrz na przykład

Alex Simpson, Adekwatność obliczeniowa dla typów rekurencyjnych w modelach intuicyjnej teorii zbiorów, In Annals of Pure and Applied Logic, 130: 207-275, 2004.

Andrej Bauer
źródło
7

Podtyp semantyczny oparty jest na teoretycznej interpretacji typów, przy czym podtyp jest podzbiorem. Oryginalna praca , jak sądzę, jest dziełem Castagny w kontekście CDuce języka przetwarzania XML. Typy odpowiadają zestawom dokumentów XML. Od tego czasu pomysły zostały ponownie zastosowane do rachunku - rachunek różniczkowy i całkowy oraz obiektów i klas .π

Dave Clarke
źródło
1
Są prekursory Castagna. Dawno temu ludzie używali już relacji podzbiorów do modelowania podtypów w modelach PER. Tam typ odpowiada częściowej relacji równoważności (PER), a podtyp jest po prostu włączeniem takich relacji.
Andrej Bauer,
4

Z kilkoma wyjątkami (jednym, który przytacza Dave Clarke), prosta semantyka zestawów teoretycznych typów jest trudna w użyciu. Powodem jest to, że abstrakcja danych nie gra zbyt dobrze z semantyką teoretyczną.

α.ααU

[[α.αα]]=ΠXU.XX

UUXXXUα

α.αα

Neel Krishnaswami
źródło
Neel, nie sądzę, żeby ta odpowiedź miała sens. Jeśli semantyka języka jest standardową semantyką w stylu F, to kompilator może dobrze zoptymalizować optymalizację, w oparciu o system typów. Jeśli semantyka jest semantyką teoretyczną, optymalizacja byłaby nieuzasadniona. Model, którego używasz dla typów, nie wchodzi w to.
Sam Tobin-Hochstadt,
Sam, nie rozumiem twojego punktu widzenia: brzmi to tak, jakbyś całkowicie się ze mną zgadzał! Standardowa semantyka zestawów teoretycznych nie może udowodnić, że jedynym mieszkańcem tego typu jest tożsamość, więc potrzebujesz innej semantyki.
Neel Krishnaswami
1
@Neel: opisany problem utrzymuje się nawet po odejściu od zestawów. Rozwiązaniem nie jest zmiana kategorii zbiorów o coś innego, ale odmienne modelowanie parametryczności. Mianowicie, należy zastosować parametryczną relację , jak jestem pewien. Ale wtedy wszystko działa równie dobrze w zestawach, jeśli się nie mylę. „Jedynym” problemem w zestawach jest brak punktów stałych (zarówno na poziomie wartości rekurencyjnych, jak i typów rekurencyjnych).
Andrej Bauer,
1
Ach, chyba rozumiem, dlaczego mylę ciebie i Sama! Z pewnością nie mam na myśli sugerowania, że ​​stosowanie naiwnego modelu teoretycznego nie jest rozsądne, po prostu ten model często daje nieprzydatne odpowiedzi - dlatego powiedziałem „trudny w użyciu”, a nie „zły”. Możesz oczywiście użyć zestawów do zbudowania użytecznego modelu (tj. Relacyjnie), ale wtedy nie interpretujemy typów zestawów jako zestawów w sposób sugerowany w pytaniu. (Ponadto, jak wiadomo, przy impredykatywnym polimorfizmie nie ma naiwnego modelu, ale parametryczność jest nadal znacząca predykcyjnie.)
Neel Krishnaswami
1
Myślę, że twoja uwaga dotyczy zgodności między semantyką - semantyka teoretyczna nie pasuje do polimorfizmu w stylu Systemu F, ponieważ ma niewyrażalnych mieszkańców. Ale to nie jest argument przeciwko semantyce teoretycznej, tylko stwierdzeniu, że nasza semantyka powinna się zgodzić. Jeśli nasz język pozwala nam wyrazić funkcje, o których mówisz (jak na przykład Rakieta maszynowa), możemy chcieć semantyki opartej na teorii zbiorów.
Sam Tobin-Hochstadt