| Standard ML | |
|---|---|
| Semantik | Formell , tolkningsorienterad |
| Språkklass |
applikativ , funktionell , imperativ |
| Utförandetyp | generell mening |
| Framträdde i | 1984 [1] , 1990 [2] , 1997 [3] |
| Författare | Robin Milner med flera |
| Filtillägg _ | .sml |
| Släpp | Standard ML '97 (1997 ) |
| Typ system | Hindley - Milner |
| Stora implementeringar | många |
| Dialekter | Alice , SML# , Manticore och andra |
| Blivit påverkad | Lisp , ISWIM , ML , POP-2 , Hope , Clear [4] |
| påverkas |
Erlang , Ocaml , Haskell , efterträdare ML (sML) |
| Licens | öppen källa |
| Hemsida | sml-family.org |
| Plattform |
x86 , AMD64 , PowerPC , ARM , SPARC , S390 , DEC Alpha , MIPS , HPPA , PDP-11 , JVM , .Net , LLVM , C-- , TAL , C [5] , Ada [6] |
| OS |
* BSD , Linux ( Debian , Fedora , etc.) , Windows , Cygwin , MinGW , Darwin , Solaris , Hurd , AIX , HP-UX |
Standard ML ( SML är ett allmäntkompilerat programmeringsspråk av högre ordning baserat på systemet av typen Hindley-Milner .
Det kännetecknas av en matematiskt exakt definition (som garanterar identiteten för programmens betydelse oavsett kompilator och hårdvara), som har en bevisad tillförlitlighet av statisk och dynamisk semantik. Det är ett "mest funktionellt " språk [7] [8] , det vill säga det stöder de flesta av de tekniska funktionerna i funktionella språk, men ger också avancerade imperativa programmeringsmöjligheter när det behövs. Kombinerar stabilitet hos program, flexibilitet på nivån av dynamiskt typade språk och hastighet på nivån för C- språk ; ger utmärkt stöd för både snabb prototypframställning och modularitet och storskalig programmering [9] [10] .
SML var det första fristående kompilerade språket i ML- familjen och fungerar fortfarande som ankarspråket i ML -utvecklingsgemenskapen ( efterföljaren ML ) [11] . SML var först med att implementera ett unikt applicerande modulsystem , ML-modulspråket .
Språket är ursprungligen fokuserat på storskalig programmering av mjukvarusystem: det tillhandahåller effektiva medel för abstraktion och modularitet , vilket ger en hög kodåteranvändningshastighet , och detta gör det också lämpligt för snabb prototypframställning av program, inklusive storskalig . Till exempel, under utvecklingen av den (då fortfarande experimentella) SML/NJ-kompilatorn ( 60 tusen rader per SML), var det ibland nödvändigt att göra radikala förändringar i implementeringen av nyckeldatastrukturer som påverkar dussintals moduler – och den nya versionen av kompilatorn blev klar under dagen. [9] (Se även ICFP Programming Contest 2008, 2009.) Men till skillnad från många andra språk som är lämpliga för snabb prototyping kan SML kompilera mycket effektivt .
SML är känt för sin relativt låga starttröskel och fungerar som undervisningsspråk i programmering vid många universitet runt om i världen [12] . Det är omfattande dokumenterat i arbetsform och används aktivt av forskare som grund för att forska i nya delar av programmeringsspråk och idiom (se till exempel polymorfism av strukturella typer ). Vid det här laget har alla implementeringar av språket (inklusive föråldrade sådana) blivit öppen källkod och gratis .
Språket har en matematiskt exakt ( eng. rigorous ) formell definition som kallas "Definition" ( eng. The Definition ). För definitionen byggs ett fullständigt säkerhetsbevis som garanterar stabiliteten hos programmen och förutsägbart beteende även med felaktiga indata och eventuella programmeringsfel. Även ett buggigt SML-program beter sig alltid som ett ML-program: det kan gå in i beräkningar för alltid eller skapa ett undantag , men det kan inte krascha [13] .
SML är ett mestadels funktionellt ( mestadels funktionellt eller primärt funktionellt ) språk [7] [8] , det vill säga det stöder de flesta av de tekniska egenskaperna hos funktionella språk, men ger också imperativa programmeringsmöjligheter . Det kallas oftare för ett " språk av högre ordning för att betona stöd för förstklassiga funktioner samtidigt som det skiljer det från referenstransparenta språk .
SML ger enastående stöd för storskalig programmering genom det mest kraftfulla och uttrycksfulla modulsystemet som är känt ( ML Module Language ). SML implementerar en tidig version av modulspråket, som är ett separat lager av språket: moduler kan innehålla kärnspråksobjekt, men inte vice versa [14] .
Till skillnad från många andra språk i ML- familjen ( OCaml , Haskell , F# , Felix, Opa, Nemerle och andra) är SML väldigt minimalistisk: den har inte inbyggd objektorienterad programmering , samtidighet , ad-hoc polymorfism , dynamisk typning , listgeneratorer och många andra funktioner. SML är dock ortogonal [15] (det vill säga implementerar det minsta nödvändiga, men hela uppsättningen av maximalt olika element), vilket gör det relativt enkelt att emulera andra funktioner, och de tekniker som krävs för detta täcks brett i litteraturen . Faktum är att SML låter dig använda godtyckligt högnivåfunktionalitet som en primitiv för att implementera funktionalitet på ännu högre nivå [16] . I synnerhet byggs implementeringsmodeller av typklasser och monader med endast standard SML-konstruktioner, såväl som objektorienterade programmeringsverktyg [17] . Dessutom är SML ett av få språk som direkt implementerar förstklassiga fortsättningar .
Systemet av typen Hindley-Milner (X-M) är en utmärkande egenskap hos ML och dess ättlingar. Det säkerställer tillförlitligheten hos program på grund av tidig upptäckt av fel, hög kodåteranvändning , hög potential för optimering , kombinerar dessa kvaliteter med kortfattadhet och uttrycksfullhet på nivån för dynamiskt typade språk. De mest framträdande egenskaperna som är inneboende i X-M är typpolymorfism , såväl som algebraiska datatyper och mönstermatchning på dem.
Implementeringen av X-M i SML har följande funktioner:
Till skillnad från många språk erbjuder SML en mängd olika sätt att använda det [21] :
Samtidigt, i vissa lägen, är en mängd olika målplattformar och kompileringsstrategier möjliga :
Sammanställningsstrategierna skiljer sig också avsevärt:
Värdebegränsning _ _ _ _
KontrollstrukturerModularitet
SML -modulsystemet är det mest utvecklade modulsystemet inom programmeringsspråk. Den upprepar semantiken för kärn-ML ( eng. Core ML ), så att beroenden mellan stora programkomponenter byggs som beroenden på en liten nivå. Detta system av moduler består av tre typer av moduler:
Strukturer liknar moduler i de flesta programmeringsspråk. Signaturer fungerar som strukturgränssnitt, men är inte strikt knutna till vissa strukturer, utan bygger relationer enligt " många-till-många " -schemat , vilket gör att du flexibelt kan kontrollera synligheten av strukturkomponenter beroende på programkontextens behov.
Funktioner är " funktioner över strukturer ", som låter dig bryta kompileringstidsberoenden och beskriva parametriserade moduler. De gör det möjligt att skriva -säkert beskriva beräkningar på programkomponenter som på andra språk endast kan implementeras genom metaprogrammering [23] - som C++-mallar , endast utan smärta och lidande [24] , eller makrospråket Lisp , endast med statisk säkerhetskontroll av den genererade koden [23] . De flesta språk har inget som kan jämföras med funktioner alls [25] .
Den grundläggande skillnaden mellan ML-modulspråket är att resultatet av en funktor inte bara kan innehålla värden utan också typer, och de kan bero på de typer som är en del av funktorparametern. Detta gör ML-moduler närmast i sin uttrycksfullhet till system med beroende typer , men till skillnad från de senare kan ML-moduler reduceras till ett platt System F ω (se Modulspråk ML#F-Rossberg-Rousseau-Dreyer ).
Språkets syntax är mycket kort, sett till antalet reserverade ord upptar det en mellanposition mellan Haskell och Pascal [26] .
SML har en kontextfri grammatik , även om vissa oklarheter noteras i den. SML/NJ använder LALR(1) , men LALR(2) finns på ett ställe.
Lista över språksökord ( identifierare som matchar dem är inte tillåtna) [27] :
abstype och och även som fall datatyp gör annat slut eqtype undantag fn fun functor handle if in include infix infixr låt lokal nonfix av op öppen eller höj rec delning signatur struct struktur skriv sedan val where while with withtypeTeckenidentifierare är också tillåtna – det vill säga typ-, data- och funktionsnamn kan bestå av följande icke-alfabetiska tecken:
! % & $ # + - * / : < = > ? @ \ ~ ' ^ |Namnen på dessa symboler kan ha vilken längd som helst [27] :
val ----> = 5 kul !!? ©**??!! x = x - 1 infix 5 $^$^$^$ kul a $^$^$^$ b = a + b val :-|==>-># = Lista . foldrNaturligtvis är det inte önskvärt att använda sådana namn i praktiken, men om den tidigare författaren till den underhållna koden använde dem i stor utsträckning, blir det tack vare den formella definitionen möjligt (och SML själv gör det ganska enkelt att lösa detta problem) skriva en förprocessor för att korrigera minnesminnen.
Endast följande teckensträngar exkluderas:
: | ==> -> # :>Anledningen till denna begränsning ligger i deras speciella roll i språkets syntax:
: - explicit värdetypsanteckning _ _ | - separering av prover = - separera funktionskroppen från dess rubrik => - separera lambdafunktionens kropp från dess huvud -> — konstruktör av funktionell (pil) typ # - tillgång till postfältet :> - matcha strukturen med signaturenSML har ingen inbyggd syntax för arrayer och vektorer (konstanta arrayer). [|1,2,3|]Vissa implementeringar stöder syntaxen för arrayer ( ) och vektorer ( ) i viss utsträckning #[1,2,3]som en förlängning.
Uppgiftsoperationen skrivs som på Pascal- språk :x:=5
SML - standardbiblioteket heter Basis . Den har utvecklats under många år, efter att ha genomgått rigorösa tester på verkliga problem baserade på SML/NJ , dess utkast publicerades 1996 [28] och sedan publicerades dess specifikation officiellt 2004 [29] . Under denna period dök det redan upp manualer för dess användning [30] . Basbiblioteket implementerar endast det nödvändiga minimum av moduler: triviala datatyper, aritmetik över dem, input-output , plattformsoberoende gränssnitt till operativsystemet, etc., men implementerar inte mer komplex funktionalitet (till exempel multithreading). Många kompilatorer tillhandahåller dessutom olika experimentbibliotek.
Kompilatorer kan använda kunskap om Basis för att tillämpa föroptimerade algoritmer och specialiserade optimeringstekniker: till exempel använder MLton den ursprungliga representationen av Basistyper (som exakt motsvarar primitiva C -språktyper ) såväl som de enklaste aggregattyperna som består av dem.
Som med de flesta språk har SML Basis ett antal specifika arkitektoniska och syntaktiska konventioner. Först och främst är dessa de triviala komponenterna i standardstrukturer, såsom kombinatorer som liknar namn och signaturer (som fold). Vidare är detta ett schema som gäller för de flesta typer av konvertering till strängtyp och vice versa .
Omvandlare och skannrarStandardschemat för konvertering till och från en strängtyp är inkapslat i en struktur StringCvt:
struktur StringCvt : sig datatyp radix = BIN | okt | DEC | HEX datatype realfmt = SCI för int option | FIX av int option | GEN av int option | EXAKT typ ( 'a , 'b ) reader = 'b -> ( 'a * 'b ) alternativ val padVänster : char -> int -> sträng -> sträng val padHöger : char -> int -> sträng -> sträng val splitl : ( char -> bool ) -> ( char , 'a ) reader -> 'a -> ( string * 'a ) val takl : ( char -> bool ) -> ( char , ' a ) reader -> ' a -> string val dropl : ( char -> bool ) -> ( char , ' a ) reader - > 'a -> 'a val skipWS : ( char , 'a ) reader -> 'a -> 'a typ cs val scanString : (( char , cs ) reader -> ( 'a , cs ) reader ) -> string -> 'a option endKonverteringsschemat är inte begränsat till att lista baser av talsystem, som i C ( BIN, OCT, DEC, HEX). Det sträcker sig till högre ordningsprogrammering , vilket gör att du kan beskriva operationerna för att läsa värden av specifika typer från abstrakta strömmar och skriva till dem, och sedan omvandla enkla operationer till mer komplexa med kombinatorer . Strömmar kan vara vanliga I/O -strömmar eller bara aggregerade typer som listor eller strängar. [31]
Läsare, det vill säga värden av typen ('a,'b) reader. Intuitivt är en läsare en funktion som tar en typström som indata 'boch försöker läsa ett typvärde från den 'aoch returnerar antingen det lästa värdet och "återstoden" av strömmen, eller NONEom det misslyckas. En viktig typ av läsare är skannrar eller skanningsfunktioner. För en given typ har Tskanningsfunktionen typen
( char , 'b ) läsare -> ( T , 'b ) läsare- det vill säga, det är en omvandlare från en teckenläsare till en läsare av den här typen. Skannrar ingår i många standardmoduler, till exempel INTEGERinkluderar signaturen en skanner för heltal:
signatur INTEGER = sig eqtype int ... val scan : StringCvt . radix -> ( char , ' a ) StringCvt . reader -> 'a -> ( int * 'a ) alternativ slutSiffror läses atomärt, men läsare kan läsa från strömmar och kedjor element för element, till exempel tecken för tecken en rad från en sträng:
fun stringGetc ( s ) = let val ss = Delsträng . full ( s ) i fallet Substring . getc ( ss ) av NONE => NONE | SOME ( c , ss' ) => SOME ( c , Substring . string ( ss' )) slut ; stringGetc ( "hej" ); (* val it = SOME (#"h","ello") : (char * string) option *) stringGetc ( #2 ( valOf it ) ); (* val it = SOME (#"e","llo") : (char * string) alternativ *) stringGetc ( #2 ( valOf it ) ); (* val it = SOME (#"l","lo") : (char * string) alternativ *) stringGetc ( #2 ( valOf it ) ); (* val it = SOME (#"l","o") : (char * string) alternativ *) stringGetc ( #2 ( valOf it ) ); (* val it = SOME (#"o","") : (char * string) option *) stringGetc ( #2 ( valOf it ) ); (* val it = INGEN : (char * string) alternativ *)Med skannrar kan du skapa läsare från befintliga läsare, till exempel:
val stringGetInt = Int . skanna StringCvt . DEC -strängHämtaStrukturen StringCvtger också ett antal hjälpfunktioner. Till exempel, splitloch takelkombinera droplteckenläsare med teckenpredikat för att tillåta att strömmar filtreras.
Det bör noteras att inte karaktärsläsare är ett specialfall av läsare i allmänhet, utan vice versa [32] . Anledningen till detta är att att extrahera en delsekvens från en sekvens är en generalisering av att extrahera en delsträng från en sträng.
Definitionen ganska strikt . Skillnaderna ligger i tekniska detaljer, såsom det binära formatet av separat kompilerade moduler, implementeringen av FFI , etc. I praktiken måste ett riktigt program utgå från en viss grund (en minsta uppsättning typer, input-outputfaciliteter , etc.). Definitionen ställer dock endast minimala krav på sammansättningen av den initiala basen, så det enda observerbara resultatet av ett korrekt program enligt definitionen är att programmet avslutas eller kastar ett undantag, och de flesta implementeringar är kompatibla på denna nivå [33] .
Men även standarden Basis har några potentiella portabilitetsproblem. Till exempel [33] innehåller en konstant värdet av största möjliga heltal, insvept i den valfria typen , och måste hämtas antingen genom mönstermatchning eller genom ett funktionsanrop . 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 . Öppnas som standard , till exempel i Poly/ML -kompilatorn . Int.maxIntvalOfIntN.maxIntSOME(m)IntInf.maxIntNONEvalOf OptionIntInf
Med viss ansträngning är det möjligt att utveckla program som är fritt portabla mellan alla aktuella implementeringar av språket. Ett exempel på ett sådant program är HaMLet .
Hittills har Standard ML blivit helt offentlig: alla implementeringar är gratis och med öppen källkod och distribueras under de mest lojala licenserna ( BSD-stil , MIT ); texterna i språkdefinitionen (både i 1990 års version och den reviderade 1997 versionen) och grundspecifikationen finns också tillgängliga gratis .
SML har ett stort antal implementeringar. En betydande del av dem är skrivna i själva SML; undantagen är körtiderna för vissa kompilatorer skrivna i C och Assembler , såväl som Poplog systemet .
Kompilatorer till inbyggd kod
Verifiera kompilatorer
Kompilatorer till bytekoder och Java
Implementeringar på högre nivå
Föråldrade implementeringar
SML#
SML# [56] utökar konservativt SML med rekordpolymorfism i Atsushi Ohori-modellen , som SML# använder för att sömlöst bädda in SQL i SML-kod för intensiv databasprogrammering.
Pundsymbolen ( #) i språknamnet symboliserar väljaren (operationen att välja ett fält från en post). Kompilatorn med samma namn hävdar bra prestanda. Utvecklad och utvecklad vid Tohoku Institute (Japan) under ledning av Ohori själv.
AliceAlice ML utökar konservativt SML med primitiver för samtidig programmering baserat på den exotiska" call by future " -utvärderingsstrategin , begränsningslösaren och alla konsekventa delar av efterföljarens ML- design . I synnerhet stöder Alice förstklassiga moduler i form av paket med dynamisk laddning och dynamisk typning , vilket möjliggör implementering av distribuerad datoranvändning . Alice ger också futures förstklassiga egenskaper, inklusive tillhandahållande av futures på modulnivå ( framtida strukturer och framtida signaturer). Kompilatorn använder en virtuell maskin. Utvecklad och utvecklad vid Saarlands universitet under ledning av Andreas Rossberg.
Samtidig MLConcurrent ML (CML) ett inbäddningsbart språkbiblioteksom utökar SMLsamtidiga programmeringskonstruktioner av högre ordning baserade på densynkronaförstklassigameddelandemodellen. Ingår i standarddistributionen av SML/NJ ochMLton-kompilatorerna. Kärnidéerna för CML är kärnan i Manticore projektet och ingår i det efterföljande ML- projektet [11] .
ManticoreManticore [40] implementerar omfattande stöd för samtidig och parallell programmering, från den logiska nedbrytningen av ett system till processer till finkornig kontroll över den mest effektiva användningen av flerkärniga system . Manticore är baserat på en delmängd av SML, exklusive föränderliga arrayer och referenser, dvs det är ett rent språk som upprätthåller en strikt utvärderingsordning . Mekanismer för explicit samtidighet och grov parallellism ( trådar ) är baserade på CML , medan parallella mekanismer för fina datalager (parallella arrayer ) liknar NESL . Kompilatorn med samma namn genererar inbyggd kod .
MLPolyRMLPolyR är ett leksaksspråk som är baserat på en enkel delmängd av SML och lägger till flera nivåer av typsäkerhet till det . Målet med projektet är att fördjupa studiet av rekordpolymorfism för behoven hos det efterföljande ML- projektet . Det innovativa MLPolyR- systemet löser uttrycksproblemet och garanterar inga obehandlade undantag i program.
Utvecklad under ledning av Matthias Blum (författare till NLFFI ) vid Toyota Institute of Technology i Chicago , USA .
MythrylMythryl [57] är en syntaxvariant av SML som syftar till att påskynda utvecklingen av POSIX . Den nya syntaxen är mycket lånad från C; terminologin har också reviderats för att vara mer traditionell (till exempel har funktorer bytt namn till generika ). Samtidigt understryker författarna att de inte har för avsikt att skapa "en annan dumpning av språkdrag", utan håller sig till SML:s minimalistiska karaktär och förlitar sig på dess Definition . Implementeringen är en gaffel av SML/NJ .
Andra
Det finns inga krav på utformning av program i SML, eftersom språkets grammatik är helt kontextfri och inte innehåller uppenbara oklarheter. Den noterar dock särskilda problem, till exempel när multiplikationsoperatorn passerar op *måste den avslutande parentesen separeras med ett mellanslag ( (op * )), eftersom när de skrivs i kontinuerlig form tar många implementeringar (inte alla) ett par tecken *)för att stänga en kommentar i koden och genererar ett fel.
Det finns dock fortfarande vissa rekommendationer som syftar till att förbättra läsbarhet, modularitet och kodåteranvändning, samt tidig upptäckt av fel och ökad modifierbarhet (men inte för att mata in information om typer i identifierare, vilket görs till exempel i ungersk notation ) [ 64] . SML rekommenderar särskilt en namnkonvention för identifierare på kärnnivå som liknar den som krävs av Haskell : fooBarför värden, foo_barför typkonstruktörer , FooBarför konstruktorfunktioner (vissa kompilatorer utfärdar till och med en varning om den överträds). Detta beror på karaktären av mönstermatchning, som i allmänhet inte kan skilja mellan lokal variabelinmatning och användning av nolltypskonstruktorer , så stavfel kan leda till (relativt lätt upptäckbara) buggar [65] .
Det mest ovanliga och oväntade kan vara:
För procedurer används samma formspråk som i C : procedurer representeras av funktioner som returnerar ett värde av en enda typ :
fun p s = print s (* val p = fn : sting -> unit *) Sekventiell beräkning låt D i E sluta fun foo ... = låt val _ = ... i ... slutDetta -expansion ( engelska eta-expansion ) uttryckeär ett uttryckfn z => e z, det vill säga ett omslag av det ursprungliga uttrycket till en lambdafunktion , därzdet inte förekommer ie. Naturligtvis är detta bara vettigt omedet har en piltyp , det vill säga det är en funktion. Denna -förlängning tvingar utvärderingen att försenasetills funktionen tillämpas och att omvärderas varje gång den tillämpas. Denna teknik används i SML för att övervinna de uttrycksfulla begränsningarna som är förknippade med semantiken värderestriktionen . Termen " eta -expansion" är lånad från eta -transformationen i lambda-kalkyl , vilket tvärtom betyder reduktionen av ett uttrycktillom detinte förekommer i( eta -kontraktion). [67] [68]fn z => e zeze
Värden indexerade efter typerVärden indexerade efter typer ( engelska typindexerade värden ) är en teknik som låter dig introducera stöd för ad-hoc polymorfism i SML (som den från början saknar) [69] . Det finns ett antal av dess varianter, inklusive de som syftar till att stödja fullfjädrad objektorienterad programmering [17] .
Vik" Fold " [70] är en teknik som introducerar ett antal vanliga idiom i SML, inklusive variadiska funktioner, namngivna funktionsparametrar, standardparametervärden, syntaktisk stöd för arrayer i kod, funktionell uppdatering av poster och en kosmetisk representation av beroende typning för att tillhandahålla typsäkerhet för funktioner som printf.
PrincipDet är nödvändigt att definiera tre funktioner - fold, step0och $- så att följande likhet är sann:
vik ( a , f ) ( steg0 h1 ) ( steg0 h2 ) ... ( steg0 hn ) $ = f ( hn (... ( h2 ( h1 a )))))Deras minimala definition är lakonisk:
kul $ ( a , f ) = f a struktur Fold = struct fun fold ( a , f ) g = g ( a , f ) fun step0 h ( a , f ) = fold ( h a , f ) slutEn mer avancerad implementering låter dig styra typerna av uttryck med hjälp av Fold.
Exempel: variabelt antal funktionsargument val summa = fn z => Vik . fold ( 0 , fn s => s ) z fun a i = Vik . steg 0 ( fn s => i + s ) ... summa ( a 1 ) ( a 2 ) ( a 3 ) $ (* val it : int = 6 *)
Exempel: lista bokstavliga ord val list = fn z => Vik . vika ([], rev ) z val ' = fn z => Vik . steg1 ( op :: ) z ... lista 'w 'x 'y 'z $
Exempel: (kosmetiskt) beroende typer val f = fn z => Vik . vik ((), id ) z val a = fn z => Vik . steg0 ( fn () => "hej" ) z val b = fn z => Vik . steg0 ( fn () => 13 ) z val c = fn z => Vik . steg0 ( fn () => ( 1 , 2 )) z ... f a $ = "hej" : sträng f b $ = 13 : int f c $ = ( 1 , 2 ): int * int
Det enklaste SML-programmet kan skrivas på en rad:
skriv ut "Hej världen! \n "Men med tanke på språkets fokus på storskalig programmering , bör dess omslag i modulspråket fortfarande anses vara minimal (vissa kompilatorer fungerar bara med program på modulnivå).
Detaljer signatur HELLO_WORLD = sig val helloworld : enhet -> enhet slut struktur HelloWorld : HELLO_WORLD = struct fun helloworld () = skriv ut "Hello World! \n " slutGenerellt sett kan vilken funktion som helst väljas som startpunkt för programmet, men i praktiken är det vettigt att följa allmänt accepterade konventioner, så du bör lägga till följande kod:
struktur Main = struct fun main ( namn : sträng , args : stränglista ) : OS . _ process . status = let val _ = HelloWorld . helloworld () i OS . process . framgång slut slutFör SML/NJ kompilatorn måste du också lägga till en specifik rad i strukturen :Main
val _ = SMLofNJ . exportFn ( "projekt1" , huvud );För program med flera moduler måste du också skapa en projektfil för beroendespårning i kompilatorhanteraren (vissa kompilatorer gör detta automatiskt). Till exempel, för SML/NJ , skapa en fil med sources.cmföljande innehåll:
grupp signatur HELLO_WORLD struktur HelloWorld är helloworld-sig.sml helloworld.sml slutetEtt mer mångsidigt (men något mer begränsat) alternativ när det gäller stöd från olika kompilatorer skulle vara att skapa en vanlig SML-källkodsfil med en linjär uppräkning av inkluderar-filer:
använd "helloworld-sig.sml" ; använd "helloworld.sml" ;Utdatamaskinkoden för ett minimalt program är också relativt stor (jämfört med Hello World- implementationer i C), eftersom även det minsta SML-programmet måste inkludera språkets runtime-system , varav det mesta är skräpsamlaren . Man bör dock inte uppfatta storleken på käll- och maskinkoderna i det inledande skedet som tyngden av SML: deras anledning är språkets intensiva fokus på utvecklingen av stora och komplexa system. Ytterligare tillväxt av program följer en mycket plattare kurva än i de flesta andra statiskt typade språk, och overhead blir knappt märkbart när man utvecklar seriösa program [71] .
Den här koden konverterar platt text till HTML på det enklaste sättet och formaterar dialogrutan efter roller [72] .
Demonstration av arbeteLåt oss säga att vi har följande textfil som heter Henry.txt:
Westmoreland. Av kämpande män har de hela tre poäng tusen. Exeter. Det finns fem till en; dessutom är de alla färska. Westmoreland. 0 som vi nu hade här Men tiotusen av dessa män i England Det gör inget idag! Kung Henrik V. Vad är det han som önskar det? Min kusin Westmoreland? Nej, min fina kusin: Om vi är markerade att dö räcker vi Att göra vårt land förlust; och om att leva Ju färre män, desto större andel av äran.Ring sedan upp programmet med följande rad:
val_ = htmlCvt " Henry.txt "Kommer att skapa en fil med Henry.txt.htmlföljande innehåll:
<P><EM>Westmoreland</EM>. Av kämpande män har de hela tre poäng tusen. <P><EM>Exeter</EM>. Det finns fem till en; dessutom är de alla färska. <P><EM>Westmoreland</EM>. 0 som vi nu hade här <br>Men en tiotusen av dessa män i England <br>Det fungerar inte idag! <P><EM>Kung Henrik V</EM>. Vad är det han som önskar det? Vad är min kusin Westmoreland? Nej, min fina kusin: <br>Om vi är markerade att dö, räcker vi <br>Att göra vårt land förlust; och om att leva <br>Ju färre män, desto större andel av äran.Den här filen kan öppnas i en webbläsare genom att se följande:
Westmoreland. Av kämpande män har de hela tre poäng tusen.
Exeter. Det finns fem till en; dessutom är de alla färska.
Westmoreland. 0 som vi nu hade här
Men ett tiotusen av de männen i England
som inte jobbar idag!
Kung Henrik V. Vad är det han som önskar det?
Min kusin Westmoreland? Nej, min sköna kusin:
Om vi är markerade att dö, är vi nog
att göra vårt land förlust; och om man ska leva,
desto färre män, desto större del av äran.
För uppgiften att slå upp en sträng i en ordbok kombinerar ternära träd blixthastigheten för prefixträd med minneseffektiviteten hos binära träd .
typ nyckel = Nyckel . ord_key type item = Nyckel . ord_key list datatyp set = LEAF | NOD för { key : key , lt : set , eq : set , gt : set } val tom = LEAF undantag Redan närvarande rolig medlem (_, LEAF ) = falskt | medlem ( h::t , NODE { nyckel , lt , eq , gt }) = ( case Key . compare ( h , key ) av EQUAL => medlem ( t , eq ) | LESS => medlem ( h::t , lt ) | STÖRRE => medlem ( h::t , gt ) ) | medlem ([], NODE { nyckel , lt , eq , gt }) = ( case Key . compare ( Key . sentinel , key ) av EQUAL => true | LESS => medlem ([], lt ) | GREATER => medlem ([], gt ) ) fun insert ( h::t , LEAF ) = NOD { key = h , eq = insert ( t , LEAF ), lt = LEAF , gt = LEAF } | infoga ([], LEAF ) = NOD { key = Key . sentinel , eq = LEAF , lt = LEAF , gt = LEAF } | infoga ( h::t , NOD { nyckel , lt , eq , gt }) = ( case Key . compare ( h , key ) av EQUAL => NOD { key = key , lt = lt , gt = gt , eq = infoga ( t , eq )} | MINDRE => NOD { key = key , lt = infoga ( h::t , lt ), gt = gt , eq = eq } | GREATER => NOD { key = key , lt = lt , gt = infoga ( h::t , gt ), eq = eq } ) | infoga ([], NOD { nyckel , lt , eq , gt }) = ( case Key . compare ( Key . sentinel , key ) av EQUAL => höj RedanNärvarande | LESS => NOD { key = key , lt = infoga ([ ], lt ), gt = gt , eq = eq } | GREATER => NOD { key = key , lt = lt , gt = infoga ([], gt ), eq = eq } ) kul lägg till ( l , n ) = infoga ( l , n ) hantera Redan närvarande => nDen här koden använder en basisstruktur som är Keyjämförbar med signatur ORD_KEY, såväl som en global typ order(över vilken i synnerhet funktionen är definierad Key.compare):
datatyp order = MINDRE | LIKA | STÖRREDe typiska fördelarna med funktionell programmering ( typsäkerhet , automatisk minneshantering , en hög abstraktionsnivå, etc.) manifesteras i att säkerställa tillförlitlighet och övergripande prestanda för program, och i kritiska, särskilt storskaliga uppgifter, hastighet ofta spelar en sekundär roll. Betoningen av dessa egenskaper har historiskt sett lett till att många effektiva datastrukturer (matriser, strängar, bitsträngar) ofta inte är tillgängliga för programmerare i funktionella språk, så funktionella program är vanligtvis märkbart mindre effektiva än motsvarande C -program . [73]
ML ger initialt ganska bra finkornig hastighetskontroll , men historiskt har ML-implementeringar varit extremt långsamma. Men i början av 1990-talet läste Andrew Appel [74] att SML-språket är snabbare än C - språket , åtminstone när man arbetar intensivt med komplexa strukturerade data (men SML gör inte anspråk på att vara en ersättning för C i problem med systemprogrammering ). Under de närmaste åren ledde hårt arbete med att utveckla kompilatorer till att körhastigheten för SML-program ökade med 20-40 gånger [75] .
I slutet av 1990-talet satte Steven Wicks för sig att uppnå högsta möjliga prestanda från SML-program och skrev en defunctorizer för SML/NJ , som omedelbart visade en ökning i hastighet med ytterligare 2-3 gånger. Ytterligare arbete i denna riktning ledde till skapandet av kompilatorn MLton , som vid mitten av 2000-talet av 2000-talet visade en ökning i hastighet jämfört med andra kompilatorer med i genomsnitt två storleksordningar [45] , konkurrerande med C (för mer information, se MLton ).
Strategin för automatisk minneshantering baserad på regionslutledning eliminerar kostnaden för initiering och frigöring av minne från programexekvering (det vill säga den implementerar skräpinsamling i kompileringsstadiet). ML Kit - kompilatorn använder denna strategi för att lösa problem i realtid , även om den är sämre än MLton när det gäller optimeringsmöjligheter.
Baserat på SML/NJ frontend utvecklades en kompilator till källkod i C - sml2c . Den producerar kod av god kvalitet, men det är anmärkningsvärt att kompileringsschemat " först till C, sedan till inbyggt " saktar ner prestandan med upp till två gånger jämfört med direkt kompilering av SML till inbyggd kod på grund av semantiska skillnader mellan SML och C [5] .
Vissa SML-kompilatorer ger möjlighet att profilera koden för att avgöra vilka funktioner som tar mest processortid (och resultatet är alltid oväntat) [73] , varefter du kan fokusera på att optimera dem med SML, eller flytta dem till C kod via FFI .
Den teoretiska grunden för språket är den polymorfiskt typade lambdakalkylen (System F) , begränsad av Let-polymorphism .
"Definitionen"Den officiella "standarden" för språket är The Definition , publicerad som en bok . Definitionen är formulerad i strikta matematiska termer och har bevisad tillförlitlighet . Konsistens av definitionen tillåter en person att kontrollera programmets korrekthet och beräkna dess resultat utan att köra en specifik kompilator; men å andra sidan kräver definitionen en hög grad av skicklighet för att förstå och kan inte fungera som en lärobok i språket [74] .
Pålitlighetens bevisbarhet kom inte av sig självt – Definitionen reviderades flera gånger innan den såg dagens ljus. Många språk förlitar sig på allmänna teorier, men under utvecklingen testas de nästan aldrig för säkerheten att dela specifika språkelement som är speciella tillämpningar av dessa teorier, vilket oundvikligen leder till inkompatibilitet mellan språkimplementeringar. Dessa problem ignoreras antingen eller presenteras som ett naturfenomen ( eng. "not a bug, but a feature" ), men i verkligheten orsakas de av att språket inte har utsatts för matematisk analys [76] .
DetaljerDen ursprungliga definitionen, " The Definition of Standard ML ", publicerades 1990 [2] . Ett år senare publicerades "Comments on the Definition" (" kommentarer till standard ML "), som förklarade de tillämpade tillvägagångssätten och beteckningarna [77] . Tillsammans bildar de specifikationen för språket som nu kallas " SML'90 ". Under de följande åren dök ett antal kritik och förslag till förbättringar upp (en av de mest kända är Harper-Lilybridges genomskinliga summor ), och 1997 sammanställdes många av dessa till en reviderad version av definitionen, " The Definition of Standard ML: Reviderad " [3] , definierar en version av SML'97- språket som är bakåtkompatibel med det förra. Den reviderade definitionen använder de principer som beskrivs i 1991 års kommentarer, så de som avser att studera SML-definitionen noggrant rekommenderas att studera SML'90 först, och först sedan SML'97. [78]
Med tiden hittades ett antal oklarheter och utelämnanden i definitionstexten [79] [80] [81] . Men de förringar inte definitionens strikthet i huvudsak - beviset på dess tillförlitlighet mekaniserades i Twelf [82] . De flesta implementeringar överensstämmer med definitionen ganska strikt, avviker i tekniska egenskaper - binära format, FFI , etc., såväl som i tolkningen av tvetydiga platser i definitionen - allt detta leder till behovet av ytterligare ansträngning (mycket mindre än för de flesta andra språk) för att säkerställa perfekt portabilitet av riktiga SML-program mellan implementeringar (små program har i de flesta fall inga porteringsproblem).
SML-definitionen är ett exempel på strukturell operativ semantik ; det är inte den första formella definitionen av språket, utan den första som otvetydigt förstås av kompilatorutvecklare [83] .
Definitionen verkar på semantiska objekt och beskriver deras betydelse ( betydelse ). I inledningen framhåller författarna att det är semantiska objekt (som, beroende på det specifika språket, kan innehålla sådana begrepp som ett paket, modul, struktur, undantag, kanal, typ, procedur, länk, samanvändning etc.) och inte syntax , definiera en konceptuell representation av ett programmeringsspråk, och det är på dem som definitionen av vilket språk som helst bör byggas [84] .
Innehåll
Enligt definitionen är SML uppdelat i tre språk, byggda ovanpå varandra: ett bottenskikt som kallas " Core language " ( Core language ), ett mellanskikt som kallas " Modules " ( Modules ) och ett litet toppskikt som kallas " Program " ( Program ), som är en samling toppnivådefinitioner ( toppnivådeklarationer ).
Definitionen omfattar cirka 200 slutledningsregler ( inferens ), skrivna i form av ett vanligt bråk, där den formaliserade frasen ML står i täljarpositionen, och konsekvensen, som kan dras om frasen är korrekt, är i nämnarpositionen. .
Definitionen särskiljer tre huvudfaser i språket [85] [86] : parsing ( parsing ), utveckling ( elaboration ) och evaluation ( evaluation ). Att träna hänvisar till statisk semantik; beräkning - till dynamisk. Men utvärderingen här ska inte förväxlas med exekvering ( execution ): SML är ett uttrycksbaserat språk ( expression-based language ), och att få ett resultat från att applicera en funktion på alla argument kallas exekvering ( execution ), och "utvärdera en funktion" betyder att själv bygga en definition av det. Det bör också noteras att stödet för currying på språket innebär att alla funktioner representeras av stängningar , och det betyder i sin tur att det är felaktigt att använda termen "funktionsanrop". Istället för att anropa bör vi prata om funktionsapplikation ( funktionsapplikation ) - funktionen kan helt enkelt inte anropas förrän den tar emot alla argument; partiell tillämpning av en funktion innebär utvärdering av en ny funktion (en ny stängning ). För vart och ett av språkets lager (kärna, moduler, program) beskrivs statisk och dynamisk semantik separat, det vill säga stadierna för analys, utveckling och beräkning.
En speciell implementering av språket krävs inte för att göra alla dessa distinktioner, de är bara formell [86] . Faktum är att den enda implementeringen som strävar efter att strikt upprätthålla dem är HaMLet . Framför allt betyder produktion utan utvärdering den traditionella uppfattningen om sammanställning.
Utvärderingen av varje definition under programmets gång förändrar tillståndet för den globala miljön ( toppnivåmiljö ), kallad basen . Formellt är genomförandet av programmet beräkningen av ett nytt underlag som summan av det initiala underlaget och programdefinitioner. Standardbiblioteket i SML är "default-basen" som är tillgänglig för alla program från början, och kallas därför helt enkelt för Basis. Själva definitionen innehåller endast den initiala basen ( initial basis ), som innehåller de minsta nödvändiga definitionerna; den mer omfattande Basis standardiserades långt senare, efter att ha genomgått en långvarig utveckling i praktiken .
Harper-Stone semantikHarper-Stone semantik ( HS semantik för kort ) är en tolkning av SML i ett maskinskrivet ramverk . XC-semantiken för SML definieras genom utvecklingen av den externa SML:en till ett internt språk, vilket är en explicit typad lambdakalkyl , och fungerar således som den typteoretiska motiveringen för språket. Denna tolkning kan ses som ett alternativ till Definitionen , som formaliserar "statiska semantiska objekt" i termer av typade lambda-kalkyluttryck; och även som en deklarativ beskrivning av genereringsreglerna för typriktade kompilatorer som TILT eller SML/NJ . Faktum är att fronten av TILT-kompilatorn förkroppsligar denna semantik, även om den utvecklades flera år tidigare. [87] [88] [89]
Det interna språket är baserat på Harper-Mitchells XML-språk, men har en större uppsättning primitiver och ett mer uttrycksfullt modulsystem baserat på Harper-Lilybridges genomskinliga summor . Detta språk är lämpligt för utvecklingen av många andra språk vars semantik är baserad på lambdakalkylen , såsom Haskell och Scheme .
Detta tillvägagångssätt är inbyggt i det efterföljande ML- projektet . Samtidigt betraktas förändringar i språket som inte påverkar det interna språket som ett kortsiktigt perspektiv ( eng. kortsiktig ), och som kräver förändringar - som ett långsiktigt perspektiv ( eng. långsiktigt ).
Utvecklarna av SML satte språket till högsta kvalitetsstandard från början, så tröskeln för kritik är mycket högre än de flesta industrispråk. Omnämnanden om bristerna i SML-språket finns i den officiella pressen lika ofta som i C++-språket , och mycket oftare än de flesta andra språk, men anledningen är inte alls en negativ inställning till SML - tvärtom, all kritik mot SML framförs med en mycket varm inställning till den. Även en pedantisk analys av SML:s brister åtföljs vanligtvis av dess beskrivning som "ett fantastiskt språk, det enda seriösa språket som finns " [90] . Med andra ord, forskarna fördjupar sig grundligt i bristerna och antyder att även om man tar hänsyn till dem visar sig SML vara mer att föredra för användning i gigantiska vetenskapsintensiva projekt än många populärare språk, och vill föra SML till perfektion.
Fördelar
Brister
Huvudproblemet för SML-utvecklaren idag är den dåliga utvecklingsnivån för miljön (särskilt IDE ) och biblioteksutvecklingen.
SML-säkerhet betyder overhead på aritmetik: på grund av kravet att varje operation måste ha identiskt beteende på varje plattform, är spillkontroller , division med noll , etc. väsentliga komponenter i varje aritmetisk operation. Detta gör språket till ett ineffektivt val för nummerkrossproblem , speciellt för pipelined arkitektur [91] .
Jämförelse med OKaml :
OKaml är den närmaste släktingen till SML, efter att ha splittrats från det redan före standardisering. OKaml är så brett utvecklat att det ibland skämtsamt kallas " SML++ ". Inom massprogrammering är OCaml betydligt före SML i popularitet; i akademiska kretsar är SML mycket oftare föremål för vetenskaplig forskning. OKamls ledande utvecklare Xavier Leroy är medlem i efterträdarens ML- styrelse .
OCaml har en enda implementering som inkluderar två kompilatorer (till bytekod och till native) som är nästan identiskt kompatibla, och som ständigt utvecklas och erbjuder inte bara bättre miljöer, utan också fler och kraftfullare semantiska funktioner. SML har många olika implementeringar som följer samma språkdefinition och kärnbibliotek, och ibland erbjuder ytterligare funktioner.
De viktigaste skillnaderna är typekvivalensens semantik. För det första, i SML, är funktorer generatorer, medan de i OCaml är applikativa (se typekvivalens i ML-modulspråket ). För det andra stöder inte OCaml variabler av likhetstyp : likhetsoperationen accepterar objekt av vilken typ som helst, men ger ett undantag om de är inkompatibla.
Moderna versioner av OCaml inkluderar semantiska funktioner som endast är tillgängliga individuellt i vissa SML-tillägg, som:
Jämförelse med Haskell :
Haskell är arvtagare till ML/SML (i denna mening finns det vanligtvis ingen grundläggande skillnad mellan ML och SML). Båda språken är baserade på Hindley -Milner- typsystemet , inklusive typinferens , från vilket det finns många likheter [95] ( förstklassiga funktioner , typsäker parametrisk polymorfism , algebraiska datatyper och mönstermatchning på dem) .
Bland de viktigaste skillnaderna är [95] [96] [97] [98] [99] [68] [100] :
Den formella semantiken för SML är tolkningsorienterad , men de flesta av dess implementeringar är kompilatorer (inklusive interaktiva kompilatorer), av vilka några med säkerhet konkurrerar i effektivitet med C- språket , eftersom språket lämpar sig väl för global analys. Av samma anledning kan SML kompileras till källkod på andra hög- eller mellannivåspråk — det finns till exempel kompilatorer från SML till C och Ada .
Språket är baserat på stark statisk polymorf typning, vilket inte bara säkerställer programverifiering vid kompileringsstadiet, utan också strikt separerar mutabilitet , vilket i sig ökar potentialen för automatisk programoptimering - i synnerhet förenklar implementeringen av sophämtaren [104 ] .
Den första versionen av ML introducerades till världen 1974 som ett metaspråk för att bygga interaktiva korrektur som en del av Edinburghs LCF-system (Logic for Computable Functions) [2] . Det implementerades av Malcolm Newey, Lockwood Morris och Robin Milner på DEC10-plattformen. Den första implementeringen var extremt ineffektiv, eftersom ML-konstruktioner översattes till Lisp , som sedan tolkades [105] . Den första fullständiga beskrivningen av ML som en del av LCF publicerades 1979 [2] .
Runt 1980 implementerade Luca Cardelli den första Vax ML- kompilatorn och lade till några av hans idéer till ML. Cardelli portade snart Vax ML till Unix med Berkley Pascal. Körtiden skrevs om i C , men det mesta av kompilatorn fanns kvar i Pascal. Cardellis arbete inspirerade Milner att skapa SML som ett allmänt språk i sin egen rätt, och de började arbeta tillsammans i Edinburgh , vilket resulterade i Edinburgh ML kompilatorn , som släpptes 1984. Under loppet av detta arbete kom Mike Gordon på referenstyper och föreslog dem till Louis Damas, som senare gjorde sin avhandling om dem [106] . Samtidigt samarbetade Cambridge med INRIA. Gerard Hugh från INRIA portade ML till Maclisp under Multics. INRIA utvecklade sin egen dialekt av ML kallad Caml, som senare utvecklades till OCaml . Lawrence Paulson har optimerat Edinburgh ML så att ML-koden körs 4-5 gånger snabbare. Kort därefter utvecklade David Matthews polyspråket baserat på ML. Ytterligare arbete i denna riktning ledde till skapandet av Poly/ML miljön . 1986 formulerade David McQueen ML-modulens språk , och Andrew Appel gick med i arbetet Tillsammans började de arbetet med kompilatorn SML/NJ , som fungerade som både en forskningsplattform för språkutveckling och branschens första optimerande kompilator. Många av språkimplementeringarna utvecklades ursprungligen med SML/NJ och marknadsfördes sedan .
Med erfarenheten av storskalig utveckling upptäcktes ett antal brister i 1990 års språkdefinition . Några av bristerna åtgärdades i 1997 års revision av definitionen [3] , men omfattningen av revideringen eliminerar förlusten av bakåtkompatibilitet (koder anpassar sig kosmetiskt, utan att behöva skriva om från början). 2004 publicerades specifikationen för sammansättningen av Grundbiblioteket (ett utkast till specifikationen går tillbaka till 1996 ). Andra brister har åtgärdats på andra språk: ML skapade en hel familj av X-M-skrivna språk . Dessa språk har vunnit popularitet när det gäller språkdesign och definieras ofta som " DSL för denotationssemantik . Forskare som har varit involverade i utvecklingen och användningen av SML i nästan tre decennier, i slutet av 1900-talet, bildade en gemenskap för att skapa en ny språkefterföljare ML .
Faktum är att SML inte var den första i familjen efter själva LCF/ML - det föregicks av språk som Cardelli ML och Hope [9] . Fransmännen upprätthåller sin egen dialekt - Caml / OCaml [12] . Men när man säger "ML" menar många människor "SML" [107] , och skriver till och med genom bråket: "ML/SML" [82] .
Den mest rekommenderade [108] [109] [110] [111] [112] [113] läroboken om SML är ML for the Working Programmer [107] av Lawrence Paulson (författare till HOL- systemet ) .
För en första introduktion till språket, en kort (flera dussin sidor) kurs " Introduktion till Standard ML " av Robert Harper (tillgänglig i rysk översättning [114] ), som han använde för att lära ut språket och utökade under nästa två decennier till mer stor lärobok [115] .
Ricardo Pucellas bok [30] fungerar som en handledning för att använda språkets standardbibliotek, förutsatt att man har grundläggande kunskaper om det .
Andra läroböcker inkluderar böcker av Gilmore [116] , Ullman [117] , Shipman [118] , Cummings onlinebok [119] .
Bland guiderna för professionell användning av språket kan man lyfta fram boken av Andrew Appel (huvudutvecklare av SML/NJ ) " Modern compiler implementation in ML " [120] (denna bok har två tvillingsystrar : " Modern kompilatorimplementering i Java " och " Modern kompilatorimplementering i C ", som är likvärdiga i struktur men använder andra språk för att implementera metoderna som beskrivs). Det finns också många artiklar publicerade i tidskrifter som JFP , ML workshop, etc. [121] [122]
SML, tillsammans med OCaml , fungerar som det första undervisningsspråket för undervisning i programmering på många universitet runt om i världen. Bland applikativa språk har de förmodligen den lägsta inträdeströskeln för sig.
En betydande del av den befintliga SML-koden är antingen en implementering av sina egna kompilatorer eller automatiska bevissystem som HOL , Twelf och Isabelle (automatiserat teoremprovningssystem). Alla är gratis och öppna .
Men det finns också mer "vardagliga", inklusive egna produkter [123] .