ML-modulspråk

ML-modulspråket är ett modulsystem som främst används i programmeringsspråk i ML - familjen , som har applikativ semantik, med andra ord är det ett litet funktionellt språk som fungerar med moduler [1] .

Det är det mest utvecklade modulsystemet bland de som finns i programmeringsspråk [2] [3] .

Allmän information

I sin enklaste form består ett modulspråk av tre typer av moduler:

Signaturen kan betraktas som en beskrivning av strukturen respektive strukturen som implementeringen av signaturen. Många språk tillhandahåller liknande konstruktioner, vanligtvis under olika namn: signaturer kallas ofta för gränssnitt eller paketspecifikationer, och strukturer kallas ofta för implementeringar eller paket. Oavsett terminologi är tanken att tilldela en typ till ett helt stycke kod. Till skillnad från många språk, i ML, är förhållandet mellan signaturer och strukturer många - till - många snarare än många-till-en eller en - till-en . En signatur kan beskriva många olika strukturer, och en struktur kan motsvara många olika signaturer. De flesta andra språk är bundna av starkare restriktioner, vilket kräver att en given struktur har en enda signatur, eller att en given signatur härleds från en enda struktur. Detta är inte fallet för ML [4] .

I vanliga objektorienterade språk som C++ eller Java tillhandahålls abstraktion genom klasser som kombinerar ett antal funktioner ( arv , subtyping och dynamisk utsändning ) i ett koncept samtidigt, vilket gör dem svåra att formalisera och kan leda till oönskade konsekvenser vid vårdslös användning. Till skillnad från klasser fokuserar ML-modulspråket helt på abstraktion , vilket ger ett brett utbud av dess former och ger en solid formell grund för deras studier. [5] Det tillhandahåller namnrymdshierarkihantering , finkornig anpassning av gränssnittet , abstraktion på implementersidan och abstraktion på klientsidan .

Funktioner är ett unikt koncept som inte har någon motsvarighet på de flesta språk . De är funktioner över strukturer, det vill säga de beräknar nya strukturer baserat på de som redan beräknats, naturligtvis, i enlighet med vissa signaturer. Detta gör att du kan lösa en mängd olika problem med att strukturera komplexa program .

I det här fallet är två krav uppfyllda [6] :

I praktiken används inte alltid möjligheten till separat kompilering - det finns fulloptimerande kompilatorer som öppnar ramverket för moduler för att avsevärt öka prestandan för program .

Språk

Strukturer och signaturer

Miljö ( eng.  environment ) i kärnan ML ( eng.  Core ML ) är en samling definitioner ( typer , inklusive funktionella , och värden , inklusive funktionella och exklusiva ). Miljön är lexikalt anpassad .

En struktur ( structure) är en "materialiserad" miljö, förvandlad till ett värde som kan manipuleras [7] . I förhållande till tidiga implementeringar av modulspråket är denna definition något av en konvention, eftersom strukturer från början kunde definieras eller utvärderas endast på kodens översta nivå (i den globala miljön). Efterföljande arbete utvecklar modulspråket till en förstklassig nivå .

Införandet av begreppet struktur kräver en översyn av definitionen av miljö i kärnan av språket. Från och med nu är miljön en samling av typer, värderingar och strukturer. Följaktligen är en struktur en samling av typer, värderingar och andra strukturer. Rekursiv kapsling av strukturer är inte tillåten, även om vissa implementeringar stödjer dem [5] .

Det huvudsakliga sättet att definiera strukturer är inkapslade deklarationer , det vill säga deklarationer inom syntaktiska parenteser struct...end. Till exempel implementerar följande struktur en stack , som definierar den interna organisationen av objekt av den algebraiska typen "stack" och den minsta nödvändiga uppsättningen funktioner över den:

struct typ 'a t = 'en lista val tom = [] val isEmpty = null val push = op :: val pop = Lista . getItem slut

"Värdet" av denna inkapslade deklaration är en struktur. För att använda detta värde måste du tilldela en identifierare till det:

struktur Stack = struct typ 'a t = 'en lista val tom = [] val isEmpty = null val push = op :: val pop = Lista . getItem slut

Strukturkomponenter kan nu nås via sammansatta (eller kvalificerade) namn, som Stack.push, Stack.empty : Stack.t.

Signaturen ( signature) är en uppräkning av beskrivningarna av elementen i strukturen, det vill säga strukturens gränssnitt . Varje element i denna uppräkning kallas en specifikation. Om typen anges för ett värde i signaturen måste identifieraren i strukturen vara bunden till ett värde av typen . Du kan tänka på en signatur som en slags " typ " av en struktur, men en signatur är inte en typ i strikt mening, eftersom en typ är en uppsättning värden och ett "signaturvärde" kan innehålla typer (som i ML är inte värden). Varje identifierare i signaturen måste vara unik. Regeln om lexikal skuggning av namn i signaturer följs inte, så ordningen för deras uppräkning spelar ingen roll, men typer måste deklareras innan de används, så traditionellt placeras de i början av signaturen. x tx t

Signaturdefinitionen är skriven inom syntaktiska parenteser sig...end. Till exempel har en struktur Stackföljande signatur (kompilatorn härleder den automatiskt):

struktur Stack : sig typ 'a t = 'en lista val tom : 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) alternativ slut

Den huvudsakliga egenskapen hos signaturer är att strukturer kan matchas mot dem .  En struktur är jämförbar med en given signatur om den innehåller åtminstone de typer, värden och kapslade strukturer som anges i signaturen [8] . Det finns två former av matchande strukturer med signaturer: transparent ( engelska  transparent ) och mörk ( engelska  opaque ). I allmänhet kallas möjligheten att välja signeringsform för signaturers genomskinlighetsegenskap [  9 ] [ 10] .

Den från kompilatorn härledda "standardsignaturen" är vanligtvis överflödig, eftersom den exponerar implementeringsinformationen för dess komponenter för allmänheten, vilket är ett brott mot abstraktionsprincipen . Därför, i de flesta fall, beskriver programmeraren uttryckligen den önskade signaturen och utför signering med en signatur ( English  signature description ) eller försegling ( English  sealing ) [5] [3] [11] [12] , vilket säkerställer att komponenterna i struktur vald av honom är dolda från resten av programmet [13] . Mer exakt utförs bindningen

Till exempel kan en utvecklare definiera en signatur som beskriver olika dataströmmar ( datastrukturer med sekventiell åtkomst) och tilldela en identifierare till den:

signatur STREAM = sig skriv 'a t val tom : 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * ' a t ) alternativ slut

En strukturs egen signatur kan berika ( eng.  enrich ) signaturen som jämförelsen görs med, det vill säga innehålla fler komponenter, fler typer, och dessa typer kan vara mer generella. Anrikningsrelationen skrivs formellt som (signatur berikar signatur ).

I det här fallet kan du skriva :

Transparent matchning har traditionellt S : SSsyntaxen " ", medan mörk matchning har syntaxen " " S :> SS. Men skaparna av OCaml har helt släppt stödet för transparent matchning, vilket betyder att alla mappningar i OCaml är mörka, men syntaxen " " används för enkelhetens skull. S : SS

I de enklaste fallen kan du signera en signatur omedelbart utan att tilldela den en separat identifierare:

struktur Stack :> sig skriv 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) alternativ slut = struct typ 'a t = 'en lista val tom = [] val isEmpty = null val push = op :: val pop = Lista . getItem slut

Men i praktiken är namnlösa signaturer ganska sällsynta, eftersom användningen av signaturer inte är begränsad till att gömma sig .

En struktur i olika sammanhang kan mappas till olika signaturer och en signatur kan fungera som gränssnitt för olika strukturer. Signaturen definierar en klass av strukturer (i den matematiska betydelsen av termen " klass ") [14] . En annan "vy utifrån" för en struktur, med olika grader av abstraktion , kan tillhandahållas av flera signaturer med olika specifikationer [15] . Ordningen på deklarationerna spelar ingen roll och påverkar inte jämförbarheten av strukturer med signaturer.

Detta kan ses som den enklaste analogen av abstrakta klasser (i termer av objektorienterad programmering ), i den meningen att en signatur beskriver ett gemensamt gränssnitt och strukturer som är jämförbara med det implementerar det gränssnittet på olika sätt. Men i ML deklareras inte förälder-barn-relationen explicit, eftersom ML -typsystemet har strukturell , det vill säga matchning av en struktur med en signatur utförs av samma mekanism som att matcha ett värde 5med en typ int.

Till exempel kan man definiera en struktur som implementerar en kö , men som också är jämförbar med en signatur STREAM:

struktur Kö = struct datatype 'a t = T av 'en lista * 'en lista val tom = T ([], []) val isEmpty = fn T ([], _) => sant | _ => false val normalize = fn ([], ys ) => ( rev ys , []) | q => q rolig push ( y , T ( xs , ys )) = T ( normalisera ( xs , y::ys )) val pop = fn ( T ( x::xs , ys )) => NÅGRA ( x , T ( normalisera ( xs , ys ))) | _ => INGET slut

Eftersom strukturen Stackinte var explicit signerad med en sämre signatur, "vet" det externa programmet att typen tär identisk med typen listoch kan använda denna kunskap för att bearbeta objekt av denna typ med standardmodulmetoder List. Om implementeringen av strukturen senare behöver ändras Stack(till exempel genom att representera stacken med en förallokerad array ), kommer detta att kräva omskrivning av all kod som använde denna kunskap. Detsamma gäller för struktur Queue. Dessutom, om en modul har parametriserats med sin egen struct-signatur , kommer det inte att vara möjligt att skicka en struct som en parameter till den . StackQueue

