Hatásrendszer - Effect system

A számítás során az effektusrendszer egy hivatalos rendszer, amely leírja a számítógépes programok számítási hatásait, például a mellékhatásokat . Hatásrendszer használható a program lehetséges hatásainak fordítási időbeli ellenőrzésére.

Az effektusrendszer kiterjeszti a típus fogalmát, hogy "effekt" komponens legyen, amely tartalmaz egy effekt fajtát és egy régiót . A hatásfajta leírja, hogy mi történik, és a régió leírja , hogy milyen paraméterekkel történik.

Az effektus rendszer általában egy típusú rendszer kiterjesztése . Ebben az esetben néha a " típus és hatás rendszer " kifejezést használják. Gyakran egy érték típusát a hatásával együtt típusként jelöljük ! effektus , ahol a típuskomponens és az effektuskomponens is megemlít bizonyos régiókat (például egy mutálható memóriacella típusát annak a memóriaterületnek a címkéje paraméterezi, amelyben a cella található). Az " algebrai hatás " kifejezések a típusrendszerből következnek.

Hatásrendszerek használhatók bizonyos belsőleg szennyezett definíciók külső tisztaságának bizonyítására : például ha egy függvény belsőleg lefoglal és módosít egy memóriaterületet, de a függvény típusa nem említi a régiót, akkor a megfelelő hatás kitörölhető a függvény hatása.

Példák

Néhány példa a hatásrendszerekkel leírható viselkedésre:

• Memória olvasása, írása vagy lefoglalása: az effektus típusa olvasható , írható , lefoglalható vagy szabad , és a régió annak a programnak a pontja, ahol a kiosztást végrehajtották (azaz minden programhelynek, ahol a kiosztást végzik, egyedi címke és régió van az információ statikusan terjed az adatfolyam mentén). A memóriával dolgozó legtöbb funkció valójában polimorf lesz a régióváltozóban: például annak a függvénynek a típusa lesz, amely két helyet cserél a memóriában forall r1 r2, unit ! {read r1, read r2, write r1, write r2}.
• Erőforrásokkal, például fájlokkal való munka: például az effektus típusa lehet nyitott , olvasható és bezárható , és ismét a régió a program azon pontja, ahol az erőforrást megnyitják.
• Vezérlésátvitel folytatásokkal és hosszú ugrásokkal: az effektus fajtája lehet goto (azaz a kódrész ugrást hajthat végre) és comefrom (azaz a kódrész egy ugrás célpontja lehet), a régió pedig a program, ahonnan vagy ahova az ugrás elvégezhető.

Programozói szempontból az effektusok hasznosak, mivel lehetővé teszik az egyes műveletek végrehajtásának ( hogyan ) elválasztását a végrehajtandó műveletek specifikációjától. Például egy ask név effektus olvasható a konzolról, beugrik egy ablakba, vagy csak visszaad egy alapértelmezett értéket. A szabályozási folyamat leírható a hozam (abban az értelemben , hogy a végrehajtás folytatódik) és a dobás keveréke (mivel egy kezeletlen hatás továbbterjed, amíg le nem kezelik).

Végrehajtások

• A Haskell több olyan csomaggal rendelkezik, amelyek lehetővé teszik az effektusok kódolását.
• A Java ellenőrzött kivételei példák egy effektus rendszerre: az effektus típusa dobások , a régió pedig a dobott kivétel típusa.
• A Koka egy effektet szem előtt tartó programozási nyelv.
• Az ECMAScriptnek van javaslata (és Bábel-passzja), amely algebrai hatásokat valósít meg.

Hivatkozások

Tankönyvfejezetek

• Hankin, Chris; Nielson, Flemming; Nielson, Hanne Riis (1999). A programelemzés alapelvei . Berlin: Springer. ISBN 978-3-540-65410-0.
• Gifford, David; Turbak, Franklyn A .; Sheldon, Mark A. (2008). "16". Tervezési koncepciók a programozási nyelvekben . Cambridge, Massachusetts: MIT Press. ISBN 978-0-262-20175-9.

Áttekintő dokumentumok

• Nielson, Flemming; Nielson, Hanne Riis (1999). Típus és effekt rendszerek . Helyes rendszerterv: Legutóbbi betekintés és fejlődés . Előadási jegyzetek a számítástechnikában . 1710 . Springer-Verlag. pp.  114-136 . doi : 10.1007 / 3-540-48092-7_6 . ISBN 978-3-540-66624-0.

További irodalom

• Marino, Daniel; Millstein, Todd (2008). Általános típus és effekt rendszer (PDF) . A nyelvtervezés és megvalósítás típusainak 4. nemzetközi műhelymunkája . ACM . o. 39. CiteSeerX  10.1.1.157.8373 . doi : 10.1145 / 1481861.1481868 . ISBN 9781605584201.
• Lucassen, John M .; Gifford, David K. (1988). Polimorf hatásrendszerek . A 15. ACM SIGPLAN-SIGACT szimpózium anyagai a programozási nyelvek elveiről . ACM . 47–57. CiteSeerX  10.1.1.73.4916 . doi : 10.1145 / 73560.73564 . ISBN 978-0897912525.