ML modul nyelve

Az ML modulnyelv egy elsősorban az ML család programozási nyelveiben használt modulrendszer , amely applikatív szemantikával rendelkezik, vagyis egy kis funkcionális nyelv , amely modulokkal működik [1] .

Ez a legfejlettebb modulrendszer a programozási nyelvekben találhatók között [2] [3] .

Általános információk

A modulnyelv a legegyszerűbb formájában háromféle modulból áll:

Az aláírás tekinthető a struktúra leírásának, a szerkezet pedig az aláírás megvalósításának. Sok nyelv hasonló konstrukciókat kínál, általában különböző neveken: az aláírásokat gyakran interfészeknek vagy csomagspecifikációknak, a struktúrákat pedig implementációknak vagy csomagoknak nevezik. A terminológiától függetlenül az ötlet az, hogy egy egész kódrészlethez típust rendeljünk. Sok nyelvtől eltérően az ML-ben az aláírások és a struktúrák közötti kapcsolat sok a sokhoz , nem pedig több az egyhez vagy egy az egyhez . Egy aláírás sok különböző struktúrát írhat le, és egy struktúra sok különböző aláírásnak felelhet meg. A legtöbb más nyelvet szigorúbb korlátozások kötik, amelyek megkövetelik, hogy egy adott struktúrának egyetlen aláírása legyen, vagy hogy egy adott aláírás egyetlen szerkezetből származzon. Ez nem így van az ML esetében [4] .

A főáramú objektumorientált nyelvekben, mint a C++ vagy a Java , az absztrakciót olyan osztályok biztosítják , amelyek számos funkciót ( öröklés , altípus és dinamikus elküldés ) kombinálnak egyszerre egy fogalomban, ami megnehezíti azok formalizálását. és gondatlan használat esetén nemkívánatos következményekhez vezethet. Az osztályokkal ellentétben az ML modulnyelv teljes mértékben az absztrakcióra összpontosít , formáinak széles skáláját kínálja, és szilárd formai alapot biztosít a tanuláshoz. [5] Biztosítja a névtér - hierarchia kezelését , a felület finomszemcsés testreszabását , a megvalósító oldali absztrakciót és a kliens oldali absztrakciót .

A függvények egy egyedi fogalom, amelynek nincs megfelelője a legtöbb nyelven . Struktúrák feletti függvények, vagyis a már kiszámítottak alapján számolnak új struktúrákat, természetesen bizonyos aláírásoknak megfelelően. Ez lehetővé teszi az összetett programok strukturálásával kapcsolatos sokféle probléma megoldását .

Ebben az esetben két követelmény teljesül [6] :

A gyakorlatban nem mindig használják ki a külön fordítás lehetőségét - vannak teljesen optimalizáló fordítók, amelyek megnyitják a modulok keretét, hogy jelentősen növeljék a programok teljesítményét .

Nyelv

Struktúrák és aláírások

A környezet ( eng.  Environment ) a mag ML -ben ( eng.  Core ML ) definíciók gyűjteménye ( típusok , beleértve a funkcionálisakat , és értékek , beleértve a funkcionális és kizárólagosakat is ). A környezet lexikális hatókörű .

A struktúra ( structure) egy "materializált" környezet, manipulálható értékké alakítva [7] . A modulnyelv korai implementációival kapcsolatban ez a definíció egyfajta konvenció, mivel kezdetben a struktúrákat csak a kód legfelső szintjén (globális környezetben) lehetett definiálni vagy kiértékelni. Az ezt követő munka a modulnyelvet első osztályú szintre fejleszti .

A struktúra fogalmának bevezetése megköveteli a környezet definíciójának felülvizsgálatát a nyelv magjában. Mostantól a környezet típusok, értékek és struktúrák gyűjteménye. Ennek megfelelően a struktúra típusok, értékek és egyéb struktúrák gyűjteménye. A struktúrák rekurzív egymásba ágyazása nem megengedett, bár egyes implementációk támogatják [5] .

A struktúrák meghatározásának fő eszközei a beágyazott deklarációk , azaz a szintaktikai zárójelekbe zárt deklarációk struct...end. Például a következő struktúra egy veremet valósít meg , amely meghatározza a "stack" algebrai típusú objektumok belső szervezetét és a minimálisan szükséges függvénykészletet rajta:

struct type 'a t = 'a lista val empty = [] val isEmpty = null val push = op :: val pop = Lista . getItem end

Ennek a beágyazott deklarációnak az "értéke" egy struktúra. Ennek az értéknek a használatához azonosítót kell hozzá rendelni:

szerkezet Verem = struct type 'a t = 'a lista val empty = [] val isEmpty = null val push = op :: val pop = Lista . getItem end

A szerkezeti összetevők mostantól összetett (vagy minősített) neveken keresztül érhetők el, például Stack.push, Stack.empty : Stack.t.

Az aláírás ( signature) a struktúra elemeinek leírásainak felsorolása, vagyis a szerkezet interfésze . Ennek a felsorolásnak minden elemét specifikációnak nevezzük. Ha a típus az aláírásban egy értékhez x van megadva , akkor a szerkezetben az azonosítót típusú értékhez kell kötni . Az aláírást egy szerkezet egyfajta " típusának " tekinthetjük, de az aláírás nem típus a szó szoros értelmében, mivel a típus értékek halmaza , az "aláírási érték" pedig tartalmazhat típusokat (amelyek a Az ML nem értékek). Az aláírásban szereplő minden azonosítónak egyedinek kell lennie. Az aláírásokban a nevek lexikális árnyékolásának szabályát nem tartják be, így a felsorolásuk sorrendje nem számít, de használatuk előtt deklarálni kell a típusokat, így hagyományosan az aláírás elejére kerülnek. tx t

Az aláírás definíciója szintaktikai zárójelben van sig...end. Például egy struktúra Stacka következő aláírással rendelkezik (a fordító automatikusan következtet rá):

struktúra Verem : sig type 'a t = 'a lista val üres : 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) opció vége

Az aláírások fő tulajdonsága , hogy a struktúrákat össze lehet illeszteni velük .  Egy struktúra akkor hasonlítható össze egy adott aláírással, ha legalább az aláírásban felsorolt ​​típusokat, értékeket és beágyazott struktúrákat tartalmazza [8] . Kétféle aláírással illesztett szerkezet létezik: átlátszó ( angol  átlátszó ) és sötét ( angol  opaque ). Általában az aláírási forma megválasztásának lehetőségét az aláírások áttetszőségi tulajdonságának nevezik [  9 ] [ 10] .

A fordító által kikövetkeztetett "alapértelmezett aláírás" általában redundáns, mivel a nyilvánosság elé tárja összetevőinek megvalósítási információit , ami sérti az absztrakciós elvet . Ezért a legtöbb esetben a programozó kifejezetten leírja a kívánt aláírást, és aláírással ( English signature description ) vagy pecsételéssel ( angol pecsételés ) [5] [3] [11] [12] végzi az aláírást , így biztosítva, hogy az az általa választott struktúra el van rejtve a program többi része elől [13] . Pontosabban az illesztett struktúra kötése történik.   

Például egy fejlesztő definiálhat egy aláírást, amely különféle adatfolyamokat ( szekvenciális hozzáférésű adatstruktúrákat ) ír le, és azonosítót rendelhet hozzá:

aláírás STREAM = sig type 'a t val empty : 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * ' a t ) opció vége

Egy szerkezet saját aláírása gazdagíthatja ( eng.  enrich ) azt az aláírást, amellyel az összehasonlítás történik, vagyis több komponenst, több típust tartalmazhat, és ezek a típusok általánosabbak lehetnek. A gazdagítási reláció formálisan így van írva (az aláírás gazdagítja az aláírást ).

Ebben az esetben a következőket írhatja :

Az átlátszó egyezésnek hagyományosan a " S : SS" szintaxisa , míg a sötét egyezésnek a " " szintaxisa S :> SS. Az OCaml készítői azonban teljesen megszüntették az átlátszó illesztés támogatását, ami azt jelenti, hogy az OCaml összes leképezése sötét, de az egyszerűség kedvéért a " " szintaxist használják. S : SS

A legegyszerűbb esetekben az aláírást azonnal aláírhatja anélkül, hogy külön azonosítót rendelne hozzá:

struktúra Verem :> sig type 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) opció vége = struct type 'a t = 'a lista val empty = [] val isEmpty = null val push = op :: val pop = Lista . getItem end

A gyakorlatban azonban a névtelen aláírások meglehetősen ritkák, mivel az aláírások használata nem korlátozódik a rejtőzködésre .

Egy-egy struktúra különböző kontextusokban leképezhető különböző aláírásokhoz, és egy aláírás interfészként szolgálhat különböző struktúrákhoz. Az aláírás a struktúrák egy osztályát határozza meg (az " osztály " kifejezés matematikai értelmében ) [14] . Egy struktúra eltérő "külső nézete" különböző absztrakciós fokokkal több aláírással is biztosítható, eltérő specifikációkkal [15] . A nyilatkozatok sorrendje nem számít, és nem befolyásolja a szerkezetek aláírásokkal való összehasonlíthatóságát.

Ez tekinthető az absztrakt osztályok legegyszerűbb analógjának (az objektum-orientált programozás szempontjából ), abban az értelemben, hogy az aláírás egy közös interfészt ír le , és az ahhoz hasonló struktúrák ezt az interfészt különböző módon valósítják meg. Az ML-ben azonban a szülő-gyermek kapcsolat nincs kifejezetten deklarálva, mivel az ML típusú rendszernek strukturális van, vagyis a struktúra aláírással való illesztése ugyanazzal a mechanizmussal történik, mint az érték 5és a típus párosítása int.

Például definiálhatunk egy olyan struktúrát, amely egy sort valósít meg , de amely szintén összehasonlítható egy aláírással STREAM:

struktúra Sor = struct adattípus 'a t = T of 'a lista * 'a lista val üres = T ([], []) val isEmpty = fn T ([], _) => igaz | _ => false val normalize = fn ([], ys ) => ( rev ys , []) | q => q fun push ( y , T ( xs , ys )) = T ( normalizálás ( xs , y::ys )) val pop = fn ( T ( x::xs , ys )) => SOME ( x , T ( normalizálás ( xs , ys ))) | _ => NINCS vége

Mivel a struktúra Stacknem volt kifejezetten gyengébb aláírással aláírva, a külső program "tudja", hogy a típus tmegegyezik a típussal list, és ezt a tudást felhasználhatja az ilyen típusú objektumok szabványos modulmódszerekkel történő feldolgozására List. Ha a struktúra megvalósítását később módosítani kell Stack(például a verem előre lefoglalt tömbbel történő megjelenítésével ), akkor ehhez át kell írni az összes kódot, amely ezt a tudást használta. Ugyanez igaz a szerkezetre is Queue. Sőt, ha egy modult paramétereztünk saját struct aláírással , akkor nem lehet struktúrát paraméterként átadni neki . StackQueue

