„Dowód to program; okazuje się, że formuła jest typem programu ”

To może być pytanie filozoficzne, ale uważam, że istnieje obiektywna odpowiedź na to pytanie.

Jeśli czytasz artykuł w Wikipedii o Haskell, możesz znaleźć:

Język jest zakorzeniony w spostrzeżeniach Haskella Curry'ego i jego intelektualnych potomków, że „dowód jest programem; formuła, którą dowodzi, jest typem programu”

Teraz pytam: czy to nie dotyczy właściwie wszystkich języków programowania? Jaka funkcja (lub zestaw funkcji) Haskell sprawia, że ​​jest on zgodny z tym stwierdzeniem? Innymi słowy, jakie są zauważalne sposoby, w jakie to stwierdzenie wpłynęło na projekt języka?

Podstawowa koncepcja ma zastosowanie uniwersalne w pewien sposób, tak, ale rzadko w użyteczny sposób.

Na początek, z punktu widzenia teorii typów, zakłada się, że języki „dynamiczne” mają jeden typ, który zawiera (między innymi) metadane dotyczące natury wartości, którą widzi programista, w tym także tego, co te dynamiczne języki nazwaliby sam „typ” (co koncepcyjnie nie jest tym samym). Wszelkie takie dowody mogą być nieciekawe, więc ta koncepcja dotyczy głównie języków ze statycznymi systemami typu.

Ponadto wiele języków, które rzekomo mają „statyczny system typów”, należy w tym kontekście uznać za dynamiczne, ponieważ zezwalają one na kontrolę i konwersję typów w czasie wykonywania. W szczególności oznacza to każdy język z wbudowaną, domyślną obsługą „refleksji” lub podobny. Na przykład C #.

Haskell jest niezwykły pod względem ilości informacji, jakich oczekuje od typu - w szczególności funkcje nie mogą zależeć od żadnej innej wartości niż te określone jako argumenty. Z drugiej strony w języku ze zmiennymi zmiennymi globalnymi każda funkcja może (potencjalnie) sprawdzać te wartości i odpowiednio zmieniać zachowanie. Tak więc funkcję Haskella z typem A -> Bmożna uznać za miniaturowy program udowadniający, że Aimplikuje B; równoważna funkcja w wielu innych językach mówi nam tylko, że Aimplikuje to każdy stan globalny w zasięgu B.

Zauważ, że chociaż Haskell obsługuje takie elementy, jak odbicia i typy dynamiczne, użycie takich funkcji musi być wskazane w podpisie typu funkcji; podobnie do wykorzystania stanu globalnego. Żadna z tych opcji nie jest dostępna domyślnie.

Istnieją również sposoby na załamanie rzeczy w Haskell, np. Poprzez zezwolenie na wyjątki czasu wykonywania lub użycie niestandardowych operacji prymitywnych dostarczonych przez kompilator, ale wiążą się one z dużym oczekiwaniem, że zostaną użyte z pełnym zrozumieniem w sposób, który wygrał ” t uszkodzić znaczenie kodu zewnętrznego. Teoretycznie to samo można powiedzieć o innych językach, ale w praktyce z większością innych języków zarówno trudniej jest osiągnąć coś bez „oszukiwania”, jak i mniej niechętnie „oszukiwać”. I oczywiście w prawdziwych „dynamicznych” językach cała sprawa pozostaje bez znaczenia.

Pomysł ten może być znacznie szerszy niż w Haskell.

Masz rację, że korespondencja Curry-Howard jest bardzo ogólna. Warto zapoznać się nieco z jego historią: http://en.wikipedia.org/wiki/Curry-Howard_correspondence

Zauważysz, że jak pierwotnie sformułowano, ta korespondencja dotyczyła w szczególności intuicyjnej logiki z jednej strony, a po prostu typowego rachunku lambda (STLC) z drugiej.

Klasyczny Haskell - albo z wersji 98, albo nawet wcześniejszej, bardzo ściśle przestrzegał STLC, i w przeważającej części było bardzo proste, bezpośrednie tłumaczenie między dowolnym wyrażeniem w Haskell i odpowiednim terminem w STLC (rozszerzone o rekurencję i kilka prymitywnych typów). Czyniło to Curry-Howarda bardzo wyraźnym. Dziś dzięki rozszerzeniom takie tłumaczenie jest nieco trudniejsze.

W pewnym sensie więc pytanie brzmi, dlaczego Haskell tak łatwo „zapuszcza się” w STLC. Przychodzą mi na myśl dwie rzeczy:

• Rodzaje W przeciwieństwie do Scheme, który jest także swego rodzaju cukrowym rachunkiem lambda (między innymi), Haskell jest mocno wpisany. Oznacza to, że nie istnieją terminy w klasycznym języku Haskell, które z definicji nie mogą być dobrze wpisanymi terminami w STLC.
• Czystość. Ponownie, w przeciwieństwie do Schematu, ale podobnie jak STLC, Haskell jest czystym, referencyjnie przejrzystym językiem. To jest dość ważne. Języki z efektami ubocznymi mogą być osadzone w językach, które nie powodują skutków ubocznych. Jest to jednak transformacja całego programu, a nie tylko lokalne usuwanie. Aby mieć bezpośrednią korespondencję, konieczne jest, aby zacząć od czysto funkcjonalnego języka.

Istnieje również ważny sposób, w jaki Haskell, podobnie jak większość języków, zawodzi w odniesieniu do bezpośredniego zastosowania korespondencji Curry-Howard. Haskell, jako kompletny język Turinga, zawiera możliwość nieograniczonej rekurencji, a co za tym idzie, braku wypowiedzenia. STLC nie ma operatora punktu stałego, nie jest kompletny w turingu i silnie normalizuje się - co oznacza, że ​​żadna redukcja terminu w STLC nie zakończy się. Możliwość rekurencji oznacza, że ​​można „oszukać” Curry-Howarda. Na przykład let x = x in xma typforall a. a- tzn. ponieważ nigdy nie powraca, mogę udawać, że daje mi wszystko! Ponieważ zawsze możemy to zrobić w Haskell, oznacza to, że nie możemy w pełni „uwierzyć” w żaden dowód odpowiadający programowi Haskell, chyba że mamy osobny dowód, że sam program się kończy.

Linia programowania funkcjonalnego przed Haskellem (zwłaszcza rodzina ML) była wynikiem badań CS koncentrujących się na budowaniu języków, w których można łatwo udowodnić (między innymi) rzeczy, badania bardzo świadome i pochodzące z CH na początek. I odwrotnie, Haskell służył zarówno jako język hosta, jak i inspiracja dla wielu asystentów w trakcie opracowywania, takich jak Agda i Epigram, które są zakorzenione w rozwoju teorii typów, bardzo związanej z rodowodem CH.

W przybliżeniu pierwszego rzędu większość innych (słabo i / lub jednoznacznie) języków nie obsługuje ścisłego rozgraniczenia na poziomie języka między

• propozycja (tj. typ)
• dowód (czyli program pokazujący, jak można skonstruować propozycję z zestawu prymitywów i / lub innych wyższego rzędu konstruktów)

i ścisły związek między nimi. Jeśli już, to najlepsze gwarancje, jakie dają inne takie języki

• biorąc pod uwagę ograniczone ograniczenie danych wejściowych oraz wszystko, co dzieje się w danym momencie w środowisku, możemy wytworzyć wartość z ograniczonym ograniczeniem. (tradycyjne typy statyczne, por. C / Java)
• każda konstrukcja jest tego samego typu (typy dynamiczne, por. ruby ​​/ python)

Zauważ, że według typu odwołujemy się do zdania , a zatem coś opisującego znacznie więcej informacji niż tylko int lub bool . W Haskell istnieje przenikająca kultura funkcji, na którą wpływają tylko jej argumenty - bez wyjątków *.

Aby być nieco bardziej rygorystycznym, ogólną ideą jest to, że poprzez egzekwowanie sztywnego intuicyjnego podejścia do (prawie) wszystkich konstrukcji programu (tj. Możemy tylko udowodnić, że to, co możemy zbudować), i przez ograniczenie zestawu prymitywnych konstrukcji w takim tak jak my

• ścisłe propozycje dla wszystkich prymitywów językowych
• ograniczony zestaw mechanizmów, za pomocą których można łączyć prymitywy

Konstrukcje Haskell bardzo dobrze nadają się do rozumowania o swoim zachowaniu. Jeśli możemy skonstruować dowód (czytaj: funkcję) dowodzący, że to Asugeruje B, ma to bardzo przydatne właściwości:

• to zawsze trzyma (o ile mamy A, możemy skonstruować B)
• Ta implikacja opiera się tylko na Ai nic innego.

co pozwala nam skutecznie wnioskować o niezmiennikach lokalnych / globalnych. Aby wrócić do pierwotnego pytania; Funkcje językowe Haskell, które najlepiej fascynują ten sposób myślenia, to:

• Czystość / segmentacja efektów na wyraźne konstrukcje (efekty są uwzględniane i pisane na maszynie!)
• Wpisz Wnioskowanie / Sprawdzanie w kompilatorach Haskell
• Możliwość osadzenia niezmienników kontroli i / lub przepływu danych w propozycjach / typach, które program zamierza udowodnić: (z polimorfizmem, rodzinami typów, GADT itp.)
• Więzy integralności

Żaden z nich w ogóle nie jest unikalny dla Haskell (wiele z tych pomysłów jest niewiarygodnie starych). Jednak w połączeniu z bogatym zestawem abstrakcji w standardowych bibliotekach (zwykle znajdującym się w klasach typów), różnym słodzeniem na poziomie składni i ścisłym zaangażowaniem w czystość w projektowaniu programów, uzyskujemy język, który w jakiś sposób udaje się być zarówno wystarczająco praktyczny do zastosowań w świecie rzeczywistym , ale jednocześnie łatwiej jest zrozumieć większość tradycyjnych języków.

To pytanie zasługuje na wystarczająco głęboką odpowiedź, a ja nie byłbym w stanie odpowiedzieć sprawiedliwie w tym kontekście. Proponuję przeczytać więcej na temat wikipedii / w literaturze:

• Izomorfizm Curry'ego-Howarda
• Kostka Lambda
• Konstruktywistyczna / intuicyjna teoria typów
• Omówienie obliczeniowego trynitaryzmu Boba Harpera

* NB: Rozmyślam nad / ignoruję niektóre trudniejsze aspekty zanieczyszczeń Haskell (wyjątki, brak rozwiązania itp.), Które tylko skomplikowałyby argument.

Jaka funkcja? System typów (statyczny, czysty, polimorficzny). Dobrym punktem wyjścia są „Twierdzenia Wadlera za darmo”. Zauważalny wpływ na wygląd języka? Typ IO, klasy typów.

Kleene Hierarchia pokazuje nam, że dowody nie są programy.

Pierwsza relacja rekurencyjna to:

R1( Program , Iteration )  Program halts at Iteration.
R2( Theorem , Proof ) Proof proves a Theorem.

Pierwszymi rekurencyjnie wymiennymi relacjami są:

(exists x) R1( Program , x )  Program Halts.
(exists x) R2( Theorem , x)   Theorem is provable.

Tak więc program jest twierdzeniem, a iteracja, przy której program się zatrzymuje, jest jak istniejący dowód, który potwierdza twierdzenie.

Program = Theorem
Iteration = Proof

Kiedy program jest poprawnie utworzony ze specyfikacji, musimy być w stanie udowodnić, że jest on zgodny ze specyfikacją, a jeśli możemy udowodnić, że program spełnia specyfikację, to jest to poprawna synteza programu. Dlatego przeprowadzamy syntezę programu, jeśli udowodnimy, że program jest zgodny ze specyfikacją. Twierdzenie, że program spełnia specyfikację, jest programem w tym sensie, że odnosi się do programu, który jest syntetyzowany.

Fałszywe wnioski Martina Lofa nigdy nie stworzyły żadnych programów komputerowych i zdumiewające jest to, że ludzie wierzą, że jest to metodologia syntezy programów. Nie podano nigdy pełnych przykładów syntetyzowanego programu. Specyfikacja taka jak „wprowadź typ i wyślij program tego typu” nie jest funkcją. Istnieje wiele takich programów i wybranie jednego losowo nie jest funkcją rekurencyjną, a nawet funkcją. To tylko głupia próba pokazania syntezy programu za pomocą głupiego programu, który nie reprezentuje prawdziwego programu komputerowego obliczającego funkcję rekurencyjną.