Związek między teorią typów Russelliana a układami typów

Niedawno zdałem sobie sprawę, że istnieje jakaś zależność między teorią typów Russelliana a układami typów, jak np. W Haskell. W rzeczywistości niektóre zapisy typów w Haskell wydają się mieć prekursory w teorii typów. Ale, IMHO, motywacją Russella w 1908 roku było uniknięcie paradoksu Russella i nie jestem pewien, w jaki sposób ma to związek z systemami typów w informatyce.

Czy paradoks Russella w takiej czy innej formie jest czymś, o co musielibyśmy się martwić, na przykład, gdybyśmy nie mieli dobrego systemu pisma w danym języku?

`` Teoria typów '' w sensie języków programowania i Russella są ze sobą ściśle powiązane. W rzeczywistości współczesna dziedzina teorii typów zależnych ma na celu zapewnienie konstruktywnych podstaw matematyki. W przeciwieństwie do teorii mnogości większość badań w dziedzinie teorii typów matematyka jest wykonywana w asystentach dowodowych, takich jak Coq, NuPRL lub Agda. Jako takie, dowody wykonane w tych systemach są nie tylko „sformalizowane”, ale w rzeczywistości w pełni formalne i sprawdzone maszynowo. Stosując taktykę i inne techniki automatyzacji dowodów, staramy się to udowodnić systemy „wysokiego poziomu” i tym samym przypominają nieformalną matematykę, ale ponieważ wszystko jest sprawdzane, mamy znacznie lepsze gwarancje poprawności.

Zobacz tutaj

Typy w zwykłych językach programowania są zwykle bardziej ograniczone, ale meta teoria jest taka sama.

Coś podobnego do paradoksu Russella jest głównym problemem w teorii typów zależnych. W szczególności mając

Type : Type

zwykle prowadzi do sprzeczności. Coq i podobna praca poprzez zagnieżdżanie wszechświatów

Type_0 : Type_1

ale w Coq domyślnie liczby te są niejawne, ponieważ zwykle nie mają znaczenia dla programisty.

W niektórych systemach (Agda, Idris) reguła typu jest włączana za pomocą flagi kompilacji. To sprawia, że ​​logika jest niespójna, ale często ułatwia programowanie / sprawdzanie eksploracji.

Paradoks Russella okazjonalnie pojawia się nawet w bardziej popularnych językach. Na przykład w Haskell możliwe jest kodowanie paradoksu Russella łączącego impredykatywność z przypadkiem typu otwartego, co pozwala budować rozbieżne warunki bez rekurencji nawet na poziomie typu. Haskell jest `` niespójny '' (gdy jest interpretowany jako logika w zwykły sposób), ponieważ obsługuje zarówno rekurencję na poziomie typu, jak i wartości, nie wspominając o wyjątkach. Niemniej jednak ten wynik jest dość interesujący.

Masz rację co do motywacji Russella. Jego paradoks nęka wszystkie teorie zbiorów, które dopuszczają nieograniczone rozumienie aksjomatów, w wyniku czego: dowolna funkcja zdań określa zbiór, mianowicie te wszystkich bytów, które spełniają tę funkcję. Wśród teorii lub opartych na zestawach, które miały tę wadę, znalazła się naiwna teoria zbiorów Cantora i system Grundgesetze Frege'a (konkretnie: aksjomat 5).

Ponieważ typy są uważane za specjalne rodzaje zestawów, jeśli nie zostanie zachowana ostrożność, podobny paradoks może wkraść się do systemu typów. Mimo to nie jestem świadomy istnienia systemów typów, które spotkałyby taki los. Pamiętam tylko wczesne próby Kościoła do sformułowania rachunku lambda w latach 30., które okazały się niespójne (paradoks Kleene-Rosser), ale nie wynikało to z typów ani nie było związane z paradoksem Russella.

Aktualizacja : Zobacz odpowiedź Philipa, aby uzyskać rzeczywistą odpowiedź na twoje pytanie.

Ponieważ wspominasz o Pythonie, pytanie nie jest czysto teoretyczne. Dlatego staram się dać szersze spojrzenie na typy. Rodzaje są różne dla różnych ludzi. Zebrałem co najmniej 5 różnych (ale powiązanych) pojęć typów:

1. Systemy typów są systemami logicznymi i teoriami zestawów.

