System typów oparty na naiwnej teorii mnogości

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?

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 $v$$\tau$$\tau$$v = \Phi(v)$$\Phi : \tau \to \tau$$\tau$$T$$f : T \to T$$T$

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.

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 .$\pi$

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ą.

$\forall \alpha.\; \alpha \to \alpha$$U$

$U$$U$$X \to X$$X \in U$$\alpha$

$\forall \alpha.\; \alpha \to \alpha$