Typ zależny - Dependent type
Systemy typu |
---|
Pojęcia ogólne |
Główne kategorie |
Pomniejsze kategorie |
W informatyce i logiki , o rodzaj zależny jest typem, którego definicja zależy od wartości. Jest to nakładająca się cecha teorii typów i systemów typów . W intuicjonistycznej teorii typów typy zależne są używane do kodowania kwantyfikatorów logicznych, takich jak „dla wszystkich” i „istnieje”. W funkcjonalnych językach programowania, takich jak Agda , ATS , Clojure , Coq , F* , Epigram i Idris , typy zależne pomagają zredukować błędy, umożliwiając programiście przypisywanie typów, które dodatkowo ograniczają zestaw możliwych implementacji.
Dwa typowe przykłady typów zależnych to funkcje zależne i pary zależne. Zwracany typ funkcji zależnej może zależeć od wartości (nie tylko typu) jednego z jej argumentów. Na przykład funkcja, która przyjmuje dodatnią liczbę całkowitą, może zwrócić tablicę o długości , gdzie długość tablicy jest częścią typu tablicy. (Zauważ, że różni się to od polimorfizmu i programowania generycznego , z których oba zawierają typ jako argument.) Para zależna może mieć drugą wartość, której typ zależy od pierwszej wartości. Trzymając się przykładu tablicy, para zależna może być używana do parowania tablicy z jej długością w sposób bezpieczny dla typu.
Typy zależne zwiększają złożoność systemu typów. Decydowanie o równości typów zależnych w programie może wymagać obliczeń. Jeśli dowolne wartości są dozwolone w typach zależnych, wówczas decydowanie o równości typów może obejmować podjęcie decyzji, czy dwa dowolne programy dają ten sam wynik; dlatego sprawdzanie typu może stać się nierozstrzygalne .
Historia
W 1934 roku Haskell Curry zauważył, że typy używane w typowanym rachunku lambda i jego odpowiedniku w logice kombinatorycznej mają ten sam wzorzec, co aksjomaty w logice zdań . Idąc dalej, dla każdego dowodu w logice była odpowiednia funkcja (termin) w języku programowania. Jednym z przykładów Curry'ego była zgodność między prostym rachunkiem lambda a logiką intuicjonistyczną .
Logika predykatów jest rozszerzeniem logiki zdań, dodając kwantyfikatory. Howard i de Bruijn rozszerzyli rachunek lambda, aby dopasować się do tej potężniejszej logiki, tworząc typy dla funkcji zależnych, które odpowiadają „dla wszystkich”, oraz pary zależne, które odpowiadają „istnieje”.
(Z powodu tej i innych prac Howarda propozycje-jako typy są znane jako korespondencja Curry-Howard ).
Formalna definicja
Π typ
Mówiąc ogólnie, typy zależne są podobne do typu indeksowanej rodziny zbiorów. Bardziej formalnie, mając dany typ w uniwersum typów , można mieć rodzinę typów , która przypisuje każdemu terminowi typ . Mówimy, że typ B(a) zmienia się wraz z a .
Funkcja którego typ wartości powrotu zależy od jej argumentu (tzn nie jest stała codomain ) to funkcja zależna i typ Jest to funkcja zależy od rodzaju produktu , PI typu lub zależny rodzaj funkcji . Z rodziny typów możemy skonstruować typ funkcji zależnych , których terminami są funkcje , które przyjmują wyraz i zwracają wyraz w . W tym przykładzie typ funkcji zależnej jest zwykle zapisywany jako lub
Jeśli jest funkcją stałą, odpowiedni zależny typ produktu jest równoważny zwykłemu typowi funkcji . Oznacza to, że jest krytycznie równa, gdy B nie zależy od x .
Nazwa „typ pi” pochodzi od idei, że mogą one być postrzegane jako kartezjański produkt typów. PI-ów może być również rozumiana jako modeli z kwantyfikatorami .
Na przykład, jeśli piszemy dla n -krotek liczb rzeczywistych , to byłby typ funkcji, która przy danej liczbie naturalnej n , zwraca krotkę liczb rzeczywistych o rozmiarze n . Zwykła przestrzeń funkcji powstaje jako szczególny przypadek, gdy typ zakresu w rzeczywistości nie zależy od danych wejściowych. Np. jest typem funkcji od liczb naturalnych do liczb rzeczywistych, które zapisuje się jak w typowanym rachunku lambda.
Dla bardziej konkretny przykład, biorąc jako równa rodziny bez znaku liczby całkowite od 0 do 255, (te można dopasować w 8-bitowym lub 1 bajt) i B (a) = X do 256 dowolna X „s , następnie przechodzi w iloczyn X 0 × X 1 × X 2 × ... × X 253 × X 254 × X 255 właśnie dlatego, że skończony zbiór liczb całkowitych od 0 do 255 ostatecznie zatrzymałby się na wspomnianych granicach, w wyniku skończona kodomena funkcji zależnej.
Σ typ
Podwójnego zależnej od rodzaju produktów jest zależny od typu pary , zależne od typu suma , Sigma typ lub (złudzenia) zależne od rodzaju produktu . Typy sigma można również rozumieć jako kwantyfikatory egzystencjalne . Kontynuując powyższy przykład, jeżeli we wszechświecie typów istnieje typ i rodzina typów , to istnieje typ pary zależnej . (Alternatywne zapisy są podobne do tych z typów Π).
Typ pary zależnej oddaje ideę pary uporządkowanej, w której typ drugiego terminu jest zależny od wartości pierwszego. Jeśli wtedy i . Jeśli B jest funkcją stałą, to typ pary zależnej staje się (oceniająco równy) typem produktu , czyli zwykłym iloczynem kartezjańskim .
Dla bardziej konkretnym przykładzie, Biorąc znowu równa rodziny bez znaku liczby całkowite od 0 do 255, a B (a) ponownie równa X do 256 bardziej arbitralny X jest, następnie nakładanych na suma X 0 + X 1 + X 2 + ... + X 253 + X 254 + X 255 z tych samych powodów, co z przeciwdziedziną funkcji zależnej.
Przykład jako kwantyfikacja egzystencjalna
Niech będzie jakiś typ i niech . Według korespondencji Curry-Howard , B może być interpretowane jako orzeczenie logiczne na warunkach A . Dla danego , czy typ B(a) jest zamieszkały wskazuje, czy a spełnia ten predykat. Korespondencję można rozszerzyć na kwantyfikację egzystencjalną i pary zależne: zdanie jest prawdziwe wtedy i tylko wtedy, gdy typ jest zamieszkany.
Na przykład jest mniejsze lub równe wtedy i tylko wtedy, gdy istnieje inna liczba naturalna taka, że m + k = n . W logice to stwierdzenie jest skodyfikowane przez kwantyfikację egzystencjalną:
Układy kostki lambda
Henk Barendregt opracował sześcian lambda jako środek do klasyfikowania systemów typów wzdłuż trzech osi. Każdy z ośmiu rogów wynikowego diagramu w kształcie sześcianu odpowiada systemowi typów, z po prostu typowanym rachunkiem lambda w najmniej wyrazistym rogu i rachunkiem konstrukcji w najbardziej wyrazistym. Trzy osie odpowiadają kostka trzech rozszerzonych z prosto wpisany lambda rachunku: dodatkiem typu zależnych dodanie polimorfizm, a dodanie większych kinded typu konstruktorów (funkcje od rodzaju do rodzajów, na przykład). Kostka lambda jest dalej uogólniana przez systemy czystego typu .
Teoria typu zależnego pierwszego rzędu
System czystych typów zależnych pierwszego rzędu, odpowiadający szkieletowi logicznemu LF , jest uzyskiwany przez uogólnienie typu przestrzeni funkcyjnej prostego typu rachunku lambda na zależny typ produktu.
Teoria typu zależnego drugiego rzędu
System typów zależnych drugiego rzędu uzyskuje się przez umożliwienie kwantyfikacji nad konstruktorami typu. W tej teorii operator iloczynu zależnego obejmuje zarówno operator prostego typu rachunku lambda, jak i łącznik systemu F .
polimorficzny rachunek lambda wyższego rzędu typu zależnego
System wyższego rzędu rozciąga się na wszystkie cztery formy abstrakcji z kostki lambda : funkcje od terminów do terminów, typy na typy, terminy na typy i typy na terminy. System ten odpowiada rachunku konstrukcji, których pochodna, rachunek konstrukcji indukcyjnych jest podstawowym systemem asystenta dowodu Coq .
Równoczesny język programowania i logika
Korespondencji Curry-Howard oznacza, że typy mogą być konstruowane, który wyraża dowolnie skomplikowanych obiektów matematycznych. Jeśli użytkownik może dostarczyć konstruktywny dowód, że typ jest zamieszkały (tj. że istnieje wartość tego typu), kompilator może sprawdzić dowód i przekonwertować go na wykonywalny kod komputerowy, który oblicza wartość poprzez wykonanie konstrukcji. Funkcja sprawdzania dowodu sprawia, że języki pisane w sposób zależny są blisko spokrewnione z asystentami dowodu . Aspekt generowania kodu zapewnia potężne podejście do formalnej weryfikacji programu i kodu przenoszącego dowody , ponieważ kod pochodzi bezpośrednio z mechanicznie zweryfikowanego dowodu matematycznego.
Porównanie języków z typami zależnymi
Język | Aktywnie rozwijany | Paradygmat | Taktyka | Warunki dowodowe | Sprawdzanie zakończenia | Rodzaje mogą zależeć od | Wszechświaty | Dowód nieistotności | Ekstrakcja programu | Ekstrakcja usuwa nieistotne terminy |
---|---|---|---|---|---|---|---|---|---|---|
Ada 2012 | tak | Tryb rozkazujący | tak | Tak (opcjonalnie) | ? | Dowolny termin | ? | ? | Ada | ? |
Agda | tak | Czysto funkcjonalny | Niewiele/ograniczone | tak | Tak (opcjonalnie) | Dowolny termin | Tak (opcjonalnie) | Dowód nieistotnych argumentów Dowód nieistotnych twierdzeń | Haskell , JavaScript | tak |
ATS | tak | Funkcjonalna/imperatywna | Nie | tak | tak | Warunki statyczne | ? | tak | tak | tak |
Cayenne | Nie | Czysto funkcjonalny | Nie | tak | Nie | Dowolny termin | Nie | Nie | ? | ? |
Gallina ( Coq ) |
tak | Czysto funkcjonalny | tak | tak | tak | Dowolny termin | tak | Nie | Haskell , Scheme i OCaml | tak |
Zależne ML | Nie | ? | ? | tak | ? | Liczby naturalne | ? | ? | ? | ? |
F* | tak | Funkcjonalne i konieczne | tak | tak | Tak (opcjonalnie) | Dowolny czysty termin | tak | tak | OCaml , F# i C | tak |
Guru | Nie | Czysto funkcjonalny | hypjoin | tak | tak | Dowolny termin | Nie | tak | kminek | tak |
Idrys | tak | Czysto funkcjonalny | tak | tak | Tak (opcjonalnie) | Dowolny termin | tak | Nie | tak | Tak, agresywnie |
Pochylać się | tak | Czysto funkcjonalny | tak | tak | tak | Dowolny termin | tak | tak | tak | tak |
Matita | tak | Czysto funkcjonalny | tak | tak | tak | Dowolny termin | tak | tak | OCaml | tak |
NuPRL | tak | Czysto funkcjonalny | tak | tak | tak | Dowolny termin | tak | ? | tak | ? |
PVS | tak | ? | tak | ? | ? | ? | ? | ? | ? | ? |
szałwia | Nie | Czysto funkcjonalny | Nie | Nie | Nie | ? | Nie | ? | ? | ? |
dwanaście | tak | Programowanie logiczne | ? | tak | Tak (opcjonalnie) | Dowolny termin (LF) | Nie | Nie | ? | ? |
Zobacz też
Przypisy
- ^ Odnosi się to dojęzyka rdzenia , a nie do żadnej taktyki ( procedura dowodzenia twierdzeń) czy podjęzyka generowania kodu.
- ^ Z zastrzeżeniem ograniczeń semantycznych, takich jak ograniczenia wszechświata
- ^ Static_Predicate dla terminów zastrzeżonych, Dynamic_Predicate dla sprawdzania typu Assert dowolnego terminu w typie rzutowania
- ^ Rozwiązywanie pierścieni
- ^ Opcjonalne wszechświaty, opcjonalny polimorfizm wszechświata i opcjonalne wyraźnie określone wszechświaty
- ^ Wszechświaty, automatycznie wywnioskowane ograniczenia wszechświata (nie to samo, co polimorfizm wszechświata Agdy) i opcjonalnie jawne drukowanie ograniczeń wszechświata
- ^ Został zastąpiony przez ATS
- ^ Ostatni papier Sage i ostatnia migawka kodu są datowane na 2006 rok
Bibliografia
Dalsza lektura
- Martin-Löf, Per (1984). Intuicjonistyczna teoria typów (PDF) . Bibliopolis.
- Nordström, Bengt ; Petersson, Kent; Smith, Jan M. (1990). Programowanie w teorii typów Martina-Löfa: wprowadzenie . Oxford University Press. Numer ISBN 9780198538141.
- Barendregt, H. (1992). „Rachunki lambda z typami” . W Abramsky S.; Gabbay, D.; Maibaum, T. (red.). Podręcznik logiki w informatyce . Oksfordzkie publikacje naukowe .
- McBride, Conor ; McKinna, James (styczeń 2004). „Widok z lewej” . Dziennik Programowania Funkcjonalnego . 14 (1): 69-111. doi : 10.1017/s0956796803004829 .
-
Altenkirch, Thorsten ; McBride, Conor ; McKinna, James (kwiecień 2005). „Dlaczego typy zależne są ważne” (PDF) . Cytowanie dziennika wymaga
|journal=
( pomoc ) - Norell, Ulf (wrzesień 2007). W kierunku praktycznego języka programowania opartego na teorii typów zależnych (PDF) (PhD). Göteborg, Szwecja: Wydział Informatyki i Inżynierii, Chalmers University of Technology. Numer ISBN 978-91-7291-996-9.
- Oury, Nicolas; Swierstra, Wouter (2008). „Potęga Pi” (PDF) . ICFP '08: Materiały 13. międzynarodowej konferencji ACM SIGPLAN nt . Programowania funkcjonalnego . s. 39-50. doi : 10.1145/1411204.1411213 . Numer ISBN 9781595939197.
- Norella, Ulfa (2009). "Programowanie zależne w Agdzie" (PDF) . W Koopman, P.; Plasmeijer, R.; Swierstra, D. (red.). Zaawansowane programowanie funkcjonalne. AFP 2008 . Notatki z wykładów z informatyki. 5832 . Skoczek. s. 230-266. doi : 10.1007/978-3-642-04652-0_5 . Numer ISBN 978-3-642-04651-3.
- Sitnikowski, Boro (2018). Delikatne wprowadzenie do typów zależnych z Idris . Lean publikowanie. Numer ISBN 978-1723139413.