Így a szükségtelen információk struktúrákból történő exportálása jelentősen rontja a programok módosíthatóságát . Az absztrakció szintjének növelése érdekében a szerkezeteket gyengébb aláírásokkal kell aláírni, például:

szerkezet Verem :> STREAM = struct type 'a t = 'a lista val üres = [] val isEmpty = null val push = op :: val pop = Lista . getItem end

A struktúra sötét módon van Stackleképezve az aláírásra STREAM, így egy külső program képes lesz teljes mértékben működni a típus értékein Stack.t, de nem fog hozzáférni annak megvalósításához, illetve ennek minden lehetséges értékéhez. írja be, csak az értéket fogja tudni használni Stack.empty(ismét "anélkül, hogy tudná », hogy egyenlő a -val nil). Az ilyen típusú adatok bármilyen feldolgozása absztrakt módon , a megvalósítás figyelembevétele nélkül történik, és csak a és a funkciókon keresztül Stack.pushtörténhet Stack.pop.

De az aláírások sehol nem fontosabbak és hasznosabbak, mint funktorok használatakor [16] .

Öröklődés

A struktúrák egymásba ágyazhatók :

szerkezet E = szerkezet szerkezet A szerkezet B ... vége

Az aláírások természetesen lehetővé teszik a beágyazott struktúrák leírását. Ebben az esetben, mint más esetekben, a struktúrák egymásba ágyazását aláírások, és nem azonos véletlenek alapján vezérlik:

aláírás D = szig szerkezet A : C szerkezet B : C vége

Az aláírások egymásba foglalhatók (szintaxis ) , szekvenciálisan gazdagítva a felületet:include S

aláírás POOR = sig type 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) opció vége aláírás RICH = sig include GYENÉNY val üres : 'a t vége

Megjegyezhető, hogy a leírt szemantika szerint az aláírás aláírását nem kell azonnal elvégezni. Ha egy bizonyos, egymással szorosan összefüggő modulkészletet kell kifejlesztenie, amelyek „barátságosabbak” egymással, mint a program többi részével, akkor a fejlesztés befejezése után a struktúrákat gyengébb aláírásokkal is aláírhatja:

szerkezet SomeModule :> RICH = struct ... vége ... struktúra SomeModule :> POOR = SomeModule

Az utolsó sor nem tekinthető romboló feladatnak . Ez az idióma a lexikális láthatóságon alapszik , amely minden alkalmazó nyelv szemantikájának szerves részét képezi . Mind az ML magjában, mind a modul szintjén a konstrukció x = amindig azt jelenti, hogy egy értéket egy azonosítóhoz kell kötni. A kötés nem hozzárendelés , hanem egy új azonosítót "létrehoz", aminek semmi köze a (esetleg) korábban definiálthoz [17] . Az eredeti struktúra SomeModuletovábbra is létezik a programban, de a következő kód nem fér hozzá azokhoz a komponensekhez, amelyek nem részei a gyengébb aláírásnak (jelen esetben ez egy konstans empty).

A szerkezet megnyitható (szintaxis open S). Ez a legegyszerűbb esetben szintaktikai cukornak tekinthető , amely a modulban foglalt definíciók használatának kényelmét szolgálja ( witha Pascal nyelvi konstrukcióhoz hasonlóan ):

fun foo x = let open SMLofNJ .Cont in fun f x = callcc ( fn k => ... dobja k ...) fun g x = izolálás ... vége

Ha ugyanez megtörténik a program legfelső szintjén (globális környezetben), akkor ez a konstrukció analógjának tekinthető using namespacea C++ nyelvben . Például azok a struktúrák, amelyek szabványos típusokat és műveleteket valósítanak meg rajtuk ( Int, Real, Stringés mások), alapértelmezés szerint nyitva vannak (erről bővebben lásd a számvezérlést ). A struktúrák megnyitásának lehetősége azonban más struktúrákon belül is megvan, és ebben az esetben a nyitás eszközül szolgál a struktúrák egymásba foglalására a funkcionalitás következetes bővítése érdekében (a legegyszerűbb osztályörökléssel analóg módon ). Például:

struktúra B = struktúra nyitott A ... vége

A szerkezet Btartalmazza a szerkezet összes definícióját, Aés kiegészíti azokat új definíciókkal. Ez ugyanaz, mint az összes definíció explicit felsorolása a -n Abelül B. Ennek a lehetőségnek két hátránya van [18] :

  • ha a megnyitandó struktúrában olyan azonosítók találhatók, amelyek megegyeznek az adott kontextusban már meglévő azonosítókkal, akkor az utóbbiak a közvetlen hozzáférés számára elérhetetlenné válnak. Ezzel szemben a megnyitás utáni meghatározások árnyékolják az importált összetevőket. Nincs névütközés - csak az utolsó definíció látható -, de ez kényelmetlen lehet a fejlesztő számára. Kivételt képez, ha a típusnevek egyeznek a meglévő értéknevekkel, mivel az ML fordító mindig meg tudja határozni egy azonosító jelentését a használat kontextusából [19] (lásd a típuskövetkeztetést ). A nevek árnyékolásának problémája különösen akkor fontos, ha két vagy több szerkezetet tartalmaz.
  • Néha nehéz meghatározni, hogy a megnyitott struktúrából pontosan mit is tartalmazzon, különösen akkor, ha olyan nagy struktúrákat nyitunk meg, amelyek nagyszámú azonosítót határoznak meg.

Ezért gyakran javasolt egy rövid helyi azonosító [18] bevezetése a megnyitás helyett , például:

szerkezet SomeModule :> sig fun f x : ... fun g x : ... ... end = struct lokális struktúra C = SMLofNJ . Folytatás ... móka f x = C . _ callcc ( fn k => ... C . dob k ...) fun g x = C . elszigetelni ... _ _

Néha azonban az utolsó definíció elsőbbsége felhasználható egy azonosító szándékos "újradefiniálására" (ami azonban nem túlterhelés ).

Történelmi háttér

Korábban az SML'90 Definícióban [20] volt lehetőség aláírásokban nyitni. Ezt a funkciót kritizálták az öndokumentáció romlása miatt ( az egyik modul interfészének megtanulása közben egy másikra hivatkozik) [21] , és az SML'97 Language Revision-ben eltörölték. Itt fontos megjegyezni, hogy a megnyitás ( open) alapvetően különbözik a beillesztéstől ( include), mivel minden azonosítónak egyedinek kell lennie az aláíráson belül, és a névárnyékolási szabályt nem tartják be, így a beépített aláírásból egy azonosító egyezik meg az aláírásban szereplővel. az új fordítási hibához vezet.

Az SML'90 -ben [20] volt az aláírásnak egy speciális alfaja - abstraction, a közönséges aláírások esetében pedig csak egyfajta illesztés - transzparens ( S : SS). A nyelv 1997 -es átdolgozásakor a modulnyelv ezen része leegyszerűsödött: az absztrakt aláírások helyett  bevezették a sötét ( átlátszatlan ) aláírást ( S :> SS) ( a megoldás a Harper-Lilybridge áttetsző kalkulusán alapul összegek ).

Funktorok

A funktor ( functor) egy struktúrák feletti függvény , vagyis olyan függvény, amely egy struktúrát bemenetként vesz fel és új struktúrát épít fel [22] . Néha egy funktort vizuálisan "paraméterezett struktúrának" tekintünk, vagyis olyan struktúrának, amelynek definícióját a fordító valamilyen más struktúra alapján építi fel a programozó által meghatározott szabályok szerint. Az ortodoxiák azonban azt állítják, hogy a funktorokat sajátos funkcióknak kell tekinteni [23] .

aláírás a funktor paramétertípusának szerepét tölti be . ezzel az aláírással párosítható , az ehhez a típushoz tartozó értékek szerepét tölti be, és átadják a funktornak, hogy értékelje az új struktúrákat [22] . A funktor alkalmazása eredményeként kapott struktúra saját aláírással rendelkezik (bár általánosságban elmondható, hogy nem térhet el a paraméter aláírásától).

A funktor definíció általános formája így néz ki:

Funktor F ( X : S1 ) : S2 = test

Példák a felhasználásra:

struktúra B1 = F ( A1 ) struktúra B2 = F ( A2 ) struktúra B3 = F ( A3 ) ...

A függvények lehetővé teszik a programkomponensek közötti kapcsolatok legkülönbözőbb formáinak típusbiztos leírását, a kódszerkezeti problémák széles skálájának megoldását [ 24] :

  • Általános algoritmusok és függőségkezelés megvalósítása . A függvények lehetővé teszik a hasonló viselkedésű, de eltérő megvalósítású nagy komponensek kombinálását egy programban, és szükség szerint cseréjét. Ez különösen hasznos a gyors prototípuskészítési szakaszban , amikor a rendszert részenként kell tesztelni, vagy egyszerűsített módon szimulálnia kell a viselkedést (lásd például a számvezérlést és a struktúra tesztelését ).
  • A funkcionalitás automatikus bővítése. A funkcionálisok megóvják Önt a rutinmunkától, amikor ugyanazt a funkcionalitást kell megvalósítania különböző típusokhoz. Például, ha különböző adattípusú elemekből szeretnénk halmazokat definiálni, akkor az ML -ben elég egy olyan funktort definiálni, amely egy halmazt definiáló struktúrát generál egy elem típusát meghatározó struktúra alapján. Más nyelveken az ilyen jellegű problémákat generatív programozással oldják meg .
  • Modulok példányosítása beágyazott változtatható állapottal . Ha egy struktúra egy változtatható állapotot tartalmaz , és a programnak több példánya kell, hogy legyen független állapotokkal, akkor a funktorok lehetővé teszik az ilyen struktúrák felépítésének automatizálását.

Ezeket a lehetőségeket szemléltető példákkal illusztráljuk legjobban .

Egyes programozók azonban funkcionátorokat használnak a struktúrák helyett (vagyis leírnak egy funktort, és egy struktúrát úgy határoznak meg, mint az egyetlen alkalmazást egy ismert paraméterre , és néha egy függvényt üres paraméterrel). Ez a megközelítés első pillantásra túlzásnak tűnik, de a gyakorlatban két olyan előnnyel rendelkezik, amelyek növelik a fejlesztők termelékenységét a nagy projektekben [25] [26] :

  • egyrészt az interfészek helyes szervezése azonnal biztosítva van egy alig megírt modul összeállítási szakaszában, és nem a projekt fejlődése során (mert a struktúrák egymástól való függőségét ebben az esetben a típusillesztési mechanizmus szabályozza , ill. nem észlelhető az összeszerelés során)
  • másrészt a struktúrák "függetlenebbé" válnak egymástól, így tetszőleges sorrendben fejleszthetők, és a programozók egy csapatban szabadon dolgozhatnak pontosan ellentétes irányban ( top down vagy bottom up ).

