Struktury danych w języku programowania z typami liniowymi

Załóżmy, że mamy do czynienia z językiem programowania obsługującym typy liniowe (terminy typu liniowego mogą być użyte najwyżej raz, że tak powiem). Pozwala to na traktowanie niektórych efektów obliczeniowych (takich jak mutacja, a nawet zmiana rodzaju operandu) w sposób problematyczny dla języków, których systemy typów działają tylko na „wiecznych prawdach”.

Wiele struktur danych można scharakteryzować za pomocą typów indukcyjnych (listy i drzewa są przykładami kanonicznymi). Jeśli dodamy do mieszanki liniowe typy indukcyjne, możemy również obsługiwać zmienne struktury danych.

Jednak nie jest dla mnie jasne, jak reprezentować struktury danych, które wykazują współdzielenie i odwołania cykliczne w języku programowania z typami liniowymi (przykładami takich struktur danych są DAG i inne wykresy, reprezentowane przez listy przyległości lub coś innego, listy cykliczne). Czy możemy to zrobić? Jeśli nie jest to możliwe, w jaki sposób powinniśmy rozszerzyć język, aby uwzględnić takie struktury danych?

Najbardziej zaangażowanym przykładem, jaki do tej pory znalazłem, jest podwójnie połączona lista. Czy są inne przykłady?

pl.programming-languages type-theory linear-logic

— Bjørn Kjos-Hanssen
źródło

Liniowość nie jest wystarczającym ograniczeniem, aby określić unikalną reprezentację stanową, więc odpowiedź na twoje pytanie zależy od tego, jak interpretujesz logikę liniową w kategoriach stanu. Zazwyczaj znajdzie to odzwierciedlenie w sposobie interpretowania Modalność. $!A$

Jeśli planowana semantyka odniesień mówi, że wszystkie wskaźniki są unikatowymi wartościami (tzn. Istnieje co najwyżej jedno odniesienie do obiektu), wówczas dags i struktury grafów nie są wyrażalne, z tego rodzaju tautologicznego powodu, że dag może zawierać wiele odniesień do ten sam obiekt. W tym przypadku Musi być obliczenia , które tworzy nową wartość typu , ponieważ chcesz Maps $!A$ $A$ I. $\delta_A : !A \multimap !A \otimes !A$ $\epsilon_A : !A \multimap A$

Załóżmy jednak, że chcesz reprezentować udostępnianie . Następnie obiekty można zbierać w pomocą liczenia referencji za pomocą map i można realizować jako operacje, które po prostu podważają referencje. W takim przypadku nie można użyć liniowości, aby założyć, że mutacja wartości zawsze jest bezpieczna, ponieważ istnieje współdzielenie. Możesz jednak upewnić się, że cała alokacja pamięci jest jawna w twoim programie i że nie ma żadnych cykli na stercie. $!A$ $\delta_A : !A \multimap !A \otimes !A$ $\epsilon_A : !A \multimap A$

W najbardziej praktycznych implementacjach typów liniowych nie stosuje się żadnej z tych dwóch interpretacji. Zamiast tego referencje są postrzegane jako dowolnie powielane jednostki, a to, co śledzimy liniowo, to w rzeczywistości możliwości . Możliwości nie są wartościami środowiska wykonawczego; są to podmioty czysto koncepcyjne, które mają reprezentować pozwolenie na dostęp do odniesienia. Chodzi o to, że programujesz w stylu przekazywania uprawnień, a więc nawet jeśli istnieje wiele odniesień do tego samego obiektu, odczyt lub modyfikacja elementu stanu może nastąpić tylko wtedy, gdy masz również dostęp do niego. A ponieważ zdolność jest liniowa, wiesz, że tylko Ty możesz to zmienić.

\begin{matrix} n mi w & : & \forall α . α ⊸ \exists do : ι . do za p (do) \otimes r mi fa (α, do) \\ sol mi t & : & \forall α, do : ι . do za p (do) \otimes r mi fa (α, do) ⊸ α \otimes do za p (do) \otimes r mi fa (α, do) \\ s mi t & : & \forall α, do : ι . do za p (do) \otimes r mi fa (α, do) \otimes α ⊸ do za p (do) \otimes r mi fa (α, do) \\ do o p y & : & \forall α, do : ι . r mi fa (α, do) ⊸ r mi fa (α, do) \otimes r mi fa (α, do) \end{matrix}

$\array{ \mathsf{new} & : & \forall \alpha. \;\alpha \multimap \exists c : \iota. \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{get} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \multimap \alpha \otimes \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{set} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \otimes \alpha \multimap \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{copy} & : & \forall \alpha, c:\iota.\; \mathsf{ref}(\alpha,c) \multimap \mathsf{ref}(\alpha,c) \otimes \mathsf{ref}(\alpha,c) }$

W zarysowanym powyżej interfejsie API, zakresy powyżej , niektóre dziedziny wskaźników czasu kompilacji i zakresy ponad typami. Mamy typ który jest zdolnością indeksowaną przez , oraz typ , który jest rodzajem odniesień do do którego dostęp uzyskuje zdolność . Wywołanie i na referencji wymaga zdolności , a wywołanie $c$ $\iota$ $\alpha$ $\mathsf{cap}(c)$ $c$ $\mathsf{ref}(\alpha, c)$ $\alpha$ $c$ $\mathsf{get}$ $\mathsf{set}$ $c$ tworzy nowe odniesienie i nową możliwość współużytkowania wspólnego indeksu. Jednakże, -nia odniesienie nie wymaga dostępu do jakiegokolwiek możliwości, to każdy może kopiować odniesienia, jak długo nie wyglądają w środku. $\mathsf{new}$ $\mathsf{copy}$

— Neel Krishnaswami
źródło

Dziękuję za prowokującą odpowiedź. Jestem jednak zainteresowany, czy istnieje (techniczne) rozróżnienie między aliasingiem a udostępnianiem? Czy istnieją systemy, które mogą stopniowo przechodzić od liniowego (co najwyżej jednego odniesienia) do współdzielonego przez co najwyżej n odniesień do wspólnego w nieograniczony sposób?

1. Aliasing i udostępnianie są synonimami. 2. Tak, pozwalają na to interpretacje w stylu zdolności, powiększone o uprawnienia cząstkowe Boylanda . Zobacz także ostatnią pracę Pottiera nad kalkulacjami zdolności do teorii oraz pracę Aldricha i Bierhofa nad liczbą mnogą do implementacji.

— Neel Krishnaswami,