2. System typów wiąże typ z każdą obliczoną wartością. Badając przepływ tych wartości, system typów próbuje udowodnić lub zapewnić, że nie wystąpią żadne błędy typu.

3. Typ to klasyfikacja identyfikująca jeden z różnych typów danych, takich jak wartość rzeczywista, liczba całkowita lub wartość logiczna, która określa możliwe wartości dla tego typu; operacje, które można wykonać na wartościach tego typu; znaczenie danych; oraz sposób przechowywania wartości tego typu

4. Abstrakcyjne typy danych pozwalają na abstrakcję danych w językach wysokiego poziomu. ADT są często implementowane jako moduły: interfejs modułu deklaruje procedury odpowiadające operacjom ADT. Ta strategia ukrywania informacji umożliwia zmianę implementacji modułu bez zakłócania programów klienckich.

5. Implementacje języka programowania wykorzystują typy wartości do wybrania miejsca potrzebnego na wartości oraz algorytmów operacji na wartościach.

Cytaty pochodzą z Wikipedii, ale w razie potrzeby mogę podać lepsze referencje.

Typy-1 powstały z pracy Russela, ale dziś nie są one jedynie ochroną przed paradoksami: język maszynopisany w teorii typów homotopii to nowy sposób kodowania matematyki w formalnym, zrozumiałym dla maszyny języku, i nowy sposób rozumienia podstaw przez ludzi matematyki. („Stary” sposób to kodowanie przy użyciu aksjomatycznej teorii zbiorów).

Rodzaje 2-5 powstały w programowaniu z kilku różnych potrzeb: aby uniknąć błędów, sklasyfikować dane, z którymi współpracują projektanci i programiści, zaprojektować duże systemy i odpowiednio zaimplementować języki programowania.

Systemy typów w C / C ++, Ada, Java, Python nie powstały z pracy Russel lub chęci uniknięcia błędów. Powstały z potrzeby opisania różnych rodzajów danych (np. „Nazwisko jest ciągiem znaków, a nie liczbą”), zmodularyzowania projektu oprogramowania i optymalnego wyboru reprezentacji niskiego poziomu dla danych. Te języki nie mają typów-1 ani typów-2. Java zapewnia względne bezpieczeństwo przed błędami nie poprzez udowodnienie poprawności programu za pomocą systemu typów, ale przez staranne zaprojektowanie języka (bez arytmetyki wskaźników) i systemu wykonawczego (maszyna wirtualna, weryfikacja kodu bajtowego). System typów w Javie nie jest systemem logicznym ani teorią zbiorów.

Jednak system pisma w języku programowania Agda jest nowoczesną odmianą systemu pisma Russela (opartego na późniejszych pracach lub Per Martin-Lof i inni matematycy). System typów w Agdzie jest zaprojektowany do wyrażania matematycznych właściwości programu i potwierdzania tych właściwości, jest to system logiczny i teoria mnogości.

Nie ma tu czarno-białego rozróżnienia: między wieloma językami. Na przykład system typów języka Haskell ma swoje korzenie w twórczości Russela, może być postrzegany jako uproszczony system Agdy, ale z matematycznego punktu widzenia jest niespójny (wewnętrznie sprzeczny), jeśli jest postrzegany jako system logiczny lub teoria zestawów.

Jednak jako teoretyczny pojazd do ochrony programów Haskell przed błędami działa całkiem dobrze. Możesz nawet używać typów do kodowania niektórych właściwości i ich dowodów, ale nie wszystkie właściwości można zakodować, a programista może nadal naruszać sprawdzone właściwości, jeśli użyje zniechęconych brudnych hacków.

System czcionek Scala jest jeszcze bardziej oddalony od pracy Russela i doskonałego języka dowodowego Agdy, ale nadal ma swoje korzenie w twórczości Russela.

Jeśli chodzi o sprawdzanie właściwości języków przemysłowych, których systemy typów nie zostały zaprojektowane do tego celu, istnieje wiele podejść i systemów.

Aby uzyskać ciekawe, ale różne podejścia, zobacz projekt badawczy Coq i Microsoft Boogie. Coq polega na teorii typów w celu generowania programów imperatywnych z programów Coq. Boogie opiera się na adnotacjach programów imperatywnych o właściwościach i udowadnianiu tych właściwości za pomocą twierdzenia twierdzenia Z3, stosując zupełnie inne podejście niż Coq.