Substrukturell typsystem

Substrukturella system är en familj av typsystem analoga med substrukturella logiker där en eller flera av de strukturella reglerna saknas eller endast tillåtna under kontrollerade omständigheter. Sådana system är användbara för att begränsa åtkomst till systemresurser som filer , lås och minne genom att hålla reda på tillståndsändringar som inträffar och förhindra ogiltiga tillstånd.

Olika substrukturella system

Flera typsystem har uppstått genom att förkasta några av de strukturella reglerna för utbyte, försvagning och sammandragning:


	Utbyta	Försvagning	Kontraktion	Använda sig av
Beordrade	—	—	—	Exakt en gång i ordning
Linjär	Tillåten	—	—	Exakt en gång
Affine	Tillåten	Tillåten	—	Högst en gång
Relevant	Tillåten	—	Tillåten	Åtminstone en gång
Vanligt	Tillåten	Tillåten	Tillåten	Godtyckligt

Ordnade typsystem (kassera utbyte, försvagning och kontraktion): Varje variabel används exakt en gång i den ordning den introducerades.
Linjära system (tillåter utbyte, men varken försvagning eller kontraktion): Varje variabel används exakt en gång.
Affina system (tillåter utbyte och försvagning, men inte kontraktion): Varje variabel används högst en gång.
Relevanta typsystem (tillåter utbyte och kontraktion, men inte försvagning): Varje variabel används minst en gång.
System av normal typ (tillåter utbyte, försvagning och kontraktion): Varje variabel kan användas godtyckligt.

Förklaringen till system av affin typ förstås bäst om den omformuleras som "varje förekomst av en variabel används högst en gång".

Beställt typsystem

Ordnade typer motsvarar icke-kommutativ logik där utbyte, kontraktion och försvagning kasseras. Detta kan användas för att modellera stackbaserad minnesallokering (mot linjära typer som kan användas för att modellera heapbaserad minnesallokering). Utan utbytesegenskapen får ett objekt endast användas när det är högst upp i den modellerade stacken, varefter det ploppas av vilket resulterar i att varje variabel används exakt en gång i den ordning den introducerades.

Linjära system

Linjära typer motsvarar linjär logik och säkerställer att objekt används exakt en gång. Detta gör det möjligt för systemet att säkert deallokera ett objekt efter dess användning, eller att designa programvarugränssnitt som garanterar att en resurs inte kan användas när den väl har stängts eller övergått till ett annat tillstånd.

Programmeringsspråket Clean använder sig av unika typer (en variant av linjära typer) för att stödja samtidighet, inmatning/utdata och uppdatering av arrayer på plats.

Linjära system tillåter referenser men inte alias . För att upprätthålla detta går en referens utanför omfånget efter att ha dykt upp på höger sida av en uppgift , vilket säkerställer att endast en referens till ett objekt finns på en gång. Observera att att skicka en referens som ett argument till en funktion är en form av tilldelning, eftersom funktionsparametern kommer att tilldelas värdet inuti funktionen, och därför gör sådan användning av en referens också att den går utanför räckvidden.

Ett linjärt system liknar C++: s unika_ptr- klass , som beter sig som en pekare men bara kan flyttas (dvs inte kopieras) i en uppgift. Även om linjäritetsbegränsningen kontrolleras vid kompilering , orsakar avreferensering av en ogiltiga unika_ptr odefinierat beteende vid körning . På samma sätt har programmeringsspråket Rust delvis stöd för linjära typer genom användning av lint-anteckningar, men till skillnad från C++ kan variabeln flyttad från inte användas igen.

Singelreferensegenskapen gör system av linjär typ lämpliga som programmeringsspråk för kvantberäkning , eftersom den återspeglar kvanttillståndets no-kloningssats . Ur kategoriteoretisk synvinkel är ingen kloning ett påstående om att det inte finns någon diagonalfunktion som kan duplicera tillstånd; på liknande sätt, ur den kombinatoriska logikens synvinkel, finns det ingen K-kombinator som kan förstöra tillstånd. Ur lambdakalkylens synvinkel kan en variabel x förekomma exakt en gång i en term.

Linjära typsystem är det interna språket för slutna symmetriska monoidala kategorier , ungefär på samma sätt som helt enkelt maskinskriven lambdakalkyl är språket i kartesiska slutna kategorier . Mer exakt kan man konstruera funktioner mellan kategorin linjära typsystem och kategorin slutna symmetriska monoidala kategorier.

Affina system

Affina typer är en version av linjära typer som tillåter att förkasta (dvs. inte använda ) en resurs, motsvarande affin logik . En affin resurs kan användas högst en gång, medan en linjär måste användas exakt en gång.

Relevant typsystem

Relevanta typer motsvarar relevant logik som tillåter utbyte och kontraktion, men inte försvagning, vilket innebär att varje variabel används minst en gång.

Programmeringsspråk

Följande programmeringsspråk stöder linjära eller affina typer:

C++
ATS
Rena
Idris
Merkurius
F*
LinjärML
Allmosa
Haskell med GHC 9.0.1 eller högre.
Granulat
Rost
Nim

Se även

Anteckningar

Walker, David (2002). "Substructural Type Systems". I Pierce, Benjamin C. (red.). Avancerade ämnen i typer och programmeringsspråk (PDF) . MIT Press. s. 3–43. ISBN 0-262-16228-8 .
Bernardy, Jean-Philippe; Boespflug, Mathieu; Newton, Ryan R; Peyton Jones, Simon ; Spiwack, Arnaud (2017). "Linjär Haskell: praktisk linjäritet i ett högre ordningens polymorft språk" . Proceedings of ACM on Programming Languages . 2 :1–29. arXiv : 1710.09756 . doi : 10.1145/3158093 . S2CID 9019395 .
Ambler, S. (1991). Första ordningens logik i symmetriska monoidala slutna kategorier ( PhD). U. av Edinburgh.
Baez, John C.; Stanna, Mike (2010). "Fysik, topologi, logik och beräkning: En Rosetta Stone". I Springer (red.). Nya strukturer för fysik (PDF) . s. 95–174.