Uniwersalna / egzystencjalna kwantyfikacja?

Usiłuję zrozumieć cel uniwersalnej i egzystencjalnej kwantyfikacji typów. Bawię się pisząc zabawkowy język na podstawie rachunku konstrukcji . Czytałem o Morte i Henku, aby pomóc mi lepiej zrozumieć.

Nie rozumiem, dlaczego CoC ma zarówno lambda, jak i całkowitą abstrakcję.

Wydaje mi się, że lambda ogarnia wszystko w systemie, w którym typy są przekazywane ręcznie. Innymi słowy, że następujące

Można zastąpić

Jeśli po raz pierwszy zastosowano do używanego typu.

czego mi brakuje? Jakie artykuły, blogi lub artykuły są do przeczytania, które mogą mi pomóc?

Dzięki.

Pomaga pamiętać, że (lub jak czasem widzisz) jest typem. To uogólnia . Więc chociaż mówienie ma sens, nie ma sensu mówić ponieważ jest tylko typem. Nie powiedziałbyś, że ponieważ nie jest przeznaczony do obliczeń per se, ma on na celu klasyfikację terminów lambda, które można zastosować w ten sposób .$\forall$$\Pi$$\to$$(\lambda x : A. M)\ N$$(\forall x : A. M)\ N$$\forall ...$$(A \to B)\ N$$\to$

To mnie również potknęło, ale tak definiuje się rachunek konstrukcji (jak i każdy inny system zależny od typu).

Dwa napisane przez ciebie programy mają bardzo różne intencje, a pierwszy jest źle napisany. Nie ma sensu mówić ponieważ wymaga obu argumentów według typów, co oznacza, że ​​jeśli ma być dobrze wpisany, musimy mieć . Jednak nie jest typem, można mu tylko przypisać typ formy , nigdy . Drugi natomiast jest prawie (myślę, że chodziło o powrót nie ) jest funkcją i podany jest typ używając dwóch s.$\forall x : A.\ \lambda x.\ x$$\forall$$\forall x : A. B$$B : *$$\lambda x. x$$\forall x : A. B$$*$$a$$x$$\forall$

Pamiętaj, że typy egzystencjalne i uniwersalne są raczej różne. Jest to logika konstruktywna, a nie logika klasyczna, aw logice konstruktywnej i ∃ nie są tak powiązane, jak w logice klasycznej.$\forall$$\exists$

jest rodzajem programów, które odbierają obiekt typu A i zwracają obiekt typu B ( x ) . Ważne jest tutaj to, że typ B ( x ) zależyod x i nie jest taki sam dla wszystkich x . Może się różnić w zależności od x . Dla jednego wejścia x możemy wypisać liczbę całkowitą. Dla kolejnego możemy wypisać liczbę rzeczywistą. W jeszcze innym przypadku możemy wyprowadzić funkcję ponad liczby rzeczywiste. Jeśli B ( x $\forall x:A. B(x)$$A$$B(x)$$B(x)$ $x$$x$$x$$x$$B(x)$nie zmienia się z , a następnie można użyć A → B w miejscu, które jest typem funkcji od A do B .$x$$A\to B$$A$$B$

jestzależnąwersją (konstruktywnego) rozłączenia. Można myśleć o konstruktywne alternatywy A ∨ B dwa typy A i B jako unii rozłącznych z A i B . ∃ x : . B ( x ) jest związkiem rozłączne z kolekcji typy B ( x ) indeksowana x : . Fakt, że typ B $\exists x:A. B(x)$$A \lor B$$A$$B$$A$$B$$\exists x:A.B(x)$$B(x)$$x:A$ van różni się w zależności od wartości x : A czyni go zależnym typem. Porównać z przypadkiem, gdy B nie zależy od x : A : ∃ x : A . B . Bierzemy jedną kopię tego samego B dla każdego x : A . To jest izomorficzna × B .$B(x)$$x:A$$B$$x:A$$\exists x:A. B$$B$$x:A$$A \times B$

Teraz możesz zapytać, dlaczego potrzebujemy zależnych rodzajów produktów i sum? Ponieważ dają nam większą siłę wyrazu. Teraz możemy całkowicie zignorować typy i zastosować niepoprawną teorię typów / programowanie funkcjonalne. Ale to eliminuje zalety posiadania typów, np. Nie będziesz wiedział, czy wszystkie programy zawsze zakończą się (silna normalizacja). Zobacz Lambda Cube and Dependent Type . Myślę, że dobrym sposobem na dobre zrozumienie typów zależnych jest przyjrzenie się zasadom wprowadzania i eliminowania typów zależnych w teorii typów Martina-Lofa .

Głównym celem typów zależnych jest: chcemy pozostać w ładnej teorii z różnych powodów (np. Unikanie błędów, automatyczny dowód zakończenia itp.). Nie chcemy przechodzić do czegoś takiego jak nieoparty rachunek lambda, w którym możemy robić wyrażenia takie jak te, które wypowiedziałeś i znacznie mocniejsze rzeczy. Można powiedzieć, że wymyślono typy zależne, aby umożliwić wyrażanie większej liczby rzeczy, pozostając jednocześnie w ładnej teorii typów.