Związek między teorią typów Russelliana a układami typów
12
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.
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.
Dziękuję za szczegółową odpowiedź - jeśli chodzi o dowód, wciąż nie ma narzędzi do udowodnienia poprawności programów w imperatywnych językach, takich jak C ++ lub Java, prawda? Chciałbym położyć rękę na jednym z nich ... Zdaję sobie sprawę, że to kompletna styczna. Wiem o Coq i Agdzie, ale nie wydawały się być odpowiednimi narzędziami do udowodnienia poprawności programów napisanych w C ++ lub Javie.
Frank
3
jest kilka narzędzi. Kilka dla C, wiele dla Javy i mnóstwo dla Ady. Zobacz na przykład: Dlaczego (Java, C, Ada), Krakatoa (Java) lub SPARK (podzbiór Ada z bardzo dobrym oprzyrządowaniem). Jednak w przypadku C ++ nie tak bardzo. Możesz być także zainteresowany YNot (Coq DSL).
Philip JF
3
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.
Dzięki za odpowiedź. Prawdopodobnie istnieją alternatywy dla typów a-la-Russell, aby uniknąć paradoksu Russella. Czy którekolwiek z tych alternatywnych rozwiązań miałoby coś interesującego w tworzeniu języków komputerowych? Typy mundane są bardzo przydatne do jasnego określania umów między częściami kodu, a nawet wcześniej, aby w ogóle nadać semantykę programom. Czy istniałaby inna semantyka, którą można uzyskać za pomocą czegoś innego niż typy? (Nie mam pojęcia, co by to było :-)
Frank
1
Tak, wiele alternatyw (NF Quine'a, ZFC itp.), Ale nie widzę żadnych bezpośrednich powiązań między fundamentalnym kryzysem a językami programowania. Jeśli weźmiesz pod uwagę teorię typów Martina Lofa jako język programowania, może istnieć jakiś związek sięgający wstecz do intuicji. Jeśli chodzi o semantykę języków programowania, istnieje kilka podstawowych języków, takich jak PDL (Propositional Dynamic Logic), które mają semantykę Kripke (lub możliwych światów). Ale typy wydają mi się tak fundamentalne, że mogą być po prostu za kulisami :)
Hunan Rostomyan
1
Ale typy są w pewnym sensie niepotrzebne: chcesz ich i potrzebujesz, ale nie chciałbyś ich określać (stąd, IMHO, dlaczego mamy systemy wnioskowania typów w językach takich jak Haskell lub Ocaml (uwielbiam te języki)). Na drugim końcu spektrum Python jest bardzo intuicyjny i przyjemne (i wydajne pod względem czasu kodowania) nie trzeba się zbytnio przejmować typami w tym języku. Może wnioskowanie typu jest najlepsze z obu światów - ale tak mówi inżynier. Właśnie śniłem na jawie, że matematyka może wnieść inną ważną koncepcję (jak typy) do informatyki :-)
Frank
1
@Frank Za każdym razem, gdy używam języka bez typów statycznych (głównie Ruby), nie znoszę tego doświadczenia, ponieważ nienawidzę możliwych do uniknięcia błędów w czasie wykonywania. Więc wydaje się, że to głównie kwestia gustu. Zgadzam się, że potężne wnioskowanie o typach może dać ci to, co najlepsze z obu światów. Prawdopodobnie dlatego tak bardzo lubię Scalę.
Raphael
Nie jestem przekonany, że brak „typów automatycznych” typów prowadzi do błędów w czasie wykonywania, jak sugerujesz :-) Nigdy nie miałem problemu w Pythonie.
Frank
3
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:
Systemy typów są systemami logicznymi i teoriami zestawów.
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.
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
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.
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.
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.
źródło
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:
Systemy typów są systemami logicznymi i teoriami zestawów.
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.
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
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.
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.
źródło