co-use specifikáció erőteljes használatának szükségessége .

Típusegyenértékűség

Nagy léptékű programozáskor, amikor a modulokat összekapcsolva új, összetettebbeket hoznak létre, felmerül a kérdés az ezekből a modulokból exportált absztrakt típusok konzisztenciájáról. A probléma megoldására az ML modul nyelve egy speciális mechanizmust biztosít, amely lehetővé teszi két vagy több típus vagy struktúra azonosságának kifejezett jelzését:

aláírás D = szig struktúra A : C struktúra B : C megosztási típus A .t = B . t vége

Egy ilyen specifikáció megszorítást ír elő a helyettesíthető struktúrák megengedett halmazára vonatkozóan, kimondva azt a követelményt, hogy ezeknek olyan struktúráknak kell lenniük, amelyek megosztják ( eng  . share ) ugyanazt a specifikációt (típus, aláírás vagy struktúra). Így csak azok a struktúrák hasonlíthatók össze az aláírással , amelyekben az azonosító ugyanazt a típust jelenti [27] . Ezért ezt a specifikációt " megosztási kényszernek " nevezik.  Dt

Megjegyzés - az orosz nyelvű irodalomban ennek a kifejezésnek a fordítása nem megoldott. Olyan változatok lehetségesek, mint az „ együtthasználati specifikáció ” [28] , „ megosztási kényszer ”, valamint a szemantikai fordítás „ elválaszthatósági követelmény ” vagy „ megosztási követelmény ” . Létezik [29] a „ megosztásikorlátozások ” fordítása , ami szemantikai hiba.

Szemantikailag egy ilyen specifikációnak két formája létezik - egy az aláírásokhoz és típusokhoz, egy a struktúrákhoz -, de a szintaxisuk azonos. A második forma szigorúbb: két struktúra akkor és csak akkor lehet egyenlő, ha ugyanazon struktúradeklaráció kiértékeléséből, vagy ugyanazon függvény azonos argumentumokra való alkalmazásából származik [28] .

Az együtthasználati specifikációt arra is használják, hogy szűkítsék a típusok körét, amelyek egy adott, számára "túl elvont" aláírás bizonyos használati kontextusában engedélyezettek, például:

functor Try ( Gr : sig type g share type g = int val e : g val bullet : g * g -> g val inv : g -> g end ) = struct val x = Gr . inv ( gr . bullet ( 7 , 9 ) ) vége

Itt a functor paraméter aláírása speciális követelményt támaszt a ténylegesen átadható struktúra összetételére vonatkozóan: a benne használt absztrakt típusnak típusnak g kell lennie int. Az esetek, amikor erre szükség van, meglehetősen gyakoriak, ezért az SML'97-ben [30] , hogy egyszerűsítsük a leírásukat és a névvel ellátott aláírások használatának lehetőségét, egy alternatív konstrukció került be a co-use specifikációhoz: where type( OCaml -ben szintaxis ) : with type

aláírás GROUP = sig type g val e : g val bullet : g * g -> g val inv : g -> g end functor Try ( Gr : GROUP ahol type g = int ) = struct val x = Gr . inv ( gr . bullet ( 7 , 9 ) ) vége

Mindkét kialakításnak megvannak a maga korlátai.

sharinglehetővé teszi a típusok egyenjogúságának kifejezését anélkül, hogy konkrétan meghatároznánk a szerkezetüket. A konstrukció tetszőleges aritású lehet :

aláírás S = szig struktúra A : S struktúra B : S struktúra C : S struktúra D : S megosztási típus A .t = B . t = C. _ t = D . t vége

hanem csak közvetlenül az absztrakt típusokra enged hivatkozni - pl. a forma kifejezése

megosztási típus B .t = A . t * A . t

where typeunáris , és éppen ellenkezőleg, egy absztrakt típust egy ismert típussal példányosítson (de nem teszi lehetővé a már példányosított típus szerkezetének megváltoztatását).

A konstrukciót az OCaml nem támogatja , ezért mindig a . Az utód ML -ben egyetlen leguniverzálisabb konstrukciót kell megvalósítania. sharingwith type

Az absztrakt típusok egyenértékűségének megállapításának másik fontos szempontja a funktorok spawnbilitása .

A szabványos ML a funktorok generatív szemantikáját használja, ami azt jelenti, hogy minden egyes funktor alkalmazása ugyanarra a struktúrára új típusdefiníciókat generál , pl. két azonos nevű és szerkezetben azonos, különböző szerkezetekhez tartozó típus nem egyenlő.

Az OCaml applikatív függvényeket használ, ami azt jelenti, hogy egy funktor alkalmazása bizonyíthatóan egyenlő argumentumokra automatikusan ugyanazt az eredményt generálja. Ez csökkenti az együtthasználati specifikáció szükségességét, és különösen hasznos, ha magasabb rendű függvényekkel foglalkozunk. A 4-es verziótól kezdődően az OCaml lehetőséget ad arra, hogy a funktorokat szülőivé tegye.

Kiterjesztések és nyelvjárások

Magasabb rendű funktorok

A funktor egy, az aláírás által meghatározott struktúrát kap bemenetként. Több struktúra átadásához létre kell hozni egy további burkolóstruktúrát, amely tartalmazza ezeket a struktúrákat, és le kell írni a megfelelő aláírást. A Standard ML nyelv definíciója a kényelem kedvéért előírja a szintaktikai cukrot – több paraméter is átadható sorként , és a fordító automatikusan felépíti a befoglaló szerkezetet és annak aláírását. A core ML azonban magasabb rendű funkciókat biztosít , és a velük való modulszintű analógia követése a funktorok curried formájának bevezetését jelenti. Valójában az egyetlen dolog, amit implementálni kell a nyelven ahhoz, hogy ezt a képességet biztosítsuk, az a funktorok aláírásokban való leírásának támogatása [31] [32] . Ez nem egy alapvető újítás (ellentétben az első osztályú modulokkal ) - a curried funktorok nem engednének semmit , de a klasszikus elsőrendűek nem - azonban elérhetőségük jelentősen leegyszerűsíti a komplex megvalósítását (és így olvashatóságát ) többszintű komponens hierarchiák [32] .

A magasabb rendű funktorok használatának kényelmét szemléltető példa a teljes értékű monád kombinátorok megvalósítása .

A magasabb rendű funktorok megvalósításának lehetőségét már az SML'90 Definíció [20] megjegyzései [31] is megjegyezték . Számos szabványos ML fordító kísérleti kiterjesztésként kínál magasabb rendű függvények megvalósítását [32] . Az Ocaml mindenféle modult szintaktikailag egységes módon valósít meg, így a magasabb rendű funktorok használata a legtermészetesebb.

Megjegyzés - az orosz nyelvű irodalomban [33] összetéveszthető a " magasabb rendű modulok " és az " első osztályú modulok " , ami szemantikai hiba.

Objektumorientált szolgáltatások

