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?
type-theory
applied-theory
Tamad Lang
źródło
źródło
Odpowiedzi:
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 :
źródło
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:
Poniższy cytat znajduje się we wstępie do książki Shan's Linguistic Side Effects :
źródło
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.
źródło
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
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 .
źródło
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
źródło