Codzienne zastosowania teorii typów

Chcę zrozumieć teorię typów, ale najpierw muszę wiedzieć, jak ją zastosować. Czy może być więcej nieoczywistych zastosowań teorii typów poza systemami typu w programowaniu? Czy mogą być inne aplikacje, powiedzmy w profilowaniu osobowości i tym podobne?

Możesz być zainteresowany w pracach nad Ceptre , w wyniku badań doktorskiej z Chris Martens , który używa typu teorii do interaktywnego opowiadania. Poniżej cytowana jest teza :

Interaktywne opowiadanie historii łączy głębokie pomysły obliczeniowe z bogatą historią i zabawą ludzkości, zapewniając ważny kontekst dla narzędzi i języków do zbudowania. Jednocześnie formalne języki specyfikacji oferują paletę technik reprezentacji i wnioskowania zwykle zarezerwowanych do analizy języków programowania i złożonych systemów dedukcyjnych. Teza ta łączy problemy w dziedzinie interaktywnego opowiadania z rozwiązaniami w formalnej specyfikacji.

W szczególności badamy narrację ze strukturalnego punktu widzenia i zauważamy, że alternatywne ścieżki narracji odgrywają rolę uzupełniającą w stosunku do jednoczesnych linii czasu. Logika liniowa zapewnia narzędzia reprezentacyjne niezbędne do zbadania tej struktury, a rozszerzając korespondencję na dowody i konstrukcję dowodu, znajdujemy zestaw możliwości obliczeniowych. Prezentujemy trzy wysiłki na rzecz realizacji tych możliwości: (1) wykorzystanie programowania logiki liniowej do generowania narracji; (2) nowy język programowania do tworzenia interaktywnych narracji, gier i symulacji; oraz (3) techniki określania i potwierdzania właściwości programu na poziomie projektu.

Uważamy, że liniowe programowanie logiczne, wzbogacone o minimalne rozszerzenie jego logicznej semantyki, umożliwia szeroki zakres idiomów programowania i kodowania domen. Jako dowód podajemy pięć analiz przypadków, w tym symulację społeczną, przygodowe gry walki i gry planszowe. Aby wesprzeć rozumowanie dotyczące poprawności projektu, przedstawiamy techniki ustalania i sprawdzania niezmienników programu, a także dowód rozstrzygalności w celu automatycznego sprawdzenia tych niezmienników pod kątem dużego fragmentu języka.

Odkrycia te pokazują, że logika liniowa jest owocnym językiem reprezentacji, który ma służyć jako podstawa do modelowania i wykonywania interaktywnych światów, i zachęcają do przyszłych badań nad wykorzystaniem metod teoretycznych dla systemów kreatywnych.

Istnieje ciekawe zastosowanie teorii typów w językoznawstwie. Zobacz na przykład dzieła językowe Chung-chieh Shan lub Christian Rétoré .

Cytowane poniżej opis retore za książki na gramatyk kategorialnych:

Ta książka jest współczesnym i wszechstronnym wprowadzeniem do gramatyki kategorialnej w tradycji logicznej zapoczątkowanej dziełem Lambka. Prowadzi studentów i badaczy przez podstawowe wyniki w tej dziedzinie, zapewniając współczesne dowody wielu klasycznych twierdzeń, a także oryginalne najnowsze osiągnięcia. Liczne przykłady i ćwiczenia ilustrują motywacje i zastosowania tych wyników z punktu widzenia językowego, obliczeniowego i logicznego. Rachunek Lambka i jego warianty oraz odpowiadające im gramatyki stanowią sedno tych notatek z wykładów. Rozdział poświęcony jest kluczowej funkcji tych kategorycznych gramatyk: ich bardzo eleganckiemu interfejsowi składniowo-semantycznemu. Ponadto dostosowujemy siatki logiczne liniowe do tych obliczeń, ponieważ zapewniają wydajne algorytmy parsowania, jak na przykład w parserze Graala.

Poniższy cytat znajduje się we wstępie do książki Shan's Linguistic Side Effects :

W niniejszym dokumencie opisano przypadki pozornej niekompozycji w językach naturalnych do przypadków w językach programowania. Ma kształt klepsydry: zaczynam w § 1 od podejścia do interfejsu składni-semantyki, które pomaga nam budować kompozytorskie teorie semantyczne. Podejście to polega na narysowaniu analogii między obliczeniowymi skutkami ubocznymi w językach programowania a tym, co nazywam przez analogię językowymi skutkami ubocznymi w językach naturalnych.