Export av onödig information från strukturer försämrar således programens modifierbarhet avsevärt . För att öka abstraktionsnivån bör strukturer signeras med sämre signaturer, till exempel:

struktur Stack :> STREAM = struct typ 'a t = 'en lista val tom = [] val isEmpty = null val push = op :: val pop = Lista . getItem slut

Strukturen är Stackmappad till signaturen STREAMpå ett mörkt sätt, så ett externt program kommer att kunna arbeta fullt ut på värdena av typ Stack.t, men kommer inte att ha tillgång till dess implementering och alla möjliga värden av detta typ, kommer den att kunna använda endast värdet Stack.empty(igen, "utan att veta » att det är lika med nil). All behandling av data av denna typ kommer att utföras abstrakt , utan att ta hänsyn till dess implementering, och det kan endast göras genom funktionerna Stack.pushoch Stack.pop.

Men ingenstans är signaturer viktigare och mer användbara än när man använder funktorer [16] .

Arv

Strukturer kan kapslas inuti varandra:

struktur E = struktur struktur A struktur B ... slut

Naturligtvis låter signaturer dig beskriva kapslade strukturer. I det här fallet, som i andra fall, styrs kapslingen av strukturer baserat på signaturer och inte på identiska sammanträffanden:

signatur D = sig struktur A : C struktur B : C slut

Signaturer kan inkluderas (syntax include S) i varandra, vilket sekventiellt berikar gränssnittet:

signatur DÅLIG = sig typ 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) alternativ slut signatur RICH = sig include DÅLIG val tom : 'a t end

Det kan noteras att enligt den beskrivna semantiken behöver signatursignering inte göras omedelbart. Om du behöver utveckla en viss uppsättning av nära sammankopplade moduler som är mer "vänliga" med varandra än med resten av programmet, kan du efter att utvecklingen är klar signera strukturerna med sämre signaturer:

struktur SomeModule :> RICH = struktur ... slut ... struktur SomeModule :> DÅLIG = SomeModule

Den sista raden ska inte betraktas som en destruktiv uppgift . Detta formspråk är baserat på lexikal synlighet , som är en integrerad del av semantiken för alla applicerande språk . Både i kärnan av ML och på modulnivå innebär konstruktion x = aalltid att binda ett värde till en identifierare. Bindning är inte en tilldelning , den "skapar" en ny identifierare som inte har något att göra med den (eventuellt) tidigare definierade [17] . Den ursprungliga strukturen SomeModulefinns fortfarande i programmet, men efterföljande kod har inte tillgång till de av dess komponenter som inte är en del av den sämre signaturen (i det här fallet är det en konstant empty).

Strukturen kan öppnas (syntax open S). I det enklaste fallet kan detta betraktas som syntaktisk socker , vilket tjänar till att använda definitionerna inkapslade i modulen (analogt med konstruktionen withpå Pascal- språket ):

fun foo x = låt öppna SMLofNJ .Fortsätt in fun f x = callcc ( fn k => ... kasta k ...) fun g x = isolera ... slut

Om detsamma görs på programmets översta nivå (i den globala miljön), kan detta betraktas som en analog till konstruktionen using namespacei C++-språket . Till exempel är strukturer som implementerar standardtyper och operationer på dem ( Int, Real, Stringoch andra) öppna som standard (för mer om detta, se nummerkontroll ). Möjligheten att öppna strukturer finns dock även inuti andra strukturer, och i detta fall fungerar öppningen som ett verktyg för att inkludera strukturer i varandra för att konsekvent utöka funktionaliteten (analogt med det enklaste klassarv ). Till exempel:

struktur B = struktur öppen A ... slut

Strukturen Bomfattar alla definitioner av strukturen Aoch kompletterar dem med nya definitioner. Detta är samma sak som att explicit lista alla definitioner Ainom B. Denna möjlighet har två nackdelar [18] :

  • om det finns identifierare i strukturen som öppnas som matchar de identifierare som redan finns i det givna sammanhanget, så kommer de senare att bli otillgängliga för direkt åtkomst. Omvänt kommer definitioner efter öppning att skugga importerade komponenter. Det finns ingen namnkonflikt - bara den sista definitionen är synlig - men detta kan vara obekvämt för utvecklaren. Undantaget är om typnamn matchar befintliga värdenamn, eftersom ML- kompilatorn alltid kan bestämma betydelsen av en identifierare utifrån sammanhanget för dess användning [19] (se typinferens ). Problemet med att skugga namn är särskilt relevant när man inkluderar två eller flera strukturer.
  • ibland blir det svårt att avgöra exakt vad som ingår i den öppnade strukturen, speciellt när man öppnar stora strukturer som definierar ett stort antal identifierare.

Därför rekommenderas det ofta att använda introduktionen av en kort lokal identifierare [18] istället för att öppna , till exempel:

struktur SomeModule :> sig fun f x : ... fun g x : ... ... end = struktur lokal struktur C = SMLofNJ . Fortsätt in ... kul f x = C . callcc ( fn k => ... C . throw k ...) fun g x = C . isolera ... _ _

Men ibland kan den sista definitionens företräde användas för att avsiktligt "omdefiniera" en identifierare (som dock inte är en överbelastning ).

Historisk bakgrund

Tidigare, i SML'90 Definition [20] , var det möjligt att öppna i signaturer. Denna funktion kritiserades på grund av försämringen av självdokumentation (att lära sig gränssnittet för en modul medan du använder den tvingar dig att hänvisa till en annan) [21] , och den avskaffades i SML'97 Language Revision. Det är viktigt att notera här att öppning ( open) skiljer sig fundamentalt från inkludering ( include), eftersom varje identifierare måste vara unik i signaturen och regeln för namnskuggning inte följs, så att en identifierare från den inkluderade signaturen som matchar den i signaturen ny leder till ett kompileringsfel.

I SML'90 [20] fanns det en speciell underart av signatur - abstraction, och för vanliga signaturer fanns det bara en form av matchning - transparent ( S : SS). När språket reviderades 1997 förenklades denna del av modulspråket: istället för abstrakta signaturer introducerades  mörk ( ogenomskinlig ) matchning med signaturen ( S :> SS) ( lösningen är baserad på kalkylen för Harper-Lilybridge translucent summor ).

Funktioner

En funktor ( functor) är en funktion över strukturer , det vill säga en funktion som tar en struktur som input och bygger en ny struktur [22] . Ibland ses en funktor visuellt som en "parameteriserad struktur", det vill säga en struktur vars definition är byggd av kompilatorn på basis av någon annan struktur enligt reglerna som specificeras av programmeraren. Ortodoxier hävdar dock att funktorer bör ses som speciella funktioner [23] .

Signaturen spelar rollen som funktionatorns parametertyp . Alla typer av strukturer som kan matchas med denna signatur spelar rollen som värden som hör till denna typ och skickas till funktionären för att utvärdera nya strukturer [22] . Strukturen som erhålls som ett resultat av applicering av funktionorn har sin egen signatur (även om den generellt sett kanske inte skiljer sig från parameterns signatur).

Den allmänna formen av en funktionsdefinition ser ut så här:

funktion F ( X : S1 ) : S2 = kropp

Exempel på användning:

struktur B1 = F ( A1 ) struktur B2 = F ( A2 ) struktur B3 = F ( A3 ) ...

Funktioner tillåter dig att på ett typsäkert sätt beskriva de mest skilda formerna av relationer mellan programkomponenter och lösa ett brett spektrum av kodstruktureringsproblem [24] :

Dessa möjligheter illustreras bäst med illustrativa exempel .

Vissa programmerare använder dock funktorer istället för strukturer (det vill säga de beskriver en funktor och definierar en struktur som dess enda tillämpning på en känd parameter , och ibland en funktor med en tom parameter). Detta tillvägagångssätt verkar överdrivet vid första anblicken, men i praktiken ger det två fördelar som ökar produktiviteten för utvecklare i stora projekt [25] [26] :

  • å ena sidan säkerställs den korrekta organisationen av gränssnitt omedelbart vid kompileringsstadiet av en knappt skriven modul, och inte när projektet utvecklas (eftersom strukturernas beroende av varandra i detta fall styrs av typmatchningsmekanismen , och inte upptäcks under montering)
  • å andra sidan blir strukturer "mer oberoende" av varandra, så att de kan utvecklas i valfri ordning, och programmerare i ett team är fria att arbeta i exakt motsatta riktningar ( uppifrån och ned eller nedifrån ).

samanvändningsspecifikationen .

Typ ekvivalens

Vid programmering i stor skala , när moduler länkas för att skapa nya, mer komplexa, uppstår frågan om konsekvensen av abstrakta typer som exporteras från dessa moduler. För att lösa detta problem tillhandahåller ML-modulspråket en speciell mekanism som låter dig explicit ange identiteten för två eller flera typer eller strukturer:

signatur D = sig struktur A : C struktur B : C delar typ A.t = B. _ _ t slut

En sådan specifikation sätter en begränsning på den tillåtna uppsättningen utbytbara strukturer, och deklarerar kravet att dessa måste vara strukturer som delar ( eng  . share ) användningen av samma specifikation (typ, signatur eller struktur). Således är endast de strukturerna jämförbara med signaturen , där identifieraren betyder samma typ [27] . Därför kallas denna specifikation " sharing constraint ".  Dt

