System typu substrukturalnego - Substructural type system
| Systemy typu |
|---|
| Pojęcia ogólne |
| Główne kategorie |
| Pomniejsze kategorie |
Systemy typu substrukturalnego to rodzina systemów typu analogiczna do logiki substrukturalnej, w której co najmniej jedna reguła strukturalna jest nieobecna lub dozwolona tylko w kontrolowanych okolicznościach. Takie systemy są przydatne do ograniczania dostępu do zasobów systemowych, takich jak pliki , blokady i pamięć poprzez śledzenie zachodzących zmian stanu i zapobieganie nieprawidłowym stanom.
Różne systemy typu substrukturalnego
Kilka typów systemów pojawiło się poprzez odrzucenie niektórych strukturalnych zasad wymiany, osłabienia i kurczenia się:
| Giełda | Osłabiający | Skurcz | Posługiwać się | |
|---|---|---|---|---|
| Zamówione | — | — | — | Dokładnie raz w kolejności |
| Liniowy | Dozwolony | — | — | Dokładnie raz |
| Affine | Dozwolony | Dozwolony | — | Co najwyżej raz |
| Odpowiedni | Dozwolony | — | Dozwolony | Przynajmniej raz |
| Normalna | Dozwolony | Dozwolony | Dozwolony | Dowolnie |
- Systemy typu uporządkowanego (wymiana odrzucania, osłabianie i kontrakcja): Każda zmienna jest używana dokładnie raz w kolejności, w jakiej została wprowadzona.
- Systemy typu liniowego (pozwalają na wymianę, ale nie osłabiają ani nie skracają): Każda zmienna jest używana dokładnie raz.
- Systemy typu afinicznego (pozwalają na wymianę i osłabienie, ale nie na kurczenie): Każda zmienna jest używana co najwyżej raz.
- Systemy odpowiedniego typu (pozwalają na wymianę i kurczenie się, ale nie osłabiają): Każda zmienna jest używana przynajmniej raz.
- Systemy typu normalnego (pozwalają na wymianę, osłabienie i skurcz): Każda zmienna może być używana dowolnie.
Wyjaśnienie systemów typu afinicznego najlepiej zrozumieć, jeśli przeformułuje się je jako „każde wystąpienie zmiennej jest używane co najwyżej raz”.
Zamówiony system typu
Typy uporządkowane odpowiadają logice nieprzemiennej, w której wymiana, kontrakcja i osłabienie są odrzucane. Można to wykorzystać do modelowania alokacji pamięci opartej na stosie (w przeciwieństwie do typów liniowych, które mogą być używane do modelowania alokacji pamięci opartej na stercie). Bez właściwości exchange obiekt może być używany tylko wtedy, gdy znajduje się na szczycie modelowanego stosu, po czym jest zdejmowany, co powoduje, że każda zmienna jest używana dokładnie raz w kolejności, w jakiej została wprowadzona.
Systemy typu liniowego
Typy liniowe odpowiadają logice liniowej i zapewniają, że obiekty są używane dokładnie raz, dzięki czemu system może bezpiecznie cofnąć alokację obiektu po jego użyciu.
Język programowania Clean wykorzystuje typy unikatowości (wariant typów liniowych), aby pomóc w obsłudze współbieżności, danych wejściowych/wyjściowych i aktualizacji w miejscu tablic.
Systemy typu liniowego dopuszczają odwołania, ale nie aliasy . Aby to wymusić, odwołanie wykracza poza zakres po pojawieniu się po prawej stronie przypisania , zapewniając w ten sposób, że jednocześnie istnieje tylko jedno odwołanie do dowolnego obiektu. Zwróć uwagę, że przekazanie referencji jako argumentu do funkcji jest formą przypisania, ponieważ parametrowi funkcji zostanie przypisana wartość wewnątrz funkcji, a zatem takie użycie referencji również powoduje, że wychodzi ona poza zakres.
Liniowy układ typu jest podobne do C ++ jest unique_ptr klasy , który zachowuje się jak wskaźnik, ale może być przemieszczane (to znaczy nie zostały skopiowane) w zadania. Chociaż ograniczenie liniowości jest sprawdzane w czasie kompilacji , wyłuskanie unieważnionego unique_ptr powoduje niezdefiniowane zachowanie w czasie wykonywania .
Właściwość pojedynczego odniesienia sprawia, że systemy typu liniowego są odpowiednie jako języki programowania do obliczeń kwantowych , ponieważ odzwierciedla twierdzenie o braku klonowania stanów kwantowych. Z punktu widzenia teorii kategorii brak klonowania jest stwierdzeniem, że nie ma funktora diagonalnego, który mógłby powielać stany; podobnie, z punktu widzenia kombinatora nie ma K-kombinatora, który mógłby niszczyć stany. Z punktu widzenia rachunku lambda zmienna x może wystąpić w wyrażeniu dokładnie raz.
Systemy typu liniowego są język wewnętrzny z zamkniętymi symetrycznych kategoriach monoidal , dużo w ten sam sposób, że po prostu wpisane rachunek lambda jest językiem kartezjańskiego zamknięte kategorie . Dokładniej, można konstruować funktory pomiędzy kategorią układów typu liniowego a kategorią zamkniętych symetrycznych kategorii monoidalnych.
Systemy typu afinicznego
Typy affine to wersja typów liniowych pozwalająca na odrzucenie (tj. niewykorzystanie ) zasobu, odpowiadająca logice afinicznej . Zasób pokrewny może być użyty co najwyżej raz, podczas gdy zasób liniowy musi być użyty dokładnie raz.
Odpowiedni system typu
Odpowiednie typy odpowiadają odpowiedniej logice, która pozwala na wymianę i kurczenie się, ale nie na osłabienie, co przekłada się na to, że każda zmienna zostanie użyta przynajmniej raz.
Języki programowania
Następujące języki programowania obsługują typy liniowe lub afiniczne:
Zobacz też
Uwagi
Bibliografia
- Walker, Dawid (2002). „Systemy typu podstrukturalnego”. W Pierce, Benjamin C. (red.). Zaawansowane tematy w typach i językach programowania (PDF) . MIT Naciśnij. s. 3-43. Numer ISBN 0-262-16228-8.
