Czy elementarną logikę afiniczną można wykorzystać jako podstawowy system typów praktycznego języka programowania?

Elementary Affine Logic to system typów, który przechwytuje klasę terminów λ, które można zredukować w czasie elementarnym. Ponadto terminy typowe dla EAL można zredukować za pomocą abstrakcyjnego fragmentu algorytmu Lampinga, co jest dla mnie szczególnie interesujące, ponieważ badam odpowiednie kombinatory interakcji.

Moje pytanie brzmi: w jaki sposób można stworzyć praktyczny język programowania przy użyciu EAL jako podstawowego systemu typów? Tj. Jakie rozszerzenia (punkty stałe, polimorfizm, typy zależne, typy danych itp.) Można wprowadzić do systemu typów rdzenia bez wpływu na tę cechę, i czy taki język byłby użyteczny w praktyce, czy też byłby w jakiś sposób restrykcyjne z powodów, których nie jestem świadomy?

Baillot, Gaboardi i Mogbil kilka lat temu podjęli próbę zastosowania czegoś bardzo podobnego, ale przy użyciu logiki lekkiej afinii (LAL) zamiast EAL (artykuł można znaleźć tutaj ). Myślę, że ich prace można łatwo uogólnić na EAL, który jest systemem bardziej liberalnym.

Jeśli chodzi o cechy takiego języka, masz natywny polimorfizm (EAL jest ograniczeniem logiki liniowej drugiego rzędu). O ile mi wiadomo, nikt nie patrzył na typy zależne, ale nie rozumiem, dlaczego nie powinny działać. W rzeczywistości niepisany EAL działa tak samo dobrze, jak typowy EAL, ponieważ jego właściwości normalizacyjne nie zależą od typów.

Jedną konsekwencją jest to, że w EAL można użyć dowolnego stałego punktu typów (patrz na przykład ten inny artykuł Baillota) i zdefiniować typy danych w naturalnym rekurencyjnym stylu (np.$\mathtt{list\ A := nil\mathrel | A\ *\ list\ A}$), wraz z mniej naturalną (z punktu widzenia programowania) definicją systemu F. Jednakże, zgodnie z powyższą uwagą na temat beztypowej normalizacji, język programowania oparty na EAL będzie zawsze całkowity , co oznacza, że ​​nie będziesz miał kombinatora punktów stałych, a użycie typów rekurencyjnych nie będzie tak naturalne, jak byś się spodziewał. Weźmy na przykład cyfry Scott: bez definicji rekurencyjnych (podanych przez kombinator punktów stałych) trudno jest wyrazić cokolwiek poza operacjami w czasie stałym z taką reprezentacją liczb całkowitych. Dlatego nadal będziesz musiał używać cyfr iteracyjnych do iteracji (tj.$\mathtt{for}$ pętle), za pomocą których poniesiesz podstawowe ograniczenie stratyfikacji logiki światła (co daje im ich właściwości złożoności): nie możesz iterować funkcji $\mathsf{Nat}\rightarrow\mathsf{Nat}$ który sam został zdefiniowany przez iterację ($\mathsf{Nat}$ tutaj jest typ liczb całkowitych Kościoła).

Przykład: z pewnym „hakowaniem liczb całkowitych Kościoła” można zdefiniować w EAL $\mathsf{dbl}:\mathsf{Nat}\rightarrow\mathsf{Nat}$ takie, że $\mathsf{dbl}\ \underline{n} = \underline{2n}$ bez iteracji. Następnie możesz iterować$\mathsf{dbl}$ aby zdefiniować funkcję wykładniczą $\mathsf{exp}$które jednak nie mogą być iterowane. Tak więc każdy język programowania oparty na EAL będzie musiał mieć jakiś mechanizm zabraniający pewnych definicji przez iterację; trudno sobie wyobrazić, jak takie ograniczenie nie spowodowałoby, że język byłby dla programisty niewygodny. W każdym razie nikt nie zabrania ci próbować zobaczyć, co możesz dostać!

W każdym razie, jeśli interesuje Cię związek między optymalną oceną, EAL i ogólną logiką świetlną, sugeruję przyjrzeć się artykułom Coppoli z początku do połowy 2000 roku.