Observera - i den ryskspråkiga litteraturen har översättningen av denna term inte fastställts. Varianter som " samanvändningsspecifikation " [28] , " delningsbegränsning ", såväl som semantisk översättning " separabilitetskrav " eller " delningskrav " är möjliga . Det finns [29] översättningen " sharingrestrictions " , vilket är ett semantiskt fel.

Semantiskt finns det två former av en sådan specifikation - en för signaturer och typer, en för strukturer - men deras syntax är identisk. Den andra formen är mer restriktiv: två strukturer kan vara lika om och endast om de är resultatet av att utvärdera samma strukturdeklaration eller tillämpa samma funktion på lika argument [28] .

Samanvändningsspecifikationen används också för att tvinga fram en inskränkning av intervallet av typer som är tillåtna i en viss användningskontext av en signatur som är "överabstrakt" för den, till exempel:

funktor Försök ( Gr : sig typ g delningstyp g = int val e : g val bullet : g * g -> g val inv : g - > g end ) = struct val x = Gr . inv ( Gr . kula ( 7 , 9 ) ) slut

Här ställer signaturen för funktorparametern ett speciellt krav på sammansättningen av strukturen som faktiskt kan överföras till den: den abstrakta typen som g används i den måste vara en typ int. De fall där detta är nödvändigt är ganska vanliga, så i SML'97 [30] för att förenkla deras beskrivning och möjligheten att använda namngivna signaturer lades en alternativ konstruktion till för sambruksspecifikationen: where type(i OCaml syntax ) : with type

signatur GROUP = sig typ g val e : g val bullet : g * g -> g val inv : g -> g end functor Försök ( Gr : GROUP där typ g = int ) = struct val x = Gr . inv ( Gr . kula ( 7 , 9 ) ) slut

Båda designerna har sina begränsningar.

sharinglåter dig uttrycka likheten mellan typer utan att specifikt specificera deras struktur. Konstruktionen kan ha godtycklig aritet :

signatur S = sig struktur A : S struktur B : S struktur C : S struktur D : S delar typ A.t = B. _ _ t = C. _ t = D. _ t slut

men låter dig referera till abstrakta typer endast direkt - d.v.s. formens uttryck

delningstyp B .t = A . _ t * A . t

where typeär unär och är tvärtom avsedd att instansiera en abstrakt typ av en känd typ (men tillåter inte att ändra strukturen för en typ som redan har instansierats).

>>> konstruktionen stöds inte i OCaml , så du bör alltid använda . I efterföljaren ML , är det tänkt att implementera en enda mest universell konstruktion. sharingwith type

En annan viktig aspekt för att fastställa ekvivalensen av abstrakta typer är funktionsförmågan .

Standard ML använder funktionsgenerativa semantik, vilket innebär att varje applikation av en funktor till samma struktur genererar nya typdefinitioner, d.v.s. två typer med samma namn och identiska i struktur, tillhörande olika strukturer, är inte lika.

OCaml använder applikativa funktorer, vilket innebär att applicering av en funktor på bevisligen lika argument automatiskt genererar samma resultat. Detta minskar behovet av en samanvändningsspecifikation och är särskilt användbart när det handlar om funktioner av högre ordning. Från och med version 4 lägger OCaml till möjligheten att göra funktorer föräldraskap.

Tillägg och dialekter

Funktioner av högre ordning

Funktionen tar emot en struktur specificerad av signaturen som indata. För att passera flera strukturer är det nödvändigt att bygga en extra omslagsstruktur som inkluderar dessa strukturer och beskriva motsvarande signatur. Definitionen av Standard ML-språket för enkelhetens skull ger syntaktisk socker - flera parametrar kan skickas som en tupel , och kompilatorn bygger automatiskt den omslutande strukturen och dess signatur. Emellertid tillhandahåller core ML funktioner av högre ordning , och att följa analogin på modulnivå med dem innebär att man introducerar en curry form av funktorer. Faktum är att det enda som behöver implementeras i språket för att tillhandahålla denna förmåga är stöd för att beskriva funktioner i signaturer [31] [32] . Detta är inte en grundläggande innovation (till skillnad från förstklassiga moduler ) - det finns inget som curry -funktioner skulle tillåta, men klassiska första ordningens sådana skulle inte - dock förenklar deras tillgänglighet avsevärt implementeringen (och därför läsbarheten ) av komplexa komponenthierarkier på flera nivåer [32] .

Ett slående exempel som visar bekvämligheten med att använda högre ordningsfunktioner är implementeringen av fullfjädrade monadiska kombinatorer .

Potentialen för att implementera högre ordningsfunktioner noterades redan i kommentarerna [31] till SML'90-definitionen [20] . Många Standard ML -kompilatorer tillhandahåller viss implementering av högre ordningens funktorer som en experimentell förlängning [32] . Ocaml implementerar alla typer av moduler på ett syntaktiskt enhetligt sätt, så att använda högre ordningsfunktioner är mest naturligt.

Notera - i den ryskspråkiga litteraturen finns [33] förvirring mellan " moduler av högre ordning " och " förstklassiga moduler " , vilket är ett semantiskt fel.

Objektorienterade funktioner

Fullständigt stöd för objektorienterad programmering enligt Abadi och Cardelli (se Objektorienterad programmering#Klassificering av undertyper av OOP ) innebär stöd samtidigt:

  • subtypningsförhållanden _
  • objekt
  • objekttyper
  • klasser (objektgeneratorer)

Allt detta har tillhandahållits av Ocaml i många år . Dessutom sträcker sig parametrisk polymorfism även till dessa egenskaper , vilket gör språket ännu mer uttrycksfullt. Naturligtvis har modulspråket i OCaml förbättrats så att objekt och klasser kan inkluderas i moduler.

Dessa anläggningar (eventuellt utvidgade till högre ordningstyper - se subtyping av högre ordning ) kommer att bli en del av efterföljaren ML .

Första klass moduler

Problem

En svaghet med det ursprungliga modulspråket är att det inte är stängt för kärnspråket: bastyper och värden kan vara komponenter i moduler, men moduler kan inte vara komponenter av bastyper och värden. I SML gjordes denna uppdelning av språket i två lager avsiktligt, eftersom det avsevärt förenklade mekanismen för kontroll av typkonsistens [31] . Detta gör det dock omöjligt att dynamiskt länka moduler, vilket innebär att följande uttryck är ogiltigt:

struktur Karta = om maxElems < 100 då BinTreeMap annars HashTableMap (* inte tillåtet i klassisk ML! *)

Ett sådant förbud är en skam för ett sådant uttrycksfullt modulsystem, eftersom det skulle vara helt normalt för alla objektorienterade språk [34] .

Faktum är att ML-modulens språk inte behöver vara statiskt [35] (se avsnittet om lågnivårepresentation ). Problemet ligger främst i den statiska typkontrollen som är MLs natur . Stöd i ML för förstklassiga moduler i sig är inte ett problem för ett första ordningens modulspråk (som inte innehåller funktorer), men det är kombinationen av förstklassiga moduler med högre ordningens moduler som tar språket "till en annan verklighet" [36] , dvs. öppnar enorma möjligheter, men komplicerar avsevärt både mekanismerna för att härleda och kontrollera överensstämmelsen hos språktyperna [37] och dess fullprogramoptimering . Idén med förstklassiga moduler begravdes i många år av Harper och Lilybridge , genom att konstruera en idealiserad version av det förstklassiga modulspråket med hjälp av teorin om beroende typer och bevisa att typkonsistenskontroll för denna modell är obestämbar [9] [38] . Men med tiden började alternativa modeller dyka upp med andra motiveringar.

Paket

I slutet av 1900-talet föreslog Claudio Russo [39] [40] det enklaste sättet att göra moduler förstklassiga : att komplettera listan över primitiva typer av språkets kärna med typen " paket " ( engelsk  paket ) , som är ett par структура : сигнатура, och listan över kärnuttryck med packnings- och uppackningsoperationer. Med andra ord, bara kärnan i språket förändras, och språket i modulerna förblir oförändrat [41] .

Packning av strukturer i paket och efterföljande uppackning gör att du dynamiskt kan binda olika strukturer till identifierare (inklusive de som beräknas med hjälp av funktorer). Det enklaste exemplet [42] :

struktur Karta = packa upp ( om maxElems < 100 packa sedan BinTreeMap : MAP else pack HashTableMap : MAP ) : MAP

Vid uppackning av ett paket kan strukturen signeras med en annan signatur, inklusive den sämre signaturen .

Den explicita närvaron av signaturen i paketet tar bort problemet med typinferens och matchning under dynamisk uppackning av strukturen. Detta motbevisar den tidiga Harper-Mitchell-tesen om omöjligheten att höja strukturer i ML till förstklassiga nivåer utan att offra separationen av kompilerings- och körningsfaserna och avgörbarheten av typkonsistenskontrollsystemet [41] eftersom istället för första- ordningsberoende typer används en förlängning av teorin om existentiella typer som motivering andra ordningens Mitchell-Plotkin [43] .

I detta formulär implementeras förstklassiga moduler i Alice och i Ocaml , från och med den 4:e versionen.

1ML

Inspirerad av F-konverteringen Rossberg in modulboxning-unboxing djupare i språkets semantik, vilket resulterar i ett monolitiskt språk där funktorer, funktioner och till och med typkonstruktörer verkligen är samma primitiva konstruktion, och ingen skillnad är gjorda mellan poster , tupler och strukturer - den interna representationen av språket är ett platt System F ω . Detta gav en hel mängd positiva resultat [44] :

  • att bevisa språkets tillförlitlighet blir mycket enklare än traditionellt för modulspråket (användningen av teorin om beroende typer krävs inte );
  • stöd ges för "materialiserade" ( eng.  reified ) typer i kärnan av språket, vilket ger språket uttryckskraft på nivån för system med beroende typer (och återigen inte kräver deras närvaro i metateorin);
  • språket som helhet visar sig vara både mer uttrycksfullt (låter dig beskriva komplexa system mer rymligt och exakt) och enklare (mer minimalistisk och mer enhetlig i sin sammansättning).

Språket kallades " 1ML ", vilket återspeglar både stödet för verkligt förstklassiga moduler och föreningen av primitiver och moduler på ett enda språk (ej uppdelat i två lager) [44] .

Beslutet baserades på idén från Harper-Mitchell att dela upp typer i "små" och "stora". Rossberg tillämpade denna distinktion på regeln för inkludering av typkonsistens (underliggande struktur-till-signatur-matchning), vilket gjorde den lösbar .

Förmodligen kan vidareutveckling av 1ML också ge tillräcklig uttrycksförmåga för att stödja många intressanta modeller, vars implementering tidigare ansågs vara svår: typklasser , applikativa funktorer , rekursiva moduler etc. I synnerhet introduktionen av inline polymorfism i 1ML kommer förmodligen omedelbart att tillåta att uttrycka subtyping i bredd , vilket kommer att hålla metateorin enkel samtidigt som dess kapacitet utökas avsevärt. [45]

MixML

MixML [10] är ett modulspråk byggt genom att kombinera McQueens klassiska ML-modulspråk och Bracha & Cooks formalisering av mix - ins- modellen .  Författarna till MixML är Rossberg och Dreyer.

Grundidén med MixML är enkel: strukturer och signaturer kombineras till ett enda koncept av en modul, som kombinerar definitioner och specifikationer, både transparenta och abstrakta.

Detta gör det möjligt att definiera godtyckliga beroendegrafer i program, inklusive cykliska. Detta gör att du i synnerhet kan bygga in funktorer, inte bara direkt parameterisering (utgångens beroende av ingången), utan också rekursiv (ingångens beroende av utgången), samtidigt som stödet för separat kompilering bibehålls (till skillnad från många privata modeller som utökar ML-modulens språk med stöd för rekursion).

MixML implementerar en enda enhetlig notation för traditionellt parade semantiska modeller (för strukturer och signaturer separat) och ett stort antal separata mekanismer för det klassiska språket för ML-moduler, såsom:

  • arv (inkluderande) av underskrifter
  • samanvändningsspecifikationer
  • två former av signatursignering (transparent och mörk)
  • funktorapplikationer

Övrigt

Följande tillägg finns också på olika modeller:

  • lokala moduler
  • många alternativ för det rekursiva systemet av moduler som låter dig bilda cykliska beroendegrafer, varav det mest uttrycksfulla är MixML -systemet (de flesta av de andra ger inte möjlighet till separat kompilering)
  • utökat modulkapslingsstöd
  • generaliserad notation för öppningsstrukturer
  • olika alternativ för att begränsa samanvändning
  • kapslade signaturer, inklusive abstrakta
  • deklarationer av infix-operatorer som anger associativitet och prioritet inom signaturer och kräver en exakt matchning

Språkekosystem

Implementationer och dialekter

Alice

Alice - språket är en förlängning av Standard ML , inklusive många av idéerna från det efterföljande ML- projektet , såväl som avancerade konkurrenskraftiga programmeringsverktyg för att utveckla distribuerade applikationer, stöd för stark dynamisk typning och en begränsningslösare . Designad av Andreas Rossberg.

Språket för moduler i Alice utökas till notationen av komponenter ( eng.  komponenter ), som implementerar förstklassiga moduler i form av Russo paket och dessutom stödjer dynamisk typning (men enligt samma regler för statisk semantik) och lat laddning (dvs framtida strukturer stöds och framtida signaturer - se framtida samtal ) [46] [47] . typavledning respekteras i Alice , och samanvändningsspecifikationen bör användas vid behov . Ett illustrativt exempel på den praktiska användbarheten av paket kommer med Alice : ett dataserialiseringsbibliotek som tillåter trådar att utbyta dynamiska typer och data .

Dessutom tillhandahåller Alice syntaktisk socker - möjligheten att fritt använda parenteser i modulspråkuttryck, inklusive istället för traditionella "parenteser" struct...endoch sig...end:

val p = pack ( val x = längd ) : ( val x : 'a list -> int ) (* val p : package = package{|...|} *) OKaml

I Ocaml är syntaxen för modulspråket enhetlig:

modultyp S = ( * signatur *) sig ... modul M : T (* kapslad struktur *) slut modul X : S = (* struct *) struct ... end modul F ( X : S ) = (* parametriserad struktur (funktion) *) struktur ... slut modul G ( X : S ) ( Y : T ) = (* curried parameterized struct (högre ordningens funktion) *) struct ... end

Det finns dock ett antal skillnader i semantik [48] .

Från och med version 4 stöder Ocaml förstklassiga -moduler i en notation som liknar Alices paket . Syntaxen är fortfarande homogen, det vill säga den ser omöjlig att skilja från kapslade strukturer i signaturer.

Sedan starten har Ocaml utökat modulspråket med klasser och objekt .

De viktigaste skillnaderna mellan Standard ML och Ocaml visas i typekvivalenssemantiken (se avsnittet om typekvivalens ).

Modulhantering

För att länka gigantiska ML-program kan traditionella länkar för de flesta språk , som make , i princip användas . SML-modulspråket är dock mycket kraftfullare än modulariseringsverktygen för andra språk [2] , och fabrikatet stöder inte dess fördelar, och ännu mer är det inte lämpligt för global analys av kontrollflödet av program [49] . Därför erbjuder olika kompilatorer sina egna modulhanteringssystem: Compilation Manager (CM) i SML/NJ och MLBasis System (MLB) i MLton . SML.NET [50] har ett inbyggt beroendespårningssystem. MLton innehåller också en filkonverterare från .cm till .mlb .

De flesta implementeringar använder separat kompilering, vilket resulterar i snabba kompileringstider. För att stödja separat kompilering i REPL- läge används en funktion usesom kompilerar den angivna filen och importerar definitionerna. Vissa kompilatorer (som MLton ) stöder inte REPL och implementerar därför inte stöd för use. Andra (till exempel Alice ) implementerar tvärtom ytterligare funktioner för dynamisk kompilering och laddning av moduler under programexekveringen. Poly/ML [51] tillhandahåller en funktion PolyML.ifunctorsom låter dig felsöka en funktionsimplementering interaktivt bit för bit.

Programexempel

Trots sin enkelhet är modulspråket anmärkningsvärt flexibelt och ger en hög nivå av kodåteranvändning , vilket illustreras av följande exempel.

Hantera antalet siffror

Traditionella datatyper , såsom heltal ( intoch word), reella ( real), tecken ( charoch widechar), sträng ( stringoch widestring), arrayer ( vectoroch array) och andra, implementeras i ML-dialekter, inte i form av primitiva typer och inbyggda operatorer över dem, som på de flesta språk, men i form av abstrakta datatyper och motsvarande funktioner som ingår i signaturerna respektive , INTEGER, WORD, REAL, CHARoch STRINGså vidare, tillhandahållna i form av standardbibliotek. Konkreta språkimplementeringar kan ge mycket effektiva representationer av dessa abstrakta typer (till exempel representerar MLton arrayer och strängar på samma sätt som C - språket gör ).

Till exempel:

signatur INTEGER = sig eqtype int val toLarge : int -> LargeInt . int val fromLarge : LargeInt . int -> int val toInt : int -> Int . int val fromInt : Int . int -> int val precision : Int . int option val minInt : int option val maxInt : int option 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 compare : ( 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 tecken : int -> Int . int val sameSign : ( int * int ) -> bool val fmt : StringCvt . radix -> int -> string val toString : int -> string val fromString : string -> int option val scan : StringCvt . radix -> ( char , ' a ) StringCvt . reader -> 'a -> ( int * 'a ) alternativ slut

Strukturerna , , , och många andra INTEGERkan jämföras med signaturen . På samma sätt kan strukturer / och / (och möjligen andra) matchas med signaturer / och för varje variant kommer funktionorerna att generera en lämplig I/O-stack ( , ). Int8Int16Int32Int64IntInfCHARSTRINGCharStringWideCharWideStringStreamIOTextIO

Samtidigt döljer vissa strukturer den traditionella maskinrepresentationen under den abstrakta definitionen (till exempel , Int32) Int64, andra - bitfält (till exempel Int1), och strukturen IntInfimplementerar lång aritmetik . Samtidigt kan bibliotek intensivt gå igenom många-till-många- relationer : SML Basis - specifikationen definierar en uppsättning obligatoriska och valfria moduler som är byggda ovanpå implementering av "primitiva" typer: monomorfa arrayer, deras icke-kopierande skivor, och så vidare . Även typerna "sträng" ( ) och "understräng" ( ) definieras i SML-basspecifikationen som och ( eller och för ). För att använda samma algoritmer med antal olika kapacitet räcker det alltså att explicit skicka motsvarande struktur till -funktorn (öppning kommer inte att ändra redan beräknade strukturer). stringsubstringChar.char vectorChar.char VectorSlice.sliceWideChar.char vectorWideChar.char VectorSlice.sliceWideString

Olika kompilatorer tillhandahåller olika uppsättningar av implementerade strukturer. MLton tillhandahåller det rikaste sortimentet : från Int1till Int32inklusive och Int64, samma uppsättning för Word(osignerade heltal), såväl som IntInf(implementerat av GNU Multi-Precision Library ) och många ytterligare sådana, som Int32Array, PackWord32Big, PackWord32Littleoch mer.

I de flesta implementeringar, som standard, på översta nivån (i den globala miljön), är en struktur Int32(eller Int64) öppen, det vill säga att använda en typ intoch en operation +innebär som standard att använda en typ Int32.intoch en operation Int32.+(eller, respektive, Int64.intoch Int64.+). Dessutom tillhandahålls identifierare Intoch LargeInt, som som standard är bundna till vissa strukturer (till exempel LargeIntvanligtvis lika med IntInf). Olika kompilatorer, beroende på deras orientering, kan använda olika bindningar i den globala miljön som standard, och sådan subtilitet kan påverka portabiliteten av program mellan kompilatorer. Till exempel Int.maxIntinnehåller en konstant värdet av största möjliga heltal, insvept i en valfri typ , och måste hämtas antingen genom mönstermatchning eller genom ett funktionsanrop valOf. För ändliga dimensionstyper är värdet , och båda extraktionsmetoderna är likvärdiga. Men lika , så att få tillgång till innehållet direkt via kommer att leda till ett undantag . Som standard är den öppen i Poly/ML- kompilatorn [51] eftersom den är fokuserad på problem med nummerkrossar . IntN.maxIntSOME(m)IntInf.maxIntNONEvalOf OptionIntInf

Abstrakt uppsättningar

OKaml biblioteken inkluderar en modul som tillhandahåller en funktor . Med den kan du enkelt bygga en uppsättning baserat på en given elementtyp: SetMake

modul Int_set = Set . Gör ( struct typ t = int låt jämföra = jämför slut )

Den genererade heltalsuppsättningsmodulen har följande kompilator - härledd signatur:

modul Int_set : sig typ elt = int typ t val tomt : t val är_tom : t -> bool val mem : elt -> t -> bool val add : elt -> t -> t val singleton : elt -> t val ta bort : elt -> t -> t val union : t -> t -> t val inter : t -> t -> t val diff : t -> t -> t val jämför : t -> t -> int val lika : t -> t -> bool val delmängd : t -> t -> bool val iter : ( elt -> enhet ) -> t -> enhet val fold : ( elt -> ' a -> ' a ) -> t -> ' a -> ' a val for_all : ( elt -> bool ) -> t -> bool val existerar : ( elt -> bool ) -> t -> bool val filter : ( elt -> bool ) -> t -> t val partition : ( elt -> bool ) -> t -> t * t val kardinal : t -> int val element : t -> elt lista val min_elt : t -> elt val max_elt : t -> elt val välj : t -> elt val split : elt -> t -> t * bool * t val hitta : elt -> t -> elt slut

Liknande funktionalitet ingår i SML/NJ- kompilatorbiblioteken ( ListSetFn). SML Basis tillhandahåller endast elementära verktyg.

Huvudsyftet med att använda en beroende modul istället för en enkel struktur här är att jämförelsefunktionen specificeras en gång , och alla funktioner på en viss typad uppsättning använder samma jämförelsefunktion för typen av element i denna uppsättning, så att programmeraren är därmed skyddad från sina egna misstag. Abstrakta uppsättningar skulle kunna implementeras genom att föra varje funktion över uppsättningen en jämförelsefunktion varje gång (som görs t.ex. i en standardfunktion för C- qsort språket - se parametrisk polymorfism i C och C ++ ), men detta skulle inte ökar bara komplexiteten i att arbeta med set , men skulle också medföra risken att förvirra den erforderliga jämförelsefunktionen genom att introducera ett svårupptäckt fel i programmet (se kodduplicering ).

Tyvärr [24] historiskt sett har OCaml antagit en signatur för jämförelsefunktionen som indikerar returvärdet för en tvåvägs ( boolesk ) typ (och konventioner av detta slag bör observeras för att kunna använda biblioteksmoduler i stor utsträckning) . Kraftfullare är SML Basis -lösningen (liksom Haskell Prelude ) baserad på en trevägstyp:

datatyp order = MINDRE | LIKA | STÖRRE val compare : int * int -> order

Strukturell testning

Med rapid prototyping är det ofta nödvändigt att testa systemet i delar eller simulera beteendet på ett förenklat sätt (implementera de så kallade "stubbarna"). Funktioner hanterar denna uppgift på ett elegant sätt.

Låt oss till exempel säga att det finns tre olika implementeringar av någon datastruktur , säg en kö [52] :

signatur KÖ = sig typ 'a t undantag E val tomt : '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 struktur Queue1 :> QUEUE = struktur ... slut struktur Queue2 :> QUEUE = struktur ... slut struktur Queue3 :> QUEUE = struktur ... slut

På många språk, i brist på abstraktion , skulle det vara nödvändigt att skapa separata kopiera-klistra- program för att jämföra dem . Funktioner, å andra sidan, låter dig abstrahera testet från implementeringen och iterera över dem i ett enda program:

functor TestQueue ( Q : QUEUE ) = struct fun from List I = foldl ( fn ( x , q ) => Q . enq ( q , x )) Q . tom I fun toList q = om Q . null q sedan [] annars Q . hd q :: toList ( Q . deq q ) slut val ns = upp till ( 1 , 10000 ) (* val ns = [1, 2, 3, 4, ...] : int lista *) struktur TQ1 = TestQueue ( Queue1 ) val q1 = TQ1 . fromList ns val l1 = TQ1 . toList q1 l1 = ns (* true : bool *) ... struktur TQ2 = TestQueue ( Queue2 ) struktur TQ3 = TestQueue ( Queue3 ) ...

Sedan kan du välja mellan bredd -första sökning och djup -första sökning för varje implementering, allt i ett enda program:

functor BreadthFirst ( Q : QUEUE ) = struktur ... slut functor DepthFirst ( Q : QUEUE ) = struct ... end struktur BF_Q1 = BreadthFirst ( Queue1 ) struktur BF_Q2 = BreadthFirst ( Queue2 ) struktur BF_Q3 = BreadthFirst ( Queue3 ) struktur DF_Q1 = DeepFirst ( Queue1 ) struktur DF_Q2 = DeepthFirst ( Queue2 ) struktur DF_Q3 = DeepthFirst ( Queue3 ) ...

I framtiden behöver inte "extra" implementeringar tas bort. Dessutom kommer helt optimerande kompilatorer som MLton att ta bort dem på egen hand - se borttagning av död kod .

Denna metod kan också användas för att mäta effektivitet, men i praktiken är det mycket bekvämare (och mer tillförlitligt) att mäta det med en profilerare inbyggd i kompilatorn.

Den globala typsäkerheten för beroenden mellan komponenter som modulspråket tillhandahåller är synlig i exemplet med ett felaktigt försök att använda en funktion:

struktur Fel = BreadthFirst ( Lista ); (* > Fel: unmatched typ spec: t > Fel: unmatched exception spec: E > Fel: unmatched val spec: tom > Fel: unmatched val spec: enq > Fel: unmatched val spec: deq *)

Monader och typklasser

Haskell , som är en ättling till ML , stöder inte ML -modulspråket. Istället ger den stöd för storskalig programmering (utöver det triviala systemet av moduler som liknar de som används på de flesta språk) genom monader och typklasser . De förra uttrycker abstrakt beteende, inklusive modellering av föränderligt tillstånd i termer av referenstransparens ; de senare fungerar som ett sätt att kontrollera kvantifieringen av typvariabler genom att implementera ad-hoc polymorfism . ML-modulspråket tillåter att båda idiom [53] [11] implementeras .

En typklass är inget annat än ett gränssnitt som beskriver en uppsättning operationer vars typ ges av en oberoende abstrakt typvariabel som kallas en klassparameter. Därför kommer en naturlig representation av en klass i termer av modulspråket att vara en signatur som, förutom den nödvändiga uppsättningen av operationer, även inkluderar en typspecifikation (som representerar en klassparameter) [11] :

signatur EQ = sig typ t val eq : t * t -> bool end

Monaden implementeras av signaturen:

signatur MONAD = sig typ 'a monad val ret : 'a -> 'a monad val bnd : 'a monad -> ( 'a -> 'b monad ) -> 'b monad slut

Exempel på dess användning:

struktur Alternativ : MONAD = struct typ 'a monad = 'a option fun ret x = SOME x fun bnd ( SOME x ) k = k x | bnd INGEN k = INGEN slut signatur REF = sig typ 'a ref val ref : 'a -> 'a ref IO . monad val ! : 'a ref -> 'en IO . monad val : = : 'a ref -> 'a -> enhet IO . monaden slut

Fullfjädrade monadiska kombinatorer är särskilt bekväma att implementera med hjälp av högre ordningsfunktioner [32] [53] :

(*Första beställning*) signatur MONOID = sig typ t val e : t val plus : t * t -> t end functor Prod ( M : MONOID ) ( N : MONOID ) = strukturtyp t = M. _ _ t * N . t val e = ( M . e , N . e ) fun plus (( x1 , y1 ), ( x2 , y2 )) = ( M . plus ( x1 , x2 ), N . plus ( y1 , y2 )) slut funktor Square ( M : MONOID ) : MONOID = Prod M M struktur Plan = Kvadrat ( typ t = verklig val e = 0,0 val plus = verklig . + ) val x = Plan . plus ( Plan . e , ( 7.4 , 5.4 )) (*högre ordning*) signatur PROD = MONOID -> MONOID -> MONOID funktor Square ( M : MONOID ) ( Prod : PROD ) : MONOID = Prod M M struktur T = Square Plane Prod val x = T . plus ( T.e , T.e ) _ _ _ _ (*Öppenligt*) signatur PROD' = fct M : MONOID -> fct N : MONOID -> MONOID där typ t = M . t * N . t functor Square' ( M : MONOID ) ( Prod : PROD' ) : MONOID = Prod M M struktur T' = Square' Plane Prod val x = T' . plus ( T' . e , (( 7.4 , 5.4 ), ( 3.0 , 1.7 )))

Värden indexerade efter typer

Värden indexerade efter typer är ett idiom som är gemensamt för alla tidiga språk i ML -familjen , designat för att implementera ad-hoc polymorfism ( funktionsöverbelastning ) genom parametrisk polymorfism [54] . Typklasser , som först introducerades i Haskell , är stöd för typindexerade värden på språknivå (och är som sådana enkelt implementerade i modulspråket ).

I sin enklaste form demonstreras detta idiom i följande OCaml- exempel [55] :

modultyp Arith = sig typ t val ( +) : t -> t -> t val neg : t -> t val noll : t slut modulen Build_type ( M : Arith ) = struct låt typ x = { Typ . plus = M . (+); neg = M. _ (-); noll = M . noll ; } slut låt int = låt modul Z = Bygg_typ ( Int ) i Z . typ låt int64 = låt modul Z = Bygg_typ ( Int64 ) i Z. _ typ låt int32 = låt modul Z = Bygg_typ ( Int32 ) i Z. _ typ let native = let modul Z = Build_type ( Native_int ) i Z. _ typ let float = låt modul Z = Build_type ( Flytande ) i Z. _ typ låt komplex = låt modul Z = Byggtyp ( komplex ) i Z. _ typ

Objektmodell

Med hjälp av modulspråket kan du bygga en enkel objektmodell med dynamisk sändning. Detta exempel är intressant med tanke på att SML inte tillhandahåller några objektorienterade programmeringsfaciliteter och inte stöder undertyper .

Den enklaste dynamiskt sändbara objektmodellen kan enkelt byggas i SML genom . En inmatningstyp som inkluderar funktionsvärden spelar rollen som en abstrakt klass som definierar metodsignaturen. Att dölja det interna tillståndet och de privata metoderna för dessa objekt tillhandahålls av ML :s lexikala räckvidd ; sålunda kan stängningar (ML-funktioner) spela rollen som konstruktörer av objekt i denna klass. En sådan implementering tillåter inte att bygga komplexa arvshierarkier på flera nivåer (detta kräver implementering av subtyper, vilket görs genom en komplex implementering av värden indexerade efter typer och för vilka det finns flera olika metoder), men i praktiken är det ganska tillräckligt för de flesta uppgifter med bra design [12] . Härledning av en sådan objektmodell till modulnivå betraktas nedan.

De enklaste dataströmmarna används som bas:

signatur ABSTRACT_STREAM = sig typ 'a t val isEmpty : 'a t -> bool val push : 'a * 'a t -> 'a t val pop : 'a t -> ( 'a * 'a t ) alternativ slut signatur STREAM = sig include ABSTRACT_STREAM val empty : 'a t end struktur Stack :> STREAM = struct typ 'a t = 'en lista val tom = [] val isEmpty = null val push = op :: val pop = Lista . getItem slut struktur Kö :> STREAM = struct datatype 'a t = T av 'en lista * 'en lista val tom = T ([], []) val isEmpty = fn T ([], _) => sant | _ => false val normalize = fn ([], ys ) => ( rev ys , []) | q => q rolig push ( y , T ( xs , ys )) = T ( normalisera ( xs , y::ys )) val pop = fn ( T ( x::xs , ys )) => NÅGRA ( x , T ( normalisera ( xs , ys ))) | _ => INGET slut

Med hjälp av funktorer kan du implementera generaliserade algoritmer som manipulerar dataströmmar för en okänd intern enhet och syfte:

functor StreamAlgs ( ST : ABSTRACT_STREAM ) = struktur öppen ST kul pushAlla ( xs , d ) = vikl push d xs roliga popAlla d = låt roliga lp ( xs , INGEN ) = varv xs | lp ( xs , SOME ( x , d )) = lp ( x::xs , pop d ) i lp ([], pop d ) slut fun cp ( från , till ) = pushAll ( popAll från , till ) slut

Att instansiera denna funktion med strukturer som är jämförbara med signatur ABSTRACT_STREAMger funktioner som manipulerar motsvarande dataströmmar:

struktur S = StreamAlgs ( Stack ) struktur Q = StreamAlgs ( Queue ) S. _ popAll ( S . pushAll ([ 1 , 2 , 3 , 4 ], Stack . empty )) (* resultat: [4,3,2,1] *) F. _ popAll ( Q . pushAll ([ 1 , 2 , 3 , 4 ], Queue . empty )) (* resultat: [1,2,3,4] *)

Det bör noteras att funktorn StreamAlgstar en signaturparameter ABSTRACT_STREAMoch strukturerna Stackoch Queuesignerades med signaturen som STREAMberikar signaturen . Detta innebär en subtilitet: vid utveckling är det önskvärt att följa de konventioner som antagits i standardbiblioteket för en viss dialekt för att i större utsträckning kunna använda den befintliga utvecklingen, särskilt standardfunktioner (det finns inte så många av dem i SML Basis' 2004, men i tilläggen av vissa kompilatorer och i OCaml finns mycket intressanta exempel). ABSTRACT_STREAM

Härledda strukturer innehåller typdefinitionen ST.tfrån funktorparametern, men de är olika typer: varje typdefinition i ML genererar en ny typ. Därför resulterar ett försök att blanda ihop dem i ett typkonsistensfel . Till exempel kommer följande rad att avvisas av kompilatorn:

val q = Q . push ( 1 , Stack . tom )

Trådklassgränssnittet definieras bekvämt som . Av typsäkerhetsskäl är det att föredra att inte använda ett typalias, utan en konstruktorfunktion som mappar en sådan post till ett klassobjekt:

structure Stream = struct datatype 'a t = I av { 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 () end

Modulen Streamimplementerar faktiskt signaturen ABSTRACT_STREAM( ), men explicit signering skjuts upp till senare.

För att förvandla en trådmodul till en trådklass måste du lägga till två namngivna konstruktorer till den , vilket kan göras med en funktor och öppningskonstruktionen :

functor StreamClass ( D : STREAM ) : STREAM = struktur öppen Stream kul gör d = I { isEmpty = fn () => D . isEmpty d , push = fn x => make ( D . push ( x , d )), pop = fn () => case D . pop d av INGEN => INGEN | SOME ( x , d ) => SOME ( x , gör d ) } val tom = I { isEmpty = fn () => true , push = fn x => make ( D . push ( x , D . tom )), pop = fn () => INGEN } slut

Strukturen som genereras av funktorn StreamClassinkluderar alla komponenter i strukturen Stream(inklusive konstruktorn I ), men de är inte synliga från utsidan, eftersom resultatet av funktorn signeras av signaturen STREAM.

Slutligen kan du försegla modulen Stream:

struktur Ström : ABSTRACT_STREAM = Ström

Detta är inte nödvändigt ur typsäkerhetssynpunkt , eftersom modulen Streaminte tillåter brytande inkapsling som den var. Döljande av konstruktorer I ger dock en garanti för att endast funktorn StreamClasskan användas för att skapa underklasser ABSTRACT_STREAM.

Uppenbara användningsfall:

struktur StackClass = StreamClass ( Stack ) struktur QueueClass = StreamClass ( Queue )

Men det är inte allt. Eftersom den ovan definierade funktorn StreamAlgstar en struktur av typen som input ABSTRACT_STREAM, kan den instansieras av en struktur Streamsom implementerar den abstrakta strömklassen:

struktur D = StreamAlgs ( Stream )

En härledd modul D, som en modul Stream, fungerar med vilken klass som helst som ärver från ABSTRACT_STREAM, vilket kan ses som dynamisk sändning:

D. _ popAll ( D . pushAll ([ 1 , 2 , 3 , 4 ], StackClass . empty )) (* resultat: [4,3,2,1] *) D. _ popAll ( D . pushAll ([ 1 , 2 , 3 , 4 ], QueueClass . empty )) (* resultat: [1,2,3,4] *)

Det är intressant att notera att varken Stream, eller Dinnehåller inte bara mutable state , utan också några konstanter - bara typer och funktioner - men när den skickas genom parametermekanismen används den abstrakta klassen faktiskt här som ett förstaklassvärde , och inte bara en virtuell enhet, som i många objektorienterade språk.

Om språket

Lågnivårepresentation och effektivitet

Traditionellt representeras strukturer i kompilatorn med hjälp av poster , och funktorer representeras av funktioner över sådana poster [35] . Det finns dock alternativa interna representationer, som Harper-Stone semantik och 1ML .

Att använda funktorer som ett sätt att bryta ner ett stort projekt innebär att sakta ner åtkomsten till de slutliga komponenterna i program som beräknas genom dem, och för varje nivå av kapsling multipliceras förlusterna, precis som när man använder vanliga funktioner istället för omedelbara värden. Fullständigt optimerande kompilatorer ( MLton , MLKit [56] , SML.NET [50] ) utökar modulramverket och bygger de slutgiltiga definitionerna av funktionskomponenter med hänsyn till egenskaperna hos de strukturer som faktiskt skickas in, vilket eliminerar prestationsstraffet. MLKit använder också modulexpansion för att sluta sig till regioner, vilket gör att språket kan användas för att utveckla realtidsapplikationer . I det här fallet kan avslöjandet av ramverket för moduler utföras med olika strategier: till exempel utför MLton " programavfunktion " och MLKit utför " statisk tolkning av modulspråket ". Det finns en implementering av en valfri defunctorizer för OCaml [57] .

Skäl för semantik

Under många år ansågs ML-modulspråket på typteoretisk nivå som en tillämpning av teorin om beroende typer , och detta gjorde att språket kunde slutföras och dess egenskaper noggrant undersökas. I verkligheten är moduler (även i en förstklassig roll) inte " verkligt beroende ": signaturen för en modul kan bero på de typer som finns i en annan modul, men inte på värdena som finns i den [3 ] .

Detaljer Mitchell-Plotkin korrespondens Starka McQueen summor

[58]

Genomskinliga Harper-Lilybridge summor

Robert Harper och Mark Lillibridge konstruerade [9] [59] den genomskinliga summakalkylen för att formellt motivera språket i högre ordningens förstklassiga moduler .  Denna kalkyl används i Harper-Stone semantiken . Dessutom har dess delar blivit en del av den reviderade SML-definitionen (SML'97).

Semantik av Harper-Stone

Harper-Stone semantik ( HS semantik för kort ) är en tolkning av SML i ett maskinskrivet ramverk .  Det senare inkluderar ett modulsystem baserat på Harper-Lilybridge genomskinliga summor (se ovan). Tolkningen är teoretiskt elegant, men upprätthåller det felaktiga intrycket att ML-moduler är svåra att implementera: den använder singletontyper , beroende typer och ett komplext system av effekter [3] .

Rossberg-Rousseau-Dreyer F-transform

Andreas Rossberg, Claudio Russo och Derek Dreyer har tillsammans visat att den populära uppfattningen om en orimligt hög ingångströskel för ett modulspråk är falsk. De konstruerade en omvandling av modulernas språk till ett platt System F ω ( lambdakalkyl av andra ordningen), vilket visade att själva modulernas språk egentligen bara är ett specialfall ( syntaktisk socker ) av att använda System F ω . I denna mening är den största fördelen med att använda moduler jämfört med att arbeta direkt i System F ω en betydande grad av automatisering av många komplexa åtgärder (signaturmatchning med hänsyn till anrikning, implicit packning/uppackning av existentiella ämnen , etc.).

" F-ing semantik " ( F-ing semantik ), eller F-transformation, stöder inklusive högre ordningsfunktioner och förstklassiga moduler i form av Rousseau-paket. Beviset på tillförlitligheten av F-transformen har mekaniserats med metoden "lokalt namnlös" ( Lokalt namnlös ) i Coq . Författarna sammanfattade det utförda arbetet som extremt smärtsamt och rekommenderar inte att man använder denna metod i framtiden [3] . Resultaten som uppnåddes inspirerade Rossberg ytterligare att skapa 1ML .

Kritik och jämförelse med alternativ

ML-modulspråket är det mest utvecklade systemet av moduler i programmeringsspråk [2] och fortsätter att utvecklas. Det ger kontroll över namnrymdshierarkier (genom ) , finkorniga gränssnitt (genom signaturer ), abstraktion på klientsidan (genom funktorer ) och implementersida (genom typning ) [ 3 ] .

De flesta språk har inget som kan jämföras med funktioner [52] . Den närmaste analogen till funktorer är de senare C++-klassmallarna , men funktorer är mycket lättare att använda [60] eftersom C++-mallarna inte bara är typsäkra , de lider också av ett antal andra nackdelar [61] . Vissa språk tillhandahåller makroundersystem som tillåter automatisk kodgenerering och flexibel hantering av kompileringstidsberoenden ( Lisp , C ), men ofta är dessa makroundersystem ett icke verifierbart tillägg till huvudspråket, vilket tillåter godtycklig omskrivning av en programrad. by-line, vilket kan leda till många problem [62] . Först på 2000-talet utvecklades makro-undersystem som är typsäkra ( Template Haskell , Nemerle ), av vilka några är tillgängliga samtidigt med funktorer (MetaML [63] , MetaOCaml ).

Det fina med funktorer är att de kan kompileras och typkontrolleras även om det inte finns någon struktur i programmet som skulle kunna skickas till dem som en faktisk parameter [64] . Genom att göra så beskriver funktorer interaktion på gränssnittsnivå snarare än implementeringar , vilket gör det möjligt att bryta kompileringstidsberoenden. Detta sker vanligtvis på bekostnad av viss prestandaförsämring, men optimeringsmetoder med fullständiga program löser detta problem framgångsrikt .

Språket i moduler upplevs ofta som svårt att förstå, anledningen till detta ligger i den komplexa matematik som krävs för att motivera det. Simon Peyton-Jones liknade funktorer vid en Porsche -bil för deras " höga kraft men dåliga värde för pengarna " [65] . Förespråkare av ML håller inte med om denna synpunkt och hävdar att modulspråket inte är svårare att använda/implementera/förstå än Haskells typklasser eller Javas klasssystem med generika och jokertecken [ , och är egentligen en fråga om subjektiv preferens [3] .

Om kompilatorn upptäcker fel i moduldefinitioner kan utmatningsfelmeddelandena vara mycket långa, vilket i fallet med funktionorer, speciellt av högre ordning, kan orsaka särskilt besvär. Därför bör ett block med typdefinitioner och funktioner ovanför dem formateras som en modul först efter att det har utvecklats i delar (för vilket REPL- läge tillhandahålls i de flesta implementeringar ). Vissa implementeringar (t.ex. Poly/ML [51] ) tillhandahåller sina egna tillägg för att lösa detta problem. Andra (till exempel SML2c) tillåter tvärtom att endast program på modulnivå kompileras.

Historia, filosofi, terminologi

Tanken med modulspråket är att den storskaliga semantiken för program ska upprepa semantiken för kärn - ML ( eng.  Core ML ), det vill säga beroenden mellan stora programkomponenter formuleras som beroenden av en liten nivå. Följaktligen är strukturer "värden" på modulnivån ( värden på engelska  modulnivå ); Signaturer (även kallade " modultyper " eller " modultyper ") karakteriserar "typerna" av modulnivåvärden, medan funktorer karakteriserar "funktionerna" på modulnivån. Analogin är dock inte identisk: både innehållet i moduler och relationerna mellan moduler kan vara mer komplexa än i kärnan av språket. De mest betydande komplikationerna i denna mening är införandet av understrukturer i signaturer och begränsningen av samanvändning av [4] . I kommentarerna [31] på SML'90-definitionen noterades den potentiella implementeringen av funktioner av högre ordning (analogier med funktioner av högre ordning ), men deras implementeringar dök upp senare .

Modulspråket föreslogs ursprungligen av David MacQueen [66 ] .  I framtiden gav många forskare det viktigaste bidraget till den typteoretiska motiveringen och utvidgningen av modulspråket. Arbetet inkluderar formalisering av rekursiva , kapslade, lokala, högre ordning och förstklassiga moduler , såväl som upprepad revidering av deras motivering för att förenkla både själva modellen och dess stödjande metateori och bevisa dess pålitlighet. Utvecklingen av modulspråket skär sig nära utvecklingen av kärnan ML och präglas av dussintals verk av många forskare, men följande viktiga milstolpar kan särskiljas:

  • 1984 - McQueen - initial idé [66] .
  • 1990 - Milner, Harper, McQueen, Tofty - en modell skild från kärnan av språket som en del av definitionen, bevis på dess tillförlitlighet genom den så kallade generativa typförseglingen [20] .
  • 1994 - Appel, McQueen - separat sammanställning [6] .
  • 1995 - Leroy - förenkling av metateori till transparenta typer (ej genererande), applikativa funktorer [67] .
  • 1994 - Harper, Lilybridge - Typteoretisk grund med beroende typer [9] .
  • 1999-2000 - Rousseau - förenkling av metateori till andra ordningens, förstklassiga moduler i form av paket [39] [40] .
  • 2000 - Harper-Stone semantik .
  • 2010 - Rossberg, Rousseau, Dreyer - förenkling av metateori till ett platt System F , mekanisering av beviset på dess tillförlitlighet i Coq [3] .
  • 2015 - Rossberg - 1ML , en enda modell med språkets kärna [34] .

En annan dialekt av ML - Caml- språket - stödde ursprungligen modulspråket med ett antal skillnader . Därefter utvecklades det till Objective Caml- språket, som kompletterade modulspråket med ett objektorienterat programmeringsundersystem som organiskt utvecklade idéerna för modulspråket . OCaml fortsatte att utvecklas kontinuerligt, och i mitten av 2010-talet kompletterades dess modulspråk av ett antal experimentella funktioner. Enskilda implementeringar av SML stöder vissa av dessa funktioner som tillägg. Den viktigaste innovationen är förstklassiga moduler, som också stöds av Alice språket .

Applikation

På olika språk

Semantiken i modulspråket är helt oberoende av det faktum att ML är ett strikt språk – det kan också användas i lata språk [68] . Dessutom har privata implementeringar av modulspråket föreslagits ovanpå kärnorna i semantiskt olika språk (till exempel Prolog och Signal ).

Parametrisk tillväxt av språk

År 2000 föreslog Xavier Leroy (utvecklare av OCaml ) en implementering av en generaliserad generativ modell som låter dig bygga ML-modulspråket över kärnan av ett godtyckligt (i ett ganska brett spektrum) språk med sitt eget typsystem ( till exempel C ) [1] . Denna modell implementeras genom själva modulspråket - i form av en funktion , parametriserad av data om språkets kärna och en beskrivning av dess typkonsistenskontrollmekanism .

Moduler som grund för språkets kärna

Efter tre decennier av utveckling av modulspråket som ett tillägg till språkets kärna föreslog Andreas Rossberg (utvecklaren av Alice ) 2015 istället för den traditionella utbyggnaden av modulspråket ovanpå kärnspråk, att använda modulspråket som ett mellanspråk för att representera kärnspråkets konstruktioner. Detta gör moduler till verkligt förstklassiga värden (kräver inte förpackning i paket) - se 1ML .

Anteckningar

  1. ↑ 12 Leroy, "Modular Module System", 2000 .
  2. ↑ 1 2 3 Cardelli, "Typeful programmering", 1991 , 2. Typfulla språk, sid. 5.
  3. ↑ 1 2 3 4 5 6 7 8 Rossberg, Russo, Dreyer, "F-ing Modules", 2010 .
  4. ↑ 1 2 Harper, "Programming in SML", 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 till SML", 1986 , sid. femtio.
  8. ↑ Paulson, "ML for the Working Programmer", 1996 , 7.4 Den avsedda signaturen för köer, sid. 264.
  9. ↑ 1 2 3 4 Harper, Lillibridge, "Typteoretisk inställning till högre ordningsmoduler med delning", 1994 .
  10. ↑ 1 2 Dreyer, Rossberg, "MixML", 2008 .
  11. ↑ 1 2 3 Dreyer, Harper, "Modular Type Classes", 2007 .
  12. ↑ 1 2 Objektorienterad programmering i Standard ML
  13. ↑ Paulson, "ML för den arbetande programmeraren", 1996 , 2.22 Signaturer, sid. 62.
  14. ↑ Paulson, "ML för den arbetande programmeraren", 1996 , 2.19 Introduktion till moduler, sid. 59.
  15. ↑ Paulson, "ML för den arbetande programmeraren", 1996 , 7.5 Signaturbegränsningar, sid. 264.
  16. ↑ Pucella, "anteckningar om programmering av SML/NJ", 2001 , s. 58.
  17. ↑ Harper, "Intro till SML", 1986 , sid. 13.
  18. ↑ 1 2 Paulson, "ML för den arbetande programmeraren", 1996 , 7.14 openDeklarationen, sid. 299-305.
  19. ↑ Harper, "Intro till SML", 1986 , sid. 36.
  20. ↑ 1 2 3 4 Definitionen av SML, 1990 .
  21. ↑ Appel, "A Critique of Standard ML", 1992 , öppen i signaturer, sid. 17.
  22. ↑ 1 2 Paulson, "ML för den arbetande programmeraren", 1996 , Referensguide till moduler, sid. 309.
  23. ↑ Objektmix: funktioner och körtid kontra kompileringstid
  24. ↑ 1 2 Minsky översatt av DMK, 2014 , kapitel 9. Funktioner.
  25. ↑ Harper, "Intro till SML", 1986 , sid. 75-76.
  26. ↑ Paulson, "ML för den arbetande programmeraren", 1996 , 7.13 Fullt-funktionell programmering, sid. 294.
  27. ↑ Harper, "Intro till SML", 1986 , sid. 77.
  28. ↑ 1 2 Harper, "Intro till SML", 1986 , sid. 77-78.
  29. ↑ Minsky översatt av DMK, 2014 .
  30. ↑ Definitionen av SML: Reviderad, 1997 .
  31. ↑ 1 2 3 4 Kommentar till SML, 1991 .
  32. ↑ 1 2 3 4 HOF i SML/NJ .
  33. ↑ Minsky översatt av DMK, 2014 , sid. 235.
  34. ↑ 1 2 Rossberg, "1ML - Core and Modules United", 2015 .
  35. ↑ 1 2 Frisch, Garrigue, "Förstklassiga moduler i OCaml", 2010 .
  36. ↑ Rossberg - Funktioner och körtid kontra kompileringstid .
  37. ↑ Neis, Dreyer, Rossberg, "Non-Parametric Parametricity", 2009 , sid. 1-2.
  38. ↑ Rossberg, "1ML - Core and Modules United", 2015 , s. 2.
  39. ↑ 1 2 Russo, "Icke-beroende typer för moduler", 1999 .
  40. ↑ 1 2 Russo, "Förstklassiga strukturer", 2000 .
  41. ↑ 1 2 Russo, "Förstklassiga strukturer", 2000 , sid. 17.
  42. ↑ Alice - paket .
  43. ↑ Russo, "Förstklassiga strukturer", 2000 , sid. fjorton.
  44. ↑ 1 2 Rossberg, "1ML - Core and Modules United", 2015 , sid. 3.
  45. ↑ Rossberg, "1ML - Core and Modules United", 2015 , s. 13.
  46. ↑ Rossberg, "Dynamiska komponenter", 2006 .
  47. ↑ Alice - ExtModules .
  48. ↑ SML vs. Ocaml .
  49. ↑ M.L.Basis
  50. ↑ 1 2 SML.NET-kompilator
  51. ↑ 1 2 3 Poly/ML-kompilatorsida
  52. ↑ 1 2 Paulson, "ML för den arbetande programmeraren", 1996 , 7.8 Testa köstrukturerna, sid. 274.
  53. ↑ 1 2 Harper, "Naturligtvis har ML monader!" .
  54. ↑ Typindexerade värden
  55. ↑ Yaron Minsky - En fungerande programmerares guide till typindexerade värden
  56. ↑ MLKit-komiler (nedlänk) . Hämtad 21 januari 2015. Arkiverad från originalet 7 januari 2016. 
  57. ↑ Defunctorizer för OCaml .
  58. ↑ MacQueen, "Beroende typer för att uttrycka moduler", 1986 .
  59. ↑ Reynolds, "Teorier om programmeringsspråk", 1998 , 18. Modulspecifikation, sid. 398-410.
  60. ↑ Vanden Berghe .
  61. ↑ K. Czarnecki, J. O'Donnell, J. Striegnitz, W. Taha. DSL-implementering i metaocaml, mall haskell och C++ . — University of Waterloo, University of Glasgow, Research Centre Julich, Rice University, 2004. Arkiverad från originalet den 5 mars 2016.
  62. ↑ Appel, "A Critique of Standard ML", 1992 , Brist på makron, sid. 9.
  63. ↑ Steven E. Ganz, Amr Sabry, Walid Taha . Makron som flerstegsberäkningar: typsäkra, generativa, bindande makron i MacroML . - International Conference on Functional Programming, ACM Press, 2001. Arkiverad från originalet den 23 september 2015.
  64. ↑ Tofte, "Essentials of SML Modules", 1996 .
  65. ↑ Simon Peyton Jones . Att bära hårskjortan: en retrospektiv på Haskell. — POPL, 2003.
  66. ↑ 1 2 MacQueen, "Modules for Standard ML", 1984 .
  67. ↑ Xavier Leroy, "Applicative functors", 1995 .
  68. ↑ Tofte, "Essentials of SML Modules", 1996 , sid. ett.

Litteratur

Handledningar, guider, referensböcker, användning

Standard ML- språk
  • Robert Harper . Introduktion till Standard ML (obestämd). - Carnegie Mellon University, 1986. - ISBN PA 15213-3891.
    • Översättning till ryska:
      Robert Harper. Introduktion till Standard ML  (neopr.) . - Carnegie Mellon University, 1986. - 97 sid. — ISBN PA 15213-3891.
  • Lawrence C. Paulson. ML för den arbetande programmeraren  (neopr.) . — 2:a. - Cambridge, Storbritannien: Cambridge University Press, 1996. - 492 s. - ISBN 0-521-57050-6 (inbunden), 0-521-56543-X (mjuk pärm).
Ocaml språk
  • Minsky, Madhavapeddy, Hickey. Real World OKaml: Funktionell programmering för massorna  (obestämd tid) . - O'Reilly Media, 2013. - 510 sid. — ISBN 9781449324766 .
    • Översättning till ryska:
      Minsky, Madhavapeddy, Hickey. Programmering i OCaml-språket  (neopr.) . - DMK, 2014. - 536 sid. — (Funktionell programmering). - ISBN 978-5-97060-102-0 .
Modulspråk
  • Modulspråket . (Kapitel i onlineversionen av Développement d'applications avec Objective Caml av Emmanuel Chailloux, Pascal Manoury och Bruno Pagano)
  • Michael P. Fourman. SML-moduler (  (engelska) ). — 2010.

Historia, analys, kritik

  • Robin Milner , Mads Tofte, Robert Harper. Definitionen av Standard ML  (neopr.) . - The MIT Press, 1990. - ISBN 0-262-63181-4 .
  • Luca Cardelli . Typisk programmering( (engelska)) // IFIP State-of-the-Art-rapporter. - New York: Springer-Verlag, 1991. -Vol. Formell beskrivning av programmeringskoncept. —S. 431–507.
  • Andrew W. Appel. A Critique of Standard ML (  (engelska) ). — Princeton University, reviderad version av CS-TR-364-92, 1992.
  • Claudio Russo. Icke-beroende typer för moduler (  ( engelska) ) // Principer och praxis för deklarativ programmering. — Principer och praxis för deklarativ programmering, 1999.
  • Xavier Leroy. A Modular Module System (  (engelska) ) // vol.10, nummer 3. - Journal of Functional Programming, 2000. - S. 269-303 .
  • Andreas Rossberg, Claudio Russo, Derek Dreyer. F-ing-moduler (  (engelska) ). — TLDI, 2010.

Länkar