Jakiej najbardziej intuicyjnej teorii typów zależnych mógłbym się nauczyć?

Jestem zainteresowany uzyskaniem naprawdę solidnego zrozumienia zależnego pisania. Przeczytałem większość TaPL i przeczytałem (jeśli nie w pełni zaabsorbowane) „Typy zależne” w ATTaPL . Przeczytałem również i przejrzałem kilka artykułów na temat pisania zależnego.

Wiele dyskusji na temat teorii typów wydaje się koncentrować na dodawaniu funkcji przyrostowych do poprzednich systemów typów, a nie „jakie jest następne duże uogólnienie od systemu typów X?”. Typy zależne wydają się być kolejnym dużym uogólnieniem z Systemu F, ale nie znalazłem jeszcze intuicyjnego, kanonicznego języka zależnego. Wiele odniesień do rachunku (indukcyjnych) konstrukcji powoduje, że myślę, że CoC jest tym językiem, ale wyjaśnienia języka, który widziałem, nie wydają mi się zbyt jasne ani intuicyjne.

Spodziewam się / zgaduję, że taki język miałby takie cechy jak: (i daj mi znać, jeśli coś konkretnego wyskoczy jako zdezorientowane lub nierealne)

• Uogólniona abstrakcja (może mieć funkcje z dowolnej domeny w hierarchii typów na inne, rodzaj -> termin, termin-> typ '' itp.)
• Ma nieskończoną hierarchię pisania (terminy: typy: typy ': typy' ': ...)
• Minimalna liczba podstawowych elementów. Wyobrażam sobie, że język zapewnia tylko jeden element dla każdego poziomu. Na przykład może twierdzić, że ((): Unit: Type: Type ': ...). Inne elementy są zbudowane z tych elementów.
• Suma i typy produktów są pochodnymi.

Szukam również wyjaśnienia tego języka, który najlepiej omawia:

• Związek między abstrakcją a kwantyfikacją w tym języku. Jeśli nie są zjednoczone, wyjaśnij, dlaczego nie są zjednoczone.
• Hierarchia typów nieskończonych jawnie

Zadaję to pytanie, ponieważ chcę nauczyć się teorii typów zależnych, ale także dlatego, że chcę przygotować przewodnik, który przy założeniu, że ma małe doświadczenie w CS, uczy obsługi i sposobu rozumienia asystentów dowodzenia oraz języków zależnie wpisywanych.

(Krzyż wysłany do Reddit)

Istnieje kilka różnych sposobów podejścia do tego:

1. Teoria typów zależnych . Nie jest to prawdopodobnie najłatwiejszy sposób uczenia się o typach zależnych, ale można na przykład spojrzeć na dokumenty Calculus of Constructions i ich warianty, Pure Type Systems oraz artykuł Martina Hofmanna na temat składni i semantyki typów zależnych.

2. Dowodzenie twierdzeń . Po pierwsze, spójrz na moją odpowiedź na powiązane pytanie: Jak mógłbym zacząć uczyć się podstawowej teorii asystenta dowodu Coq? .

3. $\Pi\Sigma$, pośród innych. I oczywiście jest książka Adama Chlipali, podana w odpowiedzi Marca Hamanna.

Byłbym skłonny zacząć od programowania, zanim przejdę do użycia dowodzenia twierdzeń, a następnie zacznę zgłębiać bardziej teoretyczne problemy.

$\lambda\pi$

Twelf to dobry system dowodzenia twierdzeń oparty na LF. Przegląd zaawansowanych notatek kursowych oferowanych przez Franka Pfenninga stanowi dobre wprowadzenie do teorii i praktyki LF.

To powiedziawszy, być może nie jest to najlepszy pierwszy system, aby dowiedzieć się, czy interesuje Cię matematyka konstruktywna, a nie podstawy teorii typów: LF oznacza ramy logiczne i jest systemem służącym do aksjatyzacji teorii i nie jest tak często stosowany system docelowy bezpośrednio. Korzystanie z systemu opartego na teorii typów Martina-Loefa jest prawdopodobnie najlepszym wprowadzeniem - między innymi Dave wspomina o Agdzie - jest być może lepszym punktem wyjścia, jeśli jest to twój cel, ponieważ w takim przypadku możesz szybciej zacząć z typami arytmetycznymi i indukcyjnymi struktura.

CoC jest najprawdopodobniej właściwą drogą. Po prostu zanurz się w Coq i przeprowadź fajny samouczek, taki jak Software Foundations (w który zaangażowany jest Pierce z TaPL i ATTaPL).

Po zapoznaniu się z praktycznymi aspektami pisania zależnego powróć do źródeł teoretycznych: będą one miały o wiele więcej sensu.

Twoja lista funkcji brzmi właściwie poprawnie, ale sprawdzenie, jak działają w praktyce, jest warte tysiąca punktów funkcji.

(Kolejnym, nieco bardziej zaawansowanym samouczkiem jest Certyfikowane programowanie Adama Chlipali z typami zależnymi )

Myślałem, że ten artykuł pomógł w zdemistyfikowaniu koncepcji na poziomie podstawowym: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html

Spójrz na http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf i wspomniany tam starszy system PiSigma.