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.
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.∀ ∃
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 )∀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 → 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 (∃x:A.B(x) A∨B A B A B ∃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 ∃x:A.B B x:A A×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.
źródło