To połączenie może przynieść korzyści zarówno informatykom, jak i językoznawcom, ale koncentruję się tutaj na drugim kierunku transferu technologii. Kontynuacje były przydatne w leczeniu obliczeniowych skutków ubocznych. W § 2 przedstawiam nowy metalajmniejszy ciąg kontynuacji semantyki.

Metjęzyk, który wprowadzam, jest przydatny do analizy zarówno języków programowania, jak i języków naturalnych. Dla intuicji badam pierwsze zastosowanie w §3, a następnie wskazuję zalety tego leczenia w §4.

Przechodząc do języka naturalnego w §5, szczegółowo opisuję, w jaki sposób ta perspektywa pomogła Chrisowi Barkerowi i ja studiować wiązanie i krzyżowanie, a także pytania i wyższość. Użyłem również kontynuacji do badania kwantyfikatora i zakresu wh-nieokreślonego, szczególnie w języku chińskim mandaryńskim, ale tutaj jest tylko miejsce, aby naszkicować te dalsze zmiany, w §6.

Ze względu na korespondencję Curry-Howarda typy można interpretować jako zdania, a zdania jako typy.

W rezultacie teoria typów ma zastosowanie dosłownie w każdej dziedzinie, która używa logiki formalnej do swoich dowodów. Może to być weryfikacja obwodu, analiza rzeczywista, logika symboliczna, geometria itp.

Na przykład niektóre narzędzia do automatycznego sprawdzania proofów działają zgodnie z tą zasadą: sprawdzają ważność proofu poprzez sprawdzanie określonego terminu w określonym systemie typów. Tester sprawdzający LF jest oparty na tym podejściu, podobnie jak HOL Light . Jako przykładową aplikację wykorzystano LF do sprawdzenia dowodów bezpieczeństwa pamięci niezaufanego kodu. Zaletą korzystania z tego rodzaju weryfikatora jest to, że wdrożenie może być bardzo proste, dzięki czemu możemy uzyskać dużą pewność, że wdrożenie jest prawidłowe. Zobacz np. Następujący artykuł:

Podstawowe warcaby kontrolne z małymi świadkami . Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.

Ciekawym artykułem wyjaśniającym zastosowania typów zależnych jest Moc pi , która pokazuje, jak Agda może być wykorzystana do rozwiązania interesujących problemów.

Innym dobrym przykładem jest użycie typów zależnych do kontroli zasobów. Dobrym przykładem jest interfejs API zarządzania plikami Effects of Idris . Na przykład funkcja odczytu linii z pliku ma następujący typ

readLine  : { [FILE_IO (OpenFile Read)] } Eff String

co oznacza, że ​​ta funkcja ma zastosowanie tylko wtedy, gdy otwarty jest plik. Lista w nawiasach klamrowych wskazuje, które efekty są dostępne. W tym przypadku mamy tę funkcję, że wymaga otwarcia pliku do odczytu.

Więcej informacji na temat biblioteki efektów można znaleźć tutaj .

Kolejną aplikacją jest użycie współzależnych typów do współbieżności, jak poinformował twórca Idris w następnym artykule .

jak wspomniano w odpowiedzi jmite, logika / teoria wyższego rzędu w weryfikacji obwodów / sprzętu / elektroniki istnieje już od dziesięcioleci i jest obecnie tak rutynowa, że ​​nawet nie zauważyła / nie uważa się za „aplikację” po pozornie znacznym wysiłku przeniesienia w ~ 1990, choć nadal jest to aktywny obszar badań. istnieje również wiele zastosowań Coq i jego logiki typu, w szczególności do weryfikacji obwodów / sprzętu / elektroniki, od logiki bramek niskiego poziomu do znacznie wyższych struktur / podsystemów zamówień / poziomu. oto kilka kluczowych referencji

• Logika wyższego rzędu i weryfikacja sprzętu / Melham (1993!)

• Twierdzenie o logice wyższego rzędu Dowodzenie i jego zastosowania / Claeson, Gordon

• Konstruowanie prawidłowych obwodów: weryfikacja funkcjonalnych aspektów specyfikacji sprzętu za pomocą typów zależnych / Brady, Mckinna, Hammond

• Obwody certyfikujące w teorii typów / grimal

• Coquet: biblioteka Coq do weryfikacji sprzętu / Braibant