Az objektum-orientált programozás teljes támogatása Abadi és Cardelli szerint (lásd Objektum-orientált programozás #OOP altípusainak osztályozása ) egyidejűleg támogatást jelent:

  • altípusos kapcsolatokat
  • tárgyakat
  • objektumtípusok
  • osztályok (objektumgenerátorok)

Mindezt az Ocaml biztosítja hosszú évek óta . Ezenkívül a parametrikus polimorfizmus ezekre a jellemzőkre is kiterjed , ami még kifejezőbbé teszi a nyelvet. Természetesen az OCaml modulnyelvét továbbfejlesztették, hogy lehetővé tegye objektumok és osztályok modulokba való beillesztését.

Ezek a szolgáltatások (esetleg magasabb rendű típusokra is kiterjesztve – lásd a magasabb rendű altípusokat ) az utód ML részévé válnak .

Első osztályú modulok

Probléma

Az eredeti modulnyelv gyengesége, hogy nincs zárva az alapnyelvtől: az alaptípusok és értékek lehetnek modulok összetevői, de a modulok nem lehetnek alaptípusok és -értékek összetevői. Az SML-ben a nyelv két rétegre való szétválasztása szándékosan történt, mivel nagymértékben leegyszerűsítette a típuskonzisztencia-ellenőrző mechanizmust [31] . Ez azonban lehetetlenné teszi a modulok dinamikus összekapcsolását, ami azt jelenti, hogy a következő kifejezés érvénytelen:

struktúra Térkép = ha maxElems < 100 , akkor BinTreeMap egyébként HashTableMap (* klasszikus ML-ben nem engedélyezett! *)

Egy ilyen tiltás szégyen egy ilyen kifejező modulrendszerre nézve, mivel teljesen normális lenne minden objektum-orientált nyelv esetében [34] .

Valójában az ML modul nyelvének nem kell statikusnak lennie [35] (lásd az alacsony szintű reprezentációról szóló részt ). A probléma elsősorban a statikus típusellenőrzésben rejlik , amely az ML természete . Az első osztályú modulok ML-ben való támogatása önmagában nem jelent problémát egy elsőrendű modulnyelv esetén (amely nem tartalmaz funktorokat), de az első osztályú modulok és a magasabb rendű modulok kombinációja teszi szükségessé a nyelv „egy másik valóságba” [36] , azaz hatalmas lehetőségeket nyit meg, de jelentősen megnehezíti mind a nyelv [37] típusainak konzisztenciájának levezetésének és ellenőrzésének mechanizmusait, mind pedig a teljes program optimalizálását . Az első osztályú modulok ötletét Harper és Lilybridge évekig temették el azáltal, hogy a függő típusok elméletével elkészítették az első osztályú modulnyelv idealizált változatát, és bebizonyították, hogy ennek a modellnek a típuskonzisztencia ellenőrzése . eldönthetetlen [9] [38] . Idővel azonban alternatív modellek kezdtek megjelenni, más indoklással.

Csomagok

A 20. század végén Claudio Russo javasolta [39] [40] a modulok első osztályúvá tételének legegyszerűbb módját : a nyelv magjának primitív típusainak listáját kiegészíteni a „ csomag ” ( angol  csomag ) típussal. , amely egy pár структура : сигнатураés a rendszermag-kifejezések listája a becsomagolási és kicsomagolási műveletekkel. Vagyis a nyelvnek csak a magja változik, a modulok nyelve pedig változatlan [41] .

A struktúrák csomagokba való becsomagolása és az azt követő kicsomagolás lehetővé teszi, hogy különböző struktúrákat dinamikusan hozzákössünk az azonosítókhoz (beleértve a funktorok segítségével számítottakat is). A legegyszerűbb példa [42] :

struktúra Térkép = kicsomagolás ( ha maxElemek < 100 akkor pack BinTreeMap : MAP else pack HashTableMap : MAP ) : MAP

Csomag kicsomagolásakor a szerkezetet más aláírással is alá lehet írni, beleértve a gyengébb aláírást is .

Az aláírás kifejezett jelenléte a csomagban megszünteti a típuskövetkeztetés és az illesztés problémáját a struktúra dinamikus kicsomagolása során. Ez cáfolja azt a korai Harper-Mitchell tézist, mely szerint az ML-ben nem lehet struktúrákat első osztályú szintre emelni anélkül, hogy feláldoznánk a fordítási és futási fázisok szétválasztását, valamint a típuskonzisztencia -ellenőrző rendszer eldönthetőségét [41] , mivel az első- rendfüggő típusok , az egzisztenciális típusok elméletének kiterjesztését használják igazolásként másodrendű Mitchell-Plotkin [43] .

Ebben a formában az első osztályú modulok Alice és Ocaml nyelven valósulnak meg , a 4. verziótól kezdve.

1ML

ihlette Rossberg a modulok bedobozolását-kicsomagolását mélyebbre ágyazza a nyelv szemantikájába, így egy monolitikus nyelvet eredményez, amelyben a funktorok, a függvények, sőt a típuskonstruktorok valójában ugyanazok a primitív konstrukciók, és nincs különbség. rekordok , sorok és struktúrák között készül - a nyelv belső reprezentációja egy lapos rendszer F ω . Ez egy sor pozitív eredményt hozott [44] :

  • a nyelv megbízhatóságának bizonyítása sokkal egyszerűbbé válik, mint hagyományosan a modulok nyelve esetében (nem szükséges a függő típusok elméletének alkalmazása );
  • a nyelv magjában a "materializált" ( eng.  reified ) típusok támogatása biztosított, kifejezőerőt biztosítva a nyelvnek a függő típusokkal rendelkező rendszerek szintjén (és ismét nem igényli jelenlétüket a metaelméletben);
  • a nyelv egésze kifejezőbbnek (lehetővé teszi az összetett rendszerek tágasabb és pontosabb leírását) és egyszerűbbnek (minimalisztikusabb és összetételében egységesebb).

A nyelvet " 1ML " -nek hívták , amely egyszerre tükrözi a valóban első osztályú modulok támogatását, valamint a primitívek és modulok egyetlen nyelven való egyesülését (nem két rétegre osztva) [44] .

A döntés Harper-Mitchell azon ötletén alapult, hogy a típusokat "kicsire" és "nagyra" osztják fel. Rossberg ezt a megkülönböztetést a típuskonzisztencia-befoglalási szabályra alkalmazta ( a szerkezet és az aláírás illesztése), így feloldhatóvá tette azt .

Feltehetően az 1ML továbbfejlesztése is elegendő expresszivitást biztosíthat számos érdekes modell támogatásához, amelyek megvalósítása korábban nehéznek számított: típusosztályok , aplikatív funktorok , rekurzív modulok stb. Különösen az inline polimorfizmus bevezetése az 1ML-ben valószínűleg azonnal lehetővé teszi az altípusok szélességben történő kifejezését , ami egyszerűvé teszi a metaelméletet, miközben jelentősen bővíti a képességeit. [45]

MixML

A MixML [10] egy olyan modulnyelv, amely a McQueen klasszikus ML modulnyelvének és a Bracha & Cook mix - ins modell formalizálásának kombinálásával készült .  A MixML szerzői Rossberg és Dreyer.

A MixML alapötlete egyszerű: a struktúrákat és az aláírásokat egyetlen modul koncepcióvá egyesítik, kombinálva a definíciókat és a specifikációkat, mind az átlátható, mind az absztrakt.

Ez lehetővé teszi tetszőleges függőségi gráfok meghatározását a programokban, beleértve a ciklikusakat is. Ez különösen lehetővé teszi, hogy ne csak közvetlen paraméterezést (a kimenet függősége a bemenettől), hanem rekurzív (a bemenet függősége a kimenettől) függvényeket is beépítsen, miközben fenntartja a külön fordítás támogatását (ellentétben sok privát modellel, amely kiterjeszti az ML modul nyelve a rekurzió támogatásával) .

A MixML egyetlen egységes jelölést valósít meg a hagyományosan párosított szemantikai modellekhez (a struktúrákhoz és az aláírásokhoz külön), valamint az ML modulok klasszikus nyelvének számos különálló mechanizmusát, mint például:

  • aláírások öröklése (befoglalása).
  • együtthasználati előírások
  • az aláírás aláírásának két formája (átlátszó és sötét)
  • funktor alkalmazások

Vegyes

A következő bővítmények is elérhetők a különböző modelleken:

  • helyi modulok
  • számos lehetőség a modulok rekurzív rendszeréhez, amelyek lehetővé teszik ciklikus függőségi gráfok kialakítását, amelyek közül a legkifejezőbb a MixML rendszer (a többiek többsége nem biztosítja a külön fordítás lehetőségét)
  • bővített modulbeágyazási támogatás
  • általánosított jelölés a nyitó szerkezetekre
  • különböző lehetőségek az együtthasználat korlátozására
  • beágyazott aláírások, beleértve az absztraktokat is
  • az infix operátorok deklarációi , amelyek az aláírásokon belüli asszociativitást és elsőbbséget adják meg, és pontos egyezést igényelnek

Nyelvi ökoszisztéma

Megvalósítások és dialektusok

Alice

Az Alice nyelv a Standard ML kiterjesztése , amely magában foglalja az utód ML projekt számos ötletét , valamint fejlett, versenyképes programozási eszközöket az elosztott alkalmazások fejlesztéséhez, az erős dinamikus gépelés támogatását és a kényszermegoldót . Andreas Rossberg tervezte.

Az Alice moduljainak nyelve kibővült a komponensek jelölésére ( eng.  komponensek ), amelyek első osztályú modulokat valósítanak meg Russo csomagok formájában, és emellett támogatják a dinamikus gépelést (de a statikus szemantika ugyanazon szabályai szerint) és lusta betöltés (azaz a jövőbeli struktúrák támogatottak és jövőbeli aláírások – lásd a jövőbeli felhívást ) [46] [47] . a típuslevezetést az Alice tiszteletben tartja, és szükség esetén a co-use specifikációt kell használni . A csomagok gyakorlati hasznosságának szemléltető példája az Alice : egy adatsorosító könyvtár , amely lehetővé teszi a szálak dinamikus típusok és adatok cseréjét.

Ezenkívül az Alice szintaktikai cukrot biztosít - lehetőséget ad a zárójelek szabad használatára a modulnyelvi kifejezésekben, beleértve a hagyományos "zárójelek" struct...endhelyett sig...end:

val p = csomag ( érték x = hossz ) : ( érték x : 'a lista -> int ) (* val p : csomag = csomag{|...|} *) OCaml

Az Ocaml programban a modulnyelv szintaxisa egységes:

modul típusa S = (* aláírás *) sig ... modul M : T (* beágyazott szerkezet *) vége modul X : S = (* struct *) struct ... vége modul F ( X : S ) = (* paraméterezett szerkezet (függvény) *) struct ... vége modul G ( X : S ) ( Y : T ) = (* curryed paraméterezett struktúra (magasabb rendű függvény) *) struct ... vége

A szemantikában azonban számos különbség van [48] .

A 4- es verziótól kezdve az Ocaml támogatja az első osztályú modulokat Alice csomagjaihoz hasonló jelöléssel . A szintaxis továbbra is homogén, vagyis úgy néz ki, hogy nem lehet megkülönböztetni a beágyazott struktúráktól az aláírásokban.

Megalakulása óta az Ocaml a modulnyelvet osztályokkal és objektumokkal bővíti .

A Standard ML és az Ocaml közötti legfontosabb különbségek a típusekvivalencia szemantikában jelennek meg (lásd a típusekvivalenciáról szóló részt ).

Modulkezelés

Óriási ML programok összekapcsolásához elvileg a legtöbb nyelvhez hagyományos linkerek használhatók , mint például a make . Az SML modulnyelv azonban sokkal erősebb, mint más nyelvek modularizációs eszközei [2] , és a make nem támogatja annak előnyeit, és még inkább nem alkalmas a programok vezérlési folyamatának globális elemzésére [49] . Ezért a különböző fordítók saját modulkezelő rendszereiket kínálják: Compilation Manager (CM) SML /NJ és MLBasis System (MLB) MLton nyelven . Az SML.NET [50] beépített függőségi nyomkövető rendszerrel rendelkezik. Az MLton tartalmaz egy .cm - .mlb fájlkonvertálót is .

A legtöbb megvalósítás külön fordítást használ, ami gyors fordítási időt eredményez. A REPL módban történő külön fordítás támogatásához egy függvényt használnak use, amely lefordítja a megadott fájlt és importálja a definíciókat. Egyes fordítók (például az MLton ) nem támogatják a REPL -t , ezért nem valósítják meg a támogatást a use. Mások (például Alice ) éppen ellenkezőleg, a programvégrehajtás során a modulok dinamikus fordításának és betöltésének további funkcióit valósítják meg. A Poly/ML [51] egy olyan funkciót biztosít, PolyML.ifunctoramely lehetővé teszi egy funktor-implementáció interaktív, részenkénti hibakeresését.

Programpéldák

Egyszerűsége ellenére a modulnyelv rendkívül rugalmas, és magas szintű kód-újrafelhasználást tesz lehetővé , amint azt a következő példák szemléltetik.

számjegyek számának kezelése

A hagyományos adattípusok , például egész számok ( intés word), valódi ( real), karakterek ( charés widechar), karakterlánc ( stringés widestring), tömbök ( vectorés array) és mások, az ML dialektusokban valósulnak meg, nem primitív típusok és beépített operátorok formájában. a legtöbb nyelvhez hasonlóan, de absztrakt adattípusok és megfelelő függvények formájában, amelyeket az aláírások tartalmaznak, INTEGER, WORD, REAL, CHAR, STRINGstb., szabványos könyvtárak formájában. A konkrét nyelvi megvalósítások nagyon hatékonyan tudják megjeleníteni ezeket az absztrakt típusokat (például az MLton a tömböket és a karakterláncokat ugyanúgy ábrázolja, mint a C nyelv ).

Például:

aláírás INTEGER = sig eqtype int val toLarge : int -> LargeInt . int val fromLarge : LargeInt . int -> int val toInt : int -> Int . int val fromInt : Int . int -> int érték pontosság : Int . int opció val minInt : int opció val maxInt : int opció val ˜ : int -> int val * : ( int * int ) -> int val div : ( int * int ) -> int val mod : ( int * int ) - > int val quot : ( int * int ) -> int val rem : ( int * int ) -> int val + : ( int * int ) -> int val - : ( int * int ) -> int val összehasonlítás : ( int * int ) -> order val > : ( int * int ) -> bool val > = : ( int * int ) -> bool val < : ( int * int ) -> bool val < = : ( int * int ) -> bool val abs : int -> int val min : ( int * int ) -> int val max : ( int * int ) -> int val jel : int -> Int . int val sameSign : ( int * int ) -> bool val fmt : StringCvt . radix -> int -> string val toString : int -> string val fromString : string -> int opció val scan : StringCvt . radix -> ( char , 'a ) StringCvt . olvasó -> 'a -> ( int * 'a ) opció vége

A , , , és még sok más szerkezet INTEGERösszehasonlítható az aláírással . Hasonlóképpen a / és / struktúrák (és esetleg mások is) illeszthetők aláírásokkal / , és minden változathoz a funktorok megfelelő I/O veremet generálnak ( , ). Int8Int16Int32Int64IntInfCHARSTRINGCharStringWideCharWideStringStreamIOTextIO

Ugyanakkor egyes struktúrák elrejtik a hagyományos gépi ábrázolást az absztrakt definíció alatt (például , Int32) Int64, mások - bitmezőket (például Int1), és a struktúra hosszú aritmetikátIntInf valósít meg . Ugyanakkor a könyvtárak intenzíven bejárhatnak sok-sok kapcsolatokat : az SML Basis specifikáció kötelező és választható modulokat határoz meg , amelyek a "primitív" típusok megvalósítására épülnek: monomorf tömbök, azok nem másoló szeletei stb. . Még a "string" ( ) és a "substring" ( ) típusok is az SML Basis specifikációban és (vagy és for ) néven vannak definiálva . Így ahhoz, hogy ugyanazokat az algoritmusokat különböző kapacitású számokkal használjuk, elegendő a megfelelő struktúrát kifejezetten átadni a megnyitása nem változtatja meg a már kiszámított struktúrákat). stringsubstringChar.char vectorChar.char VectorSlice.sliceWideChar.char vectorWideChar.char VectorSlice.sliceWideString

A különböző fordítók különböző megvalósított struktúrákat biztosítanak. Az MLton a leggazdagabb választékot kínálja : tól Int1-ig , Int32és ig Int64, ugyanazt a készletet Word(előjel nélküli egész számokhoz), valamint IntInf(a GNU Multi-Precision Library által megvalósítva ) és sok további készletet, például Int32Array, PackWord32Big, PackWord32Littleés így tovább.

A legtöbb megvalósításban alapértelmezés szerint a legfelső szinten (globális környezetben) egy struktúra Int32(vagy Int64) nyitva van, vagyis a típus intés egy művelet +használata alapértelmezés szerint egy típus Int32.intés egy művelet Int32.+(vagy, ill Int64.int. Int64.+). Ezen túlmenően a és azonosítók Intis rendelkezésre állnak LargeInt, amelyek alapértelmezés szerint bizonyos struktúrákhoz vannak kötve (például LargeIntáltalában egyenlő a -val IntInf). A különböző fordítók, tájolásuktól függően, alapértelmezés szerint eltérő kötéseket használhatnak a globális környezetben, és ez a finomság befolyásolhatja a programok fordítóprogramok közötti hordozhatóságát. Például egy konstans Int.maxInta lehető legnagyobb egész szám értékét tartalmazza, egy opcionális típusba csomagolva, és vagy mintaillesztéssel , vagy függvényhívással kell lekérni valOf. Véges dimenziós típusok esetén az érték , és mindkét kinyerési módszer egyenértékű. De egyenlő , így a tartalom közvetlen elérése a következőn keresztül kivételt jelent . Alapértelmezés szerint a Poly/ML fordítóban [51] nyitva van, mivel a számtörő problémákra összpontosít . IntN.maxIntSOME(m)IntInf.maxIntNONEvalOf OptionIntInf

Absztrakt halmazok

Az OCaml könyvtárak tartalmaznak egy funkciót biztosító modult . Segítségével könnyedén összeállíthat egy adott elemtípus alapján készletet: SetMake

module Int_set = Beállítás . Gyártmány ( struktúra típusa t = int hagyd összehasonlítani = összehasonlítani vége )

A generált egész számkészlet modul a következő fordítóval rendelkezik - kikövetkeztetett aláírás:

modul Int_set : sig type elt = int type t val empty : t val is_empty : t -> bool val mem : elt -> t -> bool val add : elt -> t -> t val singleton : elt -> t val remove : elt -> t -> t val union : t -> t -> t val inter : t -> t -> t val diff : t -> t -> t val összehasonlítás : t -> t -> int val egyenlő : t -> t -> bool val részhalmaz : t -> t -> bool val iter : ( elt -> unit ) -> t -> unit val fold : ( elt -> ' a -> ' a ) -> t -> ' a -> ' a val for_all : ( elt -> bool ) -> t -> bool val létezik : ( elt -> bool ) -> t -> bool val szűrő : ( elt -> bool ) -> t -> t val partíció : ( elt -> bool ) -> t -> t * t val kardinális : t -> int val elemek : t -> elt lista val min_elt : t -> elt val max_elt : t -> elt val válassz : t -> elt val split : elt -> t -> t * bool * t val find : elt -> t -> elt end

Hasonló funkciókat tartalmaznak az SML/NJ fordítókönyvtárak ( ListSetFn). Az SML Basis csak elemi eszközöket biztosít.

Az egyszerű struktúra helyett egy függő modul használatának fő célja az, hogy az összehasonlító függvényt egyszer adjuk meg , és egy adott típusú halmaz összes függvénye ugyanazt az összehasonlító függvényt használja a halmaz elemeinek típusára, így a programozó így meg van védve a saját hibáitól. Az absztrakt halmazok úgy valósíthatók meg, hogy minden függvényt minden alkalommal átadunk a halmazon egy összehasonlító függvényt (ahogy ez például a C qsort nyelv szabványos függvényében történik – lásd a parametrikus polimorfizmust C és C nyelvben ++ ), ez azonban nem csak megnöveli a halmazokkal végzett munka bonyolultságát, de azzal a kockázattal is jár, hogy összekeverjük a szükséges összehasonlító függvényt, mivel nehezen észlelhető hibát viszünk be a programba (lásd a kódduplikációt ).

Sajnos [24] a történelem során az OCaml olyan aláírást fogadott el az összehasonlító függvényhez, amely egy kétirányú ( logikai ) típusú visszatérési értékét jelzi (és az ilyen konvenciókat figyelembe kell venni a könyvtári modulok széles körben történő használatához). . Erőteljesebb az SML Basis (valamint a Haskell Prelude ) megoldás, amely háromutas típuson alapul:

adattípus sorrend = KEVESEBB | EQUAL | NAGYOBB val összehasonlítás : int * int -> sorrend

Szerkezeti tesztelés

A gyors prototípuskészítésnél gyakran szükség van a rendszer részleges tesztelésére vagy a viselkedés egyszerűsített szimulálására (az úgynevezett "csonkok" megvalósítása). A funkcionálisok kecsesen kezelik ezt a feladatot.

Tegyük fel például, hogy valamilyen adatszerkezetnek három különböző megvalósítása van , mondjuk egy sor [52] :

aláírás QUEUE = sig type 'a t kivétel E val üres : 'a t val enq : 'a t * 'a -> 'a t val null : 'a t -> bool val hd : 'a t -> 'a val deq : 'a t -> 'a t end struktúra Queue1 :> QUEUE = struct ... vége struktúra Queue2 :> QUEUE = struct ... vége struktúra Queue3 :> QUEUE = struct ... vége

Sok nyelven az absztrakció hiánya miatt külön másoló-beillesztési programokat kellene létrehozni az összehasonlításhoz . A függvények viszont lehetővé teszik, hogy a tesztet elvonja a megvalósítástól, és egyetlen programban ismételje meg őket:

functor TestQueue ( Q : QUEUE ) = struct fun fromList I = foldl ( fn ( x , q ) => Q . enq ( q , x )) Q . üres I fun toList q = if Q . null q , majd [] else Q . hd q :: toList ( Q . deq q ) end val ns = legfeljebb ( 1 , 10000 ) (* val ns = [1, 2, 3, 4, ...] : belső lista *) struktúra TQ1 = TestQueue ( Queue1 ) val q1 = TQ1 . fromList ns val l1 = TQ1 . toList q1 l1 = ns (* igaz : bool *) ... struktúra TQ2 = TestQueue ( Queue2 ) struktúra TQ3 = TestQueue ( Queue3 ) ...

Ezután választhat a szélesség -első keresés és a mélység -első keresés között az egyes megvalósításokhoz, mindezt egyetlen programban:

functor BreadthFirst ( Q : QUEUE ) = struct ... end functor DepthFirst ( Q : QUEUE ) = struct ... end struktúra BF_Q1 = BreadthFirst ( Queue1 ) struktúra BF_Q2 = Breadth First ( Queue2 ) struktúra BF_Q3 = Breadth First ( Queue3 ) struktúra DF_Q1 = DeepFirst ( Queue1 ) struktúra DF_Q2 = DeepthFirst ( Queue2 ) struktúra DF_Q3 = DeepthFirst ( Queue3 ) ...

A jövőben az "extra" megvalósításokat nem kell törölni. Sőt, a teljesen optimalizáló fordítók, mint az MLton , maguktól is eltávolítják őket – lásd a holt kód eltávolítását .

Ezzel a módszerrel a hatékonyságot is mérhetjük, de a gyakorlatban sokkal kényelmesebb (és megbízhatóbb) a fordítóba épített profilerrel mérni.

Az összetevők közötti függőségek globális típusú biztonsága , amelyet a modul nyelve biztosít, látható egy hibás függvényhasználati kísérlet példáján:

struktúra Rossz = BreadthFirst ( Lista ); (* > Hiba: nem egyező típus specifikáció: t > Hiba: nem egyező kivételspecifikáció: E > Hiba: nem egyező val spec: üres > Hiba: nem egyező val spec: enq > Hiba: nem egyező val spec: deq *)

Monádok és típusosztályok

A Haskell , amely az ML leszármazottja, nem támogatja az ML modul nyelvét. Ehelyett támogatja a nagyszabású programozást (a legtöbb nyelvben használthoz hasonló triviális modulrendszer mellett) monádokon és típusosztályokon keresztül . Az előbbiek absztrakt viselkedést fejeznek ki, beleértve a változó állapot modellezését a hivatkozási átlátszóság szempontjából ; ez utóbbiak eszközül szolgálnak a típusváltozók számszerűsítésének szabályozására az ad-hoc polimorfizmus megvalósításával . Az ML modul nyelve lehetővé teszi mindkét idióma [53] [11] megvalósítását .

A típusosztály nem más, mint egy interfész, amely olyan műveletek halmazát írja le, amelyek típusát egy osztályparaméternek nevezett független absztrakt típusváltozó adja meg. Ezért egy osztály természetes reprezentációja a modulnyelv szempontjából olyan aláírás lesz, amely a szükséges műveletek mellett egy típusspecifikációt is tartalmaz (egy osztályparamétert ábrázolva) [11] :

aláírás EQ = sig type t val eq : t * t -> bool end

A monád az aláírással valósul meg:

aláírás MONAD = sig type 'a monad val ret : 'a -> 'a monad val bnd : 'a monad -> ( 'a -> 'b monad ) -> 'b monád vége

Példák a felhasználására:

struktúra Opció : MONAD = struct type 'a monad = 'a opció fun ret x = NÉHÁNY x fun bnd ( NÉHÁNY x ) k = k x | bnd NINCS k = NINCS vége aláírás REF = sig type 'a ref val ref : 'a -> 'a ref IO . monad val ! : 'a ref -> 'a IO . monad val : = : 'a ref -> 'a -> unit IO . monád vége

A teljes értékű monád kombinátorok különösen kényelmesek a magasabb rendű funktorok használatával [32] [53] :

(*Első rendelés*) aláírás MONOID = sig típus t érték : t val plusz : t * t - > t vége Funktor Prod ( M : MONOID ) ( N : MONOID ) = struktúra típusa t = M. _ t * N . t val e = ( M . e , N . e ) móka plusz (( x1 , y1 ), ( x2 , y2 )) = ( M . plusz ( x1 , x2 ), N . plusz ( y1 , y2 )) vége Funktor Négyzet ( M : MONOID ) : MONOID = Prod M M struktúra Sík = Négyzet ( típus t = valós érték e = 0,0 val plusz = Valós . + ) val x = Sík . plusz ( Sík . e , ( 7.4 , 5.4 )) (*nagyobb sorrend*) aláírás PROD = MONOID -> MONOID -> MONOID Funktor Négyzet ( M : MONOID ) ( Prod : PROD ) : MONOID = Prod M M struktúra T = Square Plane Prod val x = T . plusz ( T.e , T.e ) _ _ _ _ (*Átláthatóan*) aláírás PROD' = fct M : MONOID -> fct N : MONOID -> MONOID ahol t = M típus . t * N . t functor Square' ( M : MONOID ) ( Prod : PROD' ) : MONOID = Prod M M struktúra T' = Négyzet' Plane Prod val x = T' . plusz ( T' . e , (( 7.4 , 5.4 ), ( 3.0 , 1.7 )

Az értékek típus szerint indexelve

A típusok szerint indexelt értékek az ML család összes korai nyelvében közös idióma , amelyet az ad-hoc polimorfizmus ( funkció túlterhelés ) megvalósítására terveztek parametrikus polimorfizmuson keresztül [54] . A típusosztályok, amelyeket először a Haskellben vezettek be , nyelvi szinten támogatják a típusindexelt értékeket (és mint ilyenek, könnyen megvalósíthatók a modulnyelvben ).

A legegyszerűbb formájában ezt az idiómát a következő OCaml -példa szemlélteti [55] :

modul típusa Arith = sig típus t val (+) : t -> t -> t val neg : t -> t val nulla : t vége modul Build_type ( M : Arith ) = struct let typ x = { Type . plusz = M . (+); neg = M. _ (-); nulla = M . nulla ; } vége let int = let module Z = Build_type ( Int ) in Z . typ let int64 = let module Z = Build_type ( Int64 ) in Z . typ let int32 = let module Z = Build_type ( Int32 ) in Z . typ let native = let module Z = Build_type ( Native_int ) in Z . typ let float = let module Z = Build_type ( Float ) in Z . typ let complex = let module Z = Build_type ( Complex ) in Z. _ típus

Objektummodell

A modulnyelv használatával egyszerű objektummodellt hozhat létre dinamikus elküldéssel. Ez a példa érdekes, mivel az SML nem biztosít semmilyen objektum-orientált programozási lehetőséget , és nem támogatja az altípusokat .

A legegyszerűbb dinamikusan elküldhető objektummodell könnyen beépíthető SML -ben a -n keresztül . A függvényértékeket tartalmazó bejegyzéstípus egy absztrakt osztály szerepét tölti be, amely meghatározza a metódus aláírását. Ezen objektumok belső állapotának és privát metódusainak elrejtését az ML lexikai hatóköre biztosítja; így a lezárások (ML függvények) betölthetik az ebbe az osztályba tartozó objektumok konstruktorának szerepét. Egy ilyen megvalósítás nem teszi lehetővé összetett, többszintű öröklődési hierarchiák felépítését (ehhez altípusok megvalósítása szükséges, ami típusok szerint indexelt értékek komplex megvalósításával történik, és amelyre többféle módszer létezik), de a gyakorlatban ez is elég. a legtöbb feladathoz jó tervezéssel [12] . Az alábbiakban egy ilyen objektummodell modulszintre való levezetését tekintjük át.

A legegyszerűbb adatfolyamok alapulnak:

aláírás ABSTRACT_STREAM = sig type 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) opció vége aláírás STREAM = sig include ABSTRACT_STREAM val üres : 'a t end szerkezet Verem :> STREAM = struct type 'a t = 'a lista val üres = [] val isEmpty = null val push = op :: val pop = Lista . getItem end structure Queue :> STREAM = struct adattípus 'a t = T of 'a lista * 'a lista val üres = T ([], []) val isEmpty = fn T ([], _) => igaz | _ => false val normalize = fn ([], ys ) => ( rev ys , []) | q => q fun push ( y , T ( xs , ys )) = T ( normalizálás ( xs , y::ys )) val pop = fn ( T ( x::xs , ys )) => SOME ( x , T ( normalizálás ( xs , ys ))) | _ => NINCS vége

Funktorok segítségével általánosított algoritmusokat valósíthat meg , amelyek egy ismeretlen belső eszköz és cél adatfolyamait manipulálják:

functor StreamAlgs ( ST : ABSTRACT_STREAM ) = struct nyitott ST fun pushAll ( xs , d ) = foldl push d xs fun popAll d = let fun lp ( xs , NONE ) = rev xs | lp ( xs , SOME ( x , d )) = lp ( x::xs , pop d ) in lp ([], pop d ) vége fun cp ( from , to ) = pushAll ( popAll from , to ) end

Ennek a függvénynek az aláíráshoz hasonló struktúrákkal való példányosítása ABSTRACT_STREAMolyan függvényeket eredményez, amelyek manipulálják a megfelelő adatfolyamokat:

struktúra S = StreamAlgs ( Stack ) struktúra Q = StreamAlgs ( Queue ) S. _ popAll ( S . pushAll ([ 1 , 2 , 3 , 4 ], Stack . üres )) (* eredmény: [4,3,2,1] *) K. _ popAll ( Q . pushAll ([ 1 , 2 , 3 , 4 ], Queue . üres )) (* eredmény: [1,2,3,4] *)

Megjegyzendő, hogy a funktor StreamAlgsegy aláírási paramétert vesz fel ABSTRACT_STREAM, a és a struktúrákat Stackpedig a aláírást gazdagító Queuealáírással írták alá . Ez egy finomságot rejt magában: a fejlesztés során kívánatos követni az adott nyelvjárás szabványkönyvtárában elfogadott konvenciókat a meglévő fejlesztések, különösen a standard funktorok szélesebb körű felhasználása érdekében (az SML Basis-ben nincs ilyen sok). 2004, de néhány fordító kiterjesztésében és az OCaml -ben nagyon érdekes példák találhatók). STREAMABSTRACT_STREAM

A származtatott struktúrák ST.ta függvényparaméterből származó típusdefiníciót tartalmazzák, de különböző típusúak: az ML-ben minden típusdefiníció új típust generál. Ezért az összekeverési kísérlet típuskonzisztencia hibát eredményez . Például a következő sort a fordító elutasítja:

val q = Q. _ push ( 1 , halom . üres )

A szálosztály interfésze kényelmesen definiálható: . Típusbiztonsági okokból célszerű nem típusaliast használni, hanem egy konstruktor függvényt , amely egy ilyen bejegyzést osztályobjektumra képez le:

szerkezet Stream = struct adattípus 'a t = I of { isEmpty : unit -> bool , push : 'a -> 'a t , pop : unit -> ( 'a * 'a t ) option } fun O m ( I t ) ) = m t fun isEmpty t = O #isEmpty t () fun push ( v , t ) = O #push t v fun pop t = O #pop t () vége

A modul Streamténylegesen megvalósítja az aláírást ABSTRACT_STREAM( ), de az explicit aláírást későbbre halasztja.

Ahhoz, hogy egy szál modult szálosztálygá alakítsunk, hozzá kell adni két névre szóló konstruktort , amit egy funktorral és a nyitókonstrukcióval lehet megtenni :

functor StreamClass ( D : STREAM ) : STREAM = struct open Stream fun make d = I { isEmpty = fn () => D . isEmpty d , push = fn x => make ( D . push ( x , d )), pop = fn () => case D . pop d of NONE => NINCS | SOME ( x , d ) => SOME ( x , make d ) } val empty = I { isEmpty = fn () => true , push = fn x => make ( D . push ( x , D . üres )), pop = fn () => NINCS } vége

A funktor által generált struktúra StreamClasstartalmazza a struktúra összes komponensét Stream(beleértve a konstruktort I is ), de ezek kívülről nem láthatók, mivel a funktor eredményét az aláírás írja alá STREAM.

Végül lezárhatja a modult Stream:

struktúra Stream : ABSTRACT_STREAM = Stream

Ez típusbiztonsági szempontból nem szükséges , mivel a modul Streamnem teszi lehetővé a tokozás feltörését, ahogy volt. A konstruktor elrejtése azonban Igarantálja, hogy csak a funktor StreamClasshasználható alosztályok létrehozására ABSTRACT_STREAM.

Nyilvánvaló használati esetek:

struktúra StackClass = StreamClass ( Stack ) struktúra QueueClass = StreamClass ( Queue )

De ez még nem minden. Mivel a fent definiált függvény StreamAlgsbemenetként egy típusú struktúrát vesz fel ABSTRACT_STREAM, példányosítható egy olyan szerkezettel Stream, amely megvalósítja az absztrakt adatfolyam osztályt:

struktúra D = StreamAlgs ( Stream )

A származtatott modul D, akárcsak a modul Stream, minden olyan osztállyal működik, amely a -tól öröklődik ABSTRACT_STREAM, ami dinamikus küldésnek tekinthető:

D. _ popAll ( D . pushAll ([ 1 , 2 , 3 , 4 ], StackClass . üres )) (* eredmény: [4,3,2,1] *) D. _ popAll ( D . pushAll ([ 1 , 2 , 3 , 4 ], QueueClass . üres )) (* eredmény: [1,2,3,4] *)

Érdekes megjegyezni, hogy sem Stream, sem Dnem csak változtatható állapotot tartalmaz , hanem konstansokat sem - csak típusokat és függvényeket -, azonban a paramétermechanizmuson áthaladva az absztrakt osztályt itt tulajdonképpen első osztályú értékként használjuk , és nem csak egy virtuális entitás, mint sok objektum-orientált nyelvben.

A nyelvről

Alacsony szintű reprezentáció és hatékonyság

Hagyományosan a struktúrákat a fordítóban rekordok , a funktorokat pedig az ilyen rekordok feletti függvények ábrázolják [35] . Vannak azonban alternatív belső reprezentációk, mint például a Harper-Stone szemantika és az 1ML .

A funktorok használata egy nagy projekt lebontásának eszközeként azt jelenti, hogy lelassítja a hozzáférést a rajtuk keresztül kiszámított programok végső komponenseihez, és minden egyes beágyazási szintnél a veszteségek megsokszorozódnak, ugyanúgy, mint az azonnali értékek helyett közönséges függvények használatakor. A teljesen optimalizáló fordítók ( MLton , MLKit [56] , SML.NET [50] ) a ténylegesen bevitt struktúrák sajátosságait figyelembe véve kibővítik a modul keretrendszert és felépítik a funktor komponensek végső definícióit, ami kiküszöböli a teljesítménybüntetést. Az MLKit modulbővítést is használ a régiók kikövetkeztetésére, ami lehetővé teszi a nyelv használatát valós idejű alkalmazások fejlesztésére . Ebben az esetben a modulok keretrendszerének nyilvánosságra hozatala különféle stratégiákkal valósítható meg: például az MLton végrehajtja a „ program-defunktorálást ”, az MLKit pedig „ a modulnyelv statikus értelmezését ”. Az OCaml számára létezik egy opcionális defunctorizer [57] megvalósítása .

A szemantika indoklása

Az ML modulnyelvet hosszú éveken át típuselméleti szinten a függő típusok elméletének alkalmazásaként tekintették , és ez lehetővé tette a nyelv véglegesítését és tulajdonságainak alapos vizsgálatát. A valóságban a modulok (még egy első osztályú szerepkörben sem) nem " igazán függőek ": egy modul aláírása függhet a másik modulban található típusoktól , de nem a benne lévő értékektől [3 ] .

Részletek Mitchell-Plotkin levelezés Erős McQueen összegek

[58]

Átlátszó Harper-Lilybridge összegek

Robert Harper és Mark Lillibridge megszerkesztette [9] [59] az áttetsző összegszámítást , hogy formálisan igazolja a magasabb rendű első osztályú modulok nyelvezetét .  Ezt a számítást a Harper-Stone szemantikában használják . Ezenkívül elemei a felülvizsgált SML-definíció (SML'97) részévé váltak.

A Harper-Stone szemantikája

A Harper-Stone szemantika ( röviden HS szemantika ) az SML értelmezése típusos keretrendszerben .  Ez utóbbi egy Harper-Lilybridge áttetsző összegeken alapuló moduli rendszert tartalmaz (lásd fent). Az értelmezés elméletileg elegáns, de fenntartja azt a hamis benyomást, hogy az ML modulokat nehéz megvalósítani: szimpla típusokat , függő típusokat és összetett hatásrendszert használ [3] .

Rossberg-Rousseau-Dreyer F-transzformáció

Andreas Rossberg, Claudio Russo és Derek Dreyer közösen kimutatták, hogy a közhiedelem a modulnyelvek indokolatlanul magas belépési küszöbéről hamis. Megszerkesztették a modulok nyelvének transzformációját egy lapos F ω rendszerré ( másodrendű lambda-számítás ), ezzel megmutatva, hogy maga a modulok nyelve valójában csak egy speciális esete ( szintaktikai cukor ) az F ω rendszer használatának . Ebben az értelemben a modulok használatának fő előnye az F ω rendszerben történő közvetlen munkához képest a számos összetett művelet jelentős automatizálása (aláírás-illesztés a dúsítás figyelembevételével, az egzisztenciális adatok implicit be-/kicsomagolása stb.).

Az „ F-ing semantics ” ( F-ing semantics ) vagy az F-transzformáció támogatja a magasabb rendű függvényeket és az első osztályú modulokat Rousseau-csomagok formájában. Az F-transzformáció megbízhatóságának bizonyítását a Coq -ban a "locally nameless" ( Locally Nameless ) módszerrel gépesítették . A szerzők rendkívül fájdalmasnak értékelték az elvégzett munkát, és nem javasolják ennek a módszernek a használatát a jövőben [3] . Az elért eredmények tovább inspirálták Rossberget 1ML megalkotására .

Kritika és összehasonlítás az alternatívákkal

Az ML modulnyelv a programozási nyelvek legfejlettebb modulrendszere [2] , és folyamatosan fejlődik. Szabályozást biztosít a névtér - hierarchiák (a keresztül ) , a finomszemcsés felületek (a aláírásokon keresztül ), a kliensoldali absztrakció (a funktorokon keresztül ) és az implementátor oldali (a gépelésen keresztül ) felett . 3 ] .

A legtöbb nyelv nem rendelkezik a funktorokkal [52] . A funktorokhoz a legközelebbi analóg a későbbi C++ osztályú sablonok , de a funktorok sokkal könnyebben használhatók [60] , mert a C++ sablonok nem csak típusbiztosak , de számos egyéb hátrányuk is van [61] . Egyes nyelvek makró-alrendszereket biztosítanak , amelyek lehetővé teszik az automatikus kódgenerálást és a fordítási idejű függőségek rugalmas kezelését ( Lisp , C ), de gyakran ezek a makróalrendszerek ellenőrizhetetlen kiegészítői a fő nyelvnek, lehetővé téve a programsor tetszőleges átírását. by-line, ami sok problémához vezethet [62] . Csak a 21. században fejlesztettek ki olyan makro-alrendszereket, amelyek típusbiztosak ( Template Haskell , Nemerle ), amelyek egy része funktorokkal egyidejűleg is elérhető (MetaML [63] , MetaOCaml ).

A funktorokban az a nagyszerű, hogy akkor is lefordíthatók és típusellenőrzhetők, ha a programban nincs olyan struktúra, amelyet tényleges paraméterként át lehetne adni [64] . Ennek során a funktorok interakciót írnak le az interfészek szintjén, nem pedig a megvalósítások szintjén , lehetővé téve a fordítási idő függőségek feltörését. Ez általában némi teljesítményromlás rovására megy, de a teljes programoptimalizálási módszerek sikeresen megoldják ezt a problémát .

A modulok nyelvezetét gyakran nehezen érthetőnek tartják, aminek oka az igazoláshoz szükséges összetett matematikában rejlik. Simon Peyton-Jones egy Porsche autóhoz hasonlította a funktorokat „ nagy teljesítményük, de rossz ár-érték arányuk miatt ” [65] . Az ML támogatói nem értenek egyet ezzel a nézőponttal, és azzal érvelnek, hogy a modulnyelv használata/végrehajtása/érthetősége semmivel sem nehezebb, mint a Haskell -féle típusú osztályok vagy a Java osztályrendszere generikus és helyettesítő karakterekkel [ , és valójában szubjektív preferencia kérdése. [3] .

Ha a fordító hibát észlel a moduldefiníciókban, akkor a kimeneti hibaüzenetek nagyon hosszúak lehetnek, ami különösen a magasabb rendű funktorok esetében okozhat különösebb kényelmetlenséget. Ezért a típusdefiníciók és a felettük lévő függvények blokkját csak azután kell modulként formázni, miután részenként kifejlesztették (amelyhez a REPL mód a legtöbb megvalósításban rendelkezésre áll ). Egyes implementációk (pl . Poly/ML [51] ) saját kiterjesztést biztosítanak a probléma megoldására. Mások (például SML2c) éppen ellenkezőleg, csak modulszintű programok fordítását teszik lehetővé.

Történelem, filozófia, terminológia

A modulnyelv elve az, hogy a programok nagyszabású szemantikája meg kell ismételje a mag ML ( eng.  Core ML ) szemantikáját, vagyis a nagy programkomponensek közötti függőségek úgy fogalmazódnak meg, mint egy kis függősége. szint. Ennek megfelelően a struktúrák a modulszint "értékei" ( angol  modulszintű értékek ); aláírások (más néven " modultípusok " vagy " modultípusok ") a modulszintű értékek "típusait" , míg a funktorok a modulszint "funkcióit" jellemzik. Az analógia azonban nem azonos: mind a modulok tartalma, mind a modulok közötti kapcsolatok bonyolultabbak lehetnek, mint a nyelv magjában. Ebben az értelemben a legjelentősebb bonyodalmak az alépítmények aláírásokba foglalása és a >>> együttes használatának korlátozása 4] . Az SML'90 definícióval kapcsolatos megjegyzésekben [31] a magasabb rendű funktorok (nagyobb rendű függvényekkel való analógiák) lehetséges implementációja is fel lett jegyezve, de ezek megvalósítása később jelent meg .

A modul nyelvét eredetileg David MacQueen javasolta [66 ] .  A jövőben sok tudós járult hozzá a legjelentősebb módon a típuselméleti igazoláshoz és a modulok nyelvének bővítéséhez. A munka magában foglalja a rekurzív , beágyazott, lokális, magasabb rendű és első osztályú modulok formalizálását , valamint indoklásuk ismételt átdolgozását annak érdekében, hogy mind magát a modellt, mind az azt támogató metaelméletet leegyszerűsítsük és bizonyítsuk. megbízhatóság. A modulnyelv fejlesztése szorosan keresztezi az ML mag fejlődését, és számos tudós több tucatnyi munkája jelzi, de a következő kulcsfontosságú mérföldköveket lehet megkülönböztetni:

  • 1984 – McQueen – kezdeti ötlet [66] .
  • 1990 – Milner, Harper, McQueen, Tofty – a Definíció részeként a nyelv magjától elkülönülő modell, megbízhatóságának bizonyítéka az úgynevezett generatív típusú pecsételéssel [20] .
  • 1994 – Appel, McQueen – külön összeállítás [6] .
  • 1995 - Leroy - a metaelmélet egyszerűsítése transzparens típusokra (nem generáló), applikatív funktorokra [67] .
  • 1994 - Harper, Lilybridge - Típuselméleti alapozás függő típusokkal [9] .
  • 1999-2000 - Rousseau - a metaelmélet leegyszerűsítése másodrendűre, első osztályú modulok csomagok formájában [39] [40] .
  • 2000 - Harper-Stone szemantika .
  • 2010 - Rossberg, Rousseau, Dreyer - a metaelmélet egyszerűsítése F lapos rendszerré , megbízhatóságának bizonyításának gépesítése a Coq -ban [3] .
  • 2015 - Rossberg - 1ML , egyetlen modell a nyelv magjával [34] .

Az ML másik dialektusa - a Caml nyelv - eredetileg számos eltéréssel támogatta a modulnyelvet . Ezt követően az Objective Caml nyelvvé fejlődött , amely a modulnyelvet kiegészítette egy objektum-orientált programozási alrendszerrel , amely szervesen fejleszti a modulnyelv gondolatait . Az OCaml folyamatosan fejlődött, és a 2010-es évek közepére modulnyelve számos kísérleti funkcióval egészült ki. Az SML egyes megvalósításai némelyik szolgáltatást bővítményként támogatják. A legjelentősebb újítás az első osztályú modulok, amelyeket az Alice nyelv is támogat .

Alkalmazás

Különféle nyelveken

A modulnyelv szemantikája teljesen független attól, hogy az ML szigorú nyelv – a lusta nyelvekben is használható [68] . Ezen túlmenően a modulnyelv privát megvalósításait javasolták a szemantikailag különböző nyelvek (például Prolog és Signal ) magjain felül.

A nyelvek paraméteres növekedése

2000-ben Xavier Leroy (az OCaml fejlesztője ) egy általánosított generatív modell megvalósítását javasolta, amely lehetővé teszi az ML modulnyelv felépítését egy tetszőleges (meglehetősen széles tartományban lévő) nyelv magjára, saját típusrendszerével ( például C ) [1] . Ezt a modellt magán a modulnyelven keresztül valósítjuk meg - egy funktor formájában , a nyelv magjával kapcsolatos adatokkal és a típuskonzisztencia-ellenőrző mechanizmus leírásával paraméterezve .

Modulok, mint a nyelv magjának alapja

A modulnyelv három évtizedes evolúciója után, mint a nyelv magjának kiegészítése , 2015-ben Andreas Rossberg (az Alice fejlesztője) javasolta a modulnyelv hagyományos felépítését . alapnyelv, hogy a modulnyelvet köztes nyelvként használjuk az alapnyelv konstrukcióinak megjelenítéséhez. Ez teszi a modulokat valóban első osztályú értékké (nem kell csomagolni) - lásd 1ML .

Jegyzetek

  1. ↑ 12 Leroy, "Modular Module System", 2000 .
  2. ↑ 1 2 3 Cardelli, "Típusos programozás", 1991 , 2. Típusnyelvek, p. 5.
  3. ↑ 1 2 3 4 5 6 7 8 Rossberg, Russo, Dreyer, "F-ing Modules", 2010 .
  4. ↑ 1 2 Harper, "Programozás SML-ben", 2011 .
  5. ↑ 1 2 3 Dreyer, "Evolving the ML Module System", 2005 .
  6. ↑ 1 2 Appel, MacQueen, "Separate Compilation for Standard ML", 1994 .
  7. ↑ Harper, "Intro to SML", 1986 , p. ötven.
  8. ↑ Paulson, "ML for the Working Programmer", 1996 , 7.4 A várólistára szánt aláírás, p. 264.
  9. ↑ 1 2 3 4 Harper, Lillibridge, "Típuselméleti megközelítés a magasabb rendű modulokhoz megosztással", 1994 .
  10. ↑ 1 2 Dreyer, Rossberg, "MixML", 2008 .
  11. ↑ 1 2 3 Dreyer, Harper, "Moduláris típusosztályok", 2007 .
  12. ↑ 1 2 Objektum-orientált programozás szabványos ML-ben
  13. ↑ Paulson, "ML for the Working Programmer", 1996 , 2.22 Aláírások, p. 62.
  14. ↑ Paulson, "ML for the Working Programmer", 1996 , 2.19 Bevezetés a modulokba, p. 59.
  15. ↑ Paulson, "ML for the Working Programmer", 1996 , 7.5 Aláírási megszorítások, p. 264.
  16. ↑ Pucella, "Megjegyzések az SML/NJ programozáshoz", 2001 , p. 58.
  17. ↑ Harper, "Intro to SML", 1986 , p. 13.
  18. ↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 7.14 A opennyilatkozat, p. 299-305.
  19. ↑ Harper, "Intro to SML", 1986 , p. 36.
  20. ↑ 1 2 3 4 Az SML meghatározása, 1990 .
  21. ↑ Appel, "A Critique of Standard ML", 1992 , aláírásokban nyitott, p. 17.
  22. ↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , Útmutató a modulokhoz, p. 309.
  23. ↑ Object Mix: Funktorok és futási idő vs fordítási idő
  24. ↑ 1 2 Minsky fordította: DMK, 2014 , 9. fejezet Funktorok.
  25. ↑ Harper, "Intro to SML", 1986 , p. 75-76.
  26. ↑ Paulson, "ML for the Working Programmer", 1996 , 7.13 Teljesen funkcionális programozás, p. 294.
  27. ↑ Harper, "Intro to SML", 1986 , p. 77.
  28. ↑ 1 2 Harper, "Intro to SML", 1986 , p. 77-78.
  29. ↑ Minsky fordítása: DMK, 2014 .
  30. ↑ Az SML meghatározása: Revised, 1997 .
  31. ↑ 1 2 3 4 Kommentár az SML-hez, 1991 .
  32. ↑ 1 2 3 4 HOF SML/NJ-ben .
  33. ↑ Minsky fordítása: DMK, 2014 , p. 235.
  34. ↑ 1 2 Rossberg, "1ML - Core and Modules United", 2015 .
  35. ↑ 1 2 Frisch, Garrigue, "First-class modules in OCaml", 2010 .
  36. ↑ Rossberg - Funktorok és futási idő vs fordítási idő .
  37. ↑ Neis, Dreyer, Rossberg, "Non-Parameterric Parametricity", 2009 , p. 1-2.
  38. ↑ Rossberg, „1ML – Core and Modules United”, 2015 , p. 2.
  39. ↑ 1 2 Russo, "Non-Dependent Types for Modules", 1999 .
  40. ↑ 1 2 Russo, "Első osztályú szerkezetek", 2000 .
  41. ↑ 1 2 Russo, "Első osztályú szerkezetek", 2000 , p. 17.
  42. ↑ Alice - Packages .
  43. ↑ Russo, "Első osztályú struktúrák", 2000 , p. tizennégy.
  44. ↑ 1 2 Rossberg, „1ML – Core and Modules United”, 2015 , p. 3.
  45. ↑ Rossberg, „1ML – Core and Modules United”, 2015 , p. 13.
  46. ↑ Rossberg, "Dinamikus komponensek", 2006 .
  47. ↑ Alice - ExtModules .
  48. ↑ SML vs. OCaml .
  49. ↑ M.L.Basis
  50. ↑ 1 2 SML.NET fordító
  51. ↑ 1 2 3 Poly/ML fordítóoldal
  52. ↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 7.8 A sorstruktúrák tesztelése, 1. o. 274.
  53. ↑ 1 2 Harper: "Természetesen az ML-nek vannak monádjai!" .
  54. ↑ Típusindexelt értékek
  55. ↑ Yaron Minsky – Útmutató a programozóknak a típusindexelt értékekhez
  56. ↑ MLKit fordítóprogram (downlink) . Letöltve: 2015. január 21. Az eredetiből archiválva : 2016. január 7.. 
  57. ↑ Defunctorizer for OCaml .
  58. ↑ MacQueen, "Dependent type to express modules", 1986 .
  59. ↑ Reynolds, "Programozási nyelvek elméletei", 1998 , 18. Modulspecifikáció, p. 398-410.
  60. ↑ Vanden Berghe .
  61. ↑ K. Czarnecki, J. O'Donnell, J. Striegnitz, W. Taha. DSL megvalósítás a metaocaml-ban, a haskell sablonban és a C++-ban . — University of Waterloo, University of Glasgow, Research Center Julich, Rice University, 2004. Az eredetiből archiválva : 2016. március 5..
  62. ↑ Appel, "A Critique of Standard ML", 1992 , Makrók hiánya, p. 9.
  63. ↑ Steven E. Ganz, Amr Sabry, Walid Taha . Makrók többlépcsős számításokként: típusbiztos, generatív, kötő makrók a MacroML-ben . - International Conference on Functional Programming, ACM Press, 2001. Az eredetiből archiválva : 2015. szeptember 23.
  64. ↑ Tofte, "Essentials of SML Modules", 1996 .
  65. ↑ Simon Peyton Jones . Hajpóló viselése: retrospektív Haskellről. – POPL, 2003.
  66. ↑ 1 2 MacQueen, "Modules for Standard ML", 1984 .
  67. ↑ Xavier Leroy, "Applicative functors", 1995 .
  68. ↑ Tofte, "Essentials of SML Modules", 1996 , p. egy.

Irodalom

Oktatóanyagok, útmutatók, kézikönyvek, használat

Szabványos ML nyelv
  • Robert Harper . Bevezetés a Standard ML-be (határozatlan idejű). - Carnegie Mellon Egyetem, 1986. - ISBN PA 15213-3891.
    • Orosz nyelvű fordítás:
      Robert Harper. Bevezetés a Standard ML  -be (neopr.) . - Carnegie Mellon Egyetem, 1986. - 97 p. — ISBN PA 15213-3891.
  • Lawrence C. Paulson. ML for the Working Programmer  (neopr.) . — 2. - Cambridge, Nagy-Britannia: Cambridge University Press, 1996. - 492 p. - ISBN 0-521-57050-6 (kemény kötés), 0-521-56543-X (puha kötés).
OCaml nyelv
  • Minsky, Madhavapeddy, Hickey. Valós világ OCaml: Funkcionális programozás tömegek számára  (határozatlan idejű) . - O'Reilly Media, 2013. - 510 p. — ISBN 9781449324766 .
    • Orosz nyelvű fordítás:
      Minsky, Madhavapeddy, Hickey. Programozás OCaml nyelven  (neopr.) . - DMK, 2014. - 536 p. — (Funkcionális programozás). - ISBN 978-5-97060-102-0 .
Modul nyelve
  • A modul nyelve . (Emmanuel Chailloux, Pascal Manoury és Bruno Pagano Développement d'applications avec Objective Caml online verziójának fejezete)
  • Michael P. Fourman. SML modulok (  (angol) ). – 2010.

Történelem, elemzés, kritika

  • Robin Milner , Mads Tofte, Robert Harper. A szabványos ML definíciója  (neopr.) . - The MIT Press, 1990. - ISBN 0-262-63181-4 .
  • Luca Cardelli . Tipikus programozás( (angol)) // IFIP State-of-the-Art Reports. - New York: Springer-Verlag, 1991. -Vol. A programozási fogalmak formális leírása. –S. 431–507.
  • Andrew W. Appel. A Standard ML kritikája (  angolul ). — Princetoni Egyetem, a CS-TR-364-92 átdolgozott változata, 1992.
  • John C. Reynolds. Programozási nyelvek elméletei . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (keménykötés), 978-0-521-10697-9 (puhakötés).
  • Claudio Russo. Non-Dependent Types for Modules (  ( angolul ) ) // A deklaratív programozás alapelvei és gyakorlata. — A deklaratív programozás alapelvei és gyakorlata, 1999.
  • Xavier Leroy. A Modular Module System (  (angol) ) // 10. kötet, 3. szám. - Journal of Functional Programming, 2000. - S. 269-303 .
  • Andreas Rossberg, Claudio Russo, Derek Dreyer. F-ing modulok (  (angol) ). – TLDI, 2010.

Linkek