Czy istnieje hierarchia ekspresyjności dla systemów typów?

Zainspirowany rozległymi hierarchiami obecnymi w teorii złożoności, zastanawiałem się, czy takie hierarchie występują również w przypadku systemów typów. Jednak dwa przykłady, które do tej pory znalazłem, bardziej przypominają listy kontrolne (z funkcjami ortogonalnymi) niż hierarchie (z coraz bardziej ekspresyjnymi systemami typów).

Te dwa przykłady znalazłem to kostka Lambda i pojęcie polimorfizmu k rankingu . Pierwsza z nich to lista kontrolna z trzema opcjami, druga to prawdziwa hierarchia (choć moim zdaniem k-ranking dla określonych wartości k jest rzadkością). Wszystkie inne funkcje systemu typów, o których wiem, są w większości ortogonalne.

Interesują mnie te koncepcje, ponieważ projektuję własny język i jestem bardzo ciekawy, jak plasuje się on wśród obecnie istniejących systemów typów (o ile wiem, mój system typów jest nieco niekonwencjonalny).

Zdaję sobie sprawę, że pojęcie „ekspresyjności” może być nieco niejasne, co może wyjaśniać, dlaczego systemy czcionek wydają mi się listami kontrolnymi.

pl.programming-languages type-theory

— Alex ten Brink
źródło

Jestem pewien, że twardych i szybkich porównań ekspresji można dokonać tylko między bardziej teoretycznymi systemami typów. Jeśli projektujesz pełny język programowania, możesz wykonać porównanie poszczególnych funkcji z istniejącymi językami / formalizmem. Niestety, ponieważ wiele funkcji można zakodować pod względem innych funkcji, nie będzie to trywialne zadanie. Jeśli możesz mieć tak wymyślne typy jak Scala lub Haskell, będziesz dobrze sobie radził pod względem ekspresji.

— Dave Clarke

Naprawdę powinienem napisać mój post na blogu na temat „Jak porównywać języki programowania” ...

— Andrej Bauer,

@Andrej Bauer: Byłby to interesujący dodatek do odpowiedzi i uwag już tutaj obecnych. Nauczyłem się już sporo o tym, jak można zdefiniować „ekspresyjność” - może powinienem był o to zapytać…

— Alex ten Brink

Jestem pewien, że widziałem polimorfizm rangi 2 używany w kilku miejscach. Pamiętam teraz Lammela, Peytona-Jonesa, Scrap Your Boilerplate, 2003.

— Radu GRIGore

@Radu GRIGore: Polimorfizm rangi 2 jest znaczący, ponieważ pozwala na pojawienie się argumentów typu w pozycji podwójnie sprzecznej, co przy zwykłym rodzaju dualności pozwala modelować typy egzystencjalne przez ich kodowanie w Kościele. Ranga 3 po prostu ponownie podaje uniwersalną kwantyfikację i zmienia się z niej, więc w porównaniu z nią dodaje się niewiele mocy ekspresji.

— CA McCann,

Odpowiedzi:

Istnieje kilka zmysłów „ekspresji”, które mogą być potrzebne dla systemu typów.

$F$
$A$ $B$ $F$ $F$
$A$ $B$
Czy jeden typ systemu gwarantuje lepsze właściwości niż inny. Na przykład systemy typu liniowego po prostu odrzucają więcej programów, ale to pozwala im na mocniejsze stwierdzanie o programach, które akceptują.

Niestety nie wierzę, że były prace nad kategoryzowaniem lub formalizowaniem tych pojęć, z wyjątkiem kostki lambda Barendregta, jak omawia @cody.

— Sam Tobin-Hochstadt
źródło

Myślę, że przez „artykuł o ekspresyjności Felleisena” masz na myśli jego „ O ekspresyjnej mocy języków programowania” .

— Martin Berger,

Tak, dokładnie. Wyjaśniłem tę część odpowiedzi.

— Sam Tobin-Hochstadt,

Nie jestem pewien, czy mam zadowalającą odpowiedź na twoje pytanie, ale jeśli weźmiesz pod uwagę Pure Type Systems, które są uogólnieniem systemów znajdujących się w kostce lambda (dokładny, choć nieco przestarzały przegląd można znaleźć w klasycznym tekście Barendregt ), istnieje kilka naturalnych pojęć hierarchii:

$\Gamma\vdash_A\ t\colon T$ $\Gamma\vdash_B\ t\colon T$ $\Gamma, t$ $T$ $*\colon *$ $(*,*,*)$ PTS w tym sensie, że występuje w nim morfizm ze wszystkich innych PTS. Można to postrzegać jako miarę ekspresyjności systemu typów, w którym końcowy PTS jest systemem najbardziej ekspresyjnym.
$A$ $B$ $A$ $F_\omega$ $ECC$ $\leftrightarrow$

— cody
źródło