Egyediség típusa - Uniqueness type

Típusrendszerek
Általános fogalmak
Főbb kategóriák
Kisebb kategóriák

A számítástechnikában az egyedi típus garantálja, hogy az objektumot egyetlen szálon használják, legfeljebb egyetlen hivatkozással. Ha egy érték egyedi típussal rendelkezik, akkor az arra alkalmazott függvény optimalizálható az érték frissítésére az objektumkódban . Az ilyen helyszíni frissítések javítják a funkcionális nyelvek hatékonyságát, miközben megőrzik a referenciális átláthatóságot . Egyedi típusok is használhatók funkcionális és kötelező programozás integrálására.

Bevezetés

Az egyedi gépelést a legjobb példával magyarázni. Tekintsünk egy függvényt, readLineamely beolvassa a fájl következő sorát: 

function readLine(File f) returns String
    return line where
        String line = doImperativeReadLineSystemCall(f)
    end
end

Most doImperativeReadLineSystemCallegy OS -szintű rendszerhívás segítségével olvassa be a fájl következő sorát, amelynek mellékhatása a fájl aktuális pozíciójának megváltoztatása. Ez azonban sérti a hivatkozási átláthatóságot, mert ha többször meghívja ugyanazzal az argumentummal, minden alkalommal más eredményt ad vissza, amikor a fájl aktuális pozíciója mozog. Ez viszont readLinemegsérti a hivatkozási átláthatóságot, mert hív doImperativeReadLineSystemCall.

Az egyediségi gépeléssel azonban létrehozhatunk egy új verziót, readLineamely referenciálisan átlátszó, annak ellenére, hogy egy olyan funkcióra épül, amely nem hivatkozási szempontból átlátható: 

function readLine2(unique File f) returns (unique File, String)
    return (differentF, line) where
        String line = doImperativeReadLineSystemCall(f)
        File differentF = newFileFromExistingFile(f)
    end
end

A uniquenyilatkozat meghatározza, hogy a típus fegyedi; vagyis a visszatérés utáni fhívó soha többé nem hivatkozik rá , és ezt a korlátozást a típusrendszer érvényesíti . És mivel nem önmagát adja vissza , hanem egy új, más fájlobjektumot , ez azt jelenti, hogy lehetetlen, hogy bármikor újra argumentumként hívják meg , így megőrizve a referenciális átláthatóságot, miközben lehetővé téve a mellékhatások előfordulását. readLine2readLine2readLine2fdifferentFreadLine2f

Programozási nyelvek

Az egyedi típusokat olyan funkcionális programozási nyelvekben valósítják meg, mint a Clean , Mercury , SAC és Idris . Néha a monádok helyett funkcionális nyelveken végeznek I/O műveleteket .

A Scala programozási nyelvhez fordítóbővítményt fejlesztettek ki, amely megjegyzéseket használ az egyediség kezelésére a szereplők közötti üzenetátadás során.

Kapcsolat a lineáris gépeléssel

Egy egyedi típus nagyon hasonlít a lineáris típushoz , olyannyira, hogy a kifejezéseket gyakran felcserélhetően használják, de valójában van különbség: a tényleges lineáris gépelés lehetővé teszi a nemlineáris értékek lineáris formába történő formázását , miközben megtartják több utalás rá. Az egyediség garantálja, hogy egy értéknek nincsenek más hivatkozásai, míg a linearitás garantálja, hogy az értékre több hivatkozás nem történhet.

Lásd még

Hivatkozások

Külső linkek

A programozási nyelvek gépelésének egyediségéről szóló megbeszélések

Kísérletek az egyediség gépelésével (teljesítmény szempontjából)