Jakie są praktyczne implikacje teorii typów homotopii w programowaniu?

11

Właśnie zaczynam uczyć się Haskell, po pochodzeniu ze światów JavaScript / Ruby. Natknąłem się na https://github.com/HoTT i książkę Teoria typów homotopii , którą bardzo chętnie czytam.

Będę jednak uczyć się pojęć z matematyki i teorii typów, więc wydaje się, że minie dużo czasu, zanim zrozumiem, co teoria typów homotopii będzie oznaczać dla praktykującego programisty.

Czy mógłbyś opisać wpływ teorii homotopii na praktykę programowania dla laika? Na przykład, czy ułatwi to napisanie niektórych rzeczy? Jeśli tak, jakie rzeczy? A może pozwoli ci robić nowe rzeczy w programowaniu, które wcześniej nie były możliwe? Jeśli tak, jakie rzeczy?

Dzięki, bardzo nie mogę się doczekać, aby owinąć moją głowę na bardziej podstawowym poziomie.

type-theory Lance Pollard
źródło
Spodziewam się, że tak jest i zawsze pozostanie nieodgadnione dla praktykujących programistów. W najlepszym przypadku możemy uzyskać szybsze kompilatory lub magiczne czarne skrzynki, które korzystają z matematyki-fu.
Telastyn
Haha, o tym też myślałem do tej pory. Nadal zastanawiam się, czy to jest odpowiedź, czy jest coś poza tym, co powiedziałeś? Na przykład, czy bazy danych mogłyby z tego skorzystać? Lub coś w tym rodzaju.
Lance Pollard
1
Nie mam pojęcia. Przeczytałem streszczenie i natychmiast wrzuciłem je do wiadra na nieprzeniknione akademickie mumbo-jumbo.
Telastyn
zalecana lektura: Jak wyjaśnić $ {coś} $ {komuś}?
komara
4
@Telastyn: Jeśli pobierzesz książkę w języku portugalskim, będzie ona również nieodgadniona, dopóki nie spróbujesz nauczyć się języka. Po co publicznie potępiać portugalskie książki obraźliwym terminem mumbo-jumbo ? Motywacja Gödla do wprowadzenia prymitywnych funkcji rekurencyjnych była niezwykle akademicka, w szczególności dlatego, że świat nie prowadził nawet żadnych programów w latach 30-tych. Nie sądzę tylko dlatego, że ktoś jest praktykującym programistą, tematy akademickie „zawsze pozostaną nieodgadnione” dla twoich możliwości.
Nikolaj-K

Odpowiedzi:

15

Jedną z potężnych rzeczy, które kompilatory są w stanie wykonać podczas fazy optymalizacji, jest zamiana nieefektywnych reprezentacji na równoważne. Na przykład w Haskell można użyć leniwej listy do obliczenia sumy liczb, ale kompilator GHC Haskell rozpozna, że ​​jest to równoważne z iteracją ze zmienną tymczasową. W ten sposób możesz programować w oparciu o prostą abstrakcję, którą łatwo uzasadnić, podczas gdy twój plik wykonywalny korzysta z reprezentacji lepiej dopasowanej do platformy sprzętowej (i okazuje się, że jest to znacznie trudniejsze do uzasadnienia w skali).

Jednak równoważności znane kompilatorowi są w większości ograniczone do dobrze znanych i zbadanych struktur danych, takich jak łączenie strumieni dla list. Możesz zdefiniować własne ekwiwalenty w kodzie źródłowym (używając pary funkcji konwersji, które składają się na tożsamość w obu kierunkach), ale musisz zastosować je ręcznie, a wybranie odpowiedniego typu we wszystkich miejscach może być trudne. w celu uniknięcia nadmiernej konwersji.

Teraz wyobraźmy sobie świat, w którym można zdefiniować „wyższe typy indukcyjne”, powiedzmy kanoniczną mapę wyszukiwania. Ten typ ma kilka konstruktorów dla różnych rodzajów map: wyszukiwanie binarne, AVL, czerwono-czarny, Trie, Patricia itp. Wraz z typowymi konstruktorami danych definiujesz również typ równoważności przechwytujący możliwie wiele konwersji między tymi reprezentacjami, gdzie różne konwersje oferują różne wymiary wydajności (tj. czas vs. pamięć).

Co by było, gdyby kompilator był w stanie użyć tego pojęcia do przezroczystego przepisywania reprezentacji map, w taki sam sposób, w jaki można to dziś zrobić w przypadku łączenia list? Tymczasem w kodzie możesz pracować z konstrukcją, która jest najprostsza do uzasadnienia (i ułatwia pracę z dowodami, jeśli jesteś w takim środowisku). Może to zabrzmieć jak abstrakcyjne interfejsy z wieloma implementacjami, ale obejmuje swobodę wyboru dowolnej implementacji i umożliwia kompilatorowi przejrzyste zastępowanie innej w razie potrzeby, bez wpływu na znaczenie programu.

HoTT daje nam podstawy teoretyczne do uzasadnienia tego fantazyjnego mechanizmu przepisywania i tych bogato zdefiniowanych typów, ponieważ promuje pojęcie równoważności jako równoważności równości. Dopiero okaże się, jak to faktycznie się sprawdzi w praktyce, ale daje nam teoretyczne ramy, na których można oprzeć przyszłe prace.

John Wiegley
źródło