Czy kompilator dla typu zależnego jest znacznie trudniejszy niż interpreter?

Nauczyłem się czegoś o implementowaniu typów zależnych, takich jak ten samouczek , ale większość z nich to implementacja tłumaczy. Moje pytanie brzmi: wydaje się, że implementacja kompilatora dla typu zależnego jest znacznie trudniejsza niż kompilator, ponieważ naprawdę można ocenić argumenty typu zależnego dla sprawdzania typu.

Więc

Czy moje naiwne wrażenie jest właściwe?
Jeśli ma rację, jakikolwiek przykład / zasoby dotyczące implementacji sprawdzanego statycznie języka obsługującego typ zależny?

type-systems compilers dependent-type

— molikto
źródło

Nie, ponieważ można zredukować problem kompilacji typów zależnych do znanego problemu: (1) typ sprawdź program za pomocą interpretera; (2) wypakuj program do OCaml / Haskell / cokolwiek; (3) skompiluj za pomocą ocamloptlub GHC :-) (

— Nawiasem mówiąc,

To interesujące pytanie! Jak sugeruje odpowiedź Anthony'ego, można użyć zwykłych podejść do kompilacji niezależnego języka funkcjonalnego, pod warunkiem , że masz już tłumacza do oceny warunków do sprawdzania typu .

Takie podejście zastosował Edwin Brady. Teraz jest to koncepcyjnie prostsze, ale traci kontrolę nad szybkością kompilacji podczas sprawdzania typu. Zostało to rozwiązane na kilka sposobów.

Po pierwsze, można zaimplementować maszynę wirtualną, która w locie kompiluje warunki do kodu bajtowego w celu wykonania sprawdzenia konwersji. Taki jest pomysł vm_computezaimplementowany w Coq przez Benjamina Gregoire'a . Podobno jest też to teza Dirk Kleeblatt na dokładnie ten temat, ale w dół rzeczywistego kodu maszynowego, a nie na maszynie wirtualnej.

Po drugie, można wygenerować kod w bardziej konwencjonalnym języku, który po uruchomieniu sprawdza wszystkie konwersje niezbędne do sprawdzania typu programu zależnie wpisanego. Oznacza to, że możemy użyć Haskell, powiedzmy, do sprawdzenia typu modułu Agda. Kod można skompilować i uruchomić, a jeśli się zgadza, można założyć, że kod w języku typu zależnego jest dobrze wpisany (błędy implementacji i błędów kompilatora). Po raz pierwszy usłyszałem takie podejście sugerowane przez Mathieu Boesfluga .

$^*$

— cody
źródło

Trochę mowiony: dlaczego miałbyś męczyć się pisać kompilator, jeśli masz tłumacza sprawdzającego typ? W końcu większość (wszystkich?) Poważnych użytkowników języków programowania o typach zależnych dba tylko o sprawdzanie typów, używając tego języka jako asystenta sprawdzania. Z pewnością nigdy nie uruchomiłem żadnego z moich programów Agda ani Coq. Jeśli więc zależy Ci na szybkości, czy nie chcesz skompilować konwersji typu?

— Martin Berger,

Rozwiązania 2 i 3 rozwiązują ten problem: kompilujesz kod, który sprawdza poprawność pisania (aw szczególności wykonuje konwersje typów). Moja druga uwaga jest taka, że w niektórych sytuacjach naprawdę chcesz uruchamiać kod wpisany w sposób zależny (patrz Idris, Ur / Web).

— cody

Ponadto: do pewnego stopnia rozwiązanie 1 również rozwiązuje ten problem, zacierając linie między tłumaczem a kompilatorem.

— cody

Zastanawiam się, czy można by zastosować technikę projekcji futurama do przyspieszenia interpretera, kończąc na kompilatorze?

— Steven Shaw

Jedyne, co widziałem, to Unison unisonweb.org/2017-10-13/scala-world.html

— Steven Shaw

Praca doktorska Edwina Brady'ego opisuje, jak zbudować kompilator dla języka programowania o typie zależnym. Nie jestem ekspertem, ale powiedziałbym, że nie jest to trudniejsze niż implementacja kompilatora podobnego do Systemu F. Wiele zasad jest dość podobnych, a niektóre są takie same (np. Kompilacja superkombinatora). Teza obejmuje wiele innych problemów.

— Anthony
źródło