ML

ML
Semantik multiparadigm : funktionell , imperativ , modulär
Språkklass programmeringsspråk , procedurspråk och funktionellt programmeringsspråk
Framträdde i 1973
Författare Robin Milner och andra - University of Edinburgh
Typ system stark , statisk , utgång
Dialekter Standard ML , Caml Light , OCaml , F# [1] , LazyML
Blivit påverkad JAG SIMMAR
påverkas Miranda , Haskell , Cyclone , Nemerle , C++

ML (Meta Language) är en familj av strikta funktionella programmeringsspråk med ett utvecklat parametriskt polymorft typsystem och parametriserbara moduler. Ett liknande system föreslogs först av Roger Hindley 1969 och kallas nu ofta för Hindley-Milner-systemet . Språken i denna familj är för det mesta inte rena funktionella språk, eftersom de också inkluderar imperativa instruktioner (men det finns undantag - till exempel Manticore ). ML undervisas på många västerländska universitet (i vissa till och med som det första programmeringsspråket).

Språkets bakgrund och historia

1963 implementerade John Alan Robinson en metod för att automatiskt bevisa teorem, kallad " upplösningsprincipen ". Idén med denna metod tillhör Herbran ; det föreslogs 1930 . Robinson utvecklade en beräkningseffektiv unifieringsalgoritm , som ligger till grund för metoden.

1969 cirkulerade Dana Scott ett memorandum som inte publicerades officiellt förrän 1993 [2] . I promemorian föreslogs det deduktiva systemet Logic for Computable Functions (LCF) - "logik för beräkningsbara funktioner". Ett system med samma namn , designat för att automatisera satsbevisande, utvecklades i början av 1970-talet av Robin Milner och hans medarbetare i Stanford och Edinburgh.

Den första versionen av ML-språket utvecklades som det interna språket i detta system. Som det blev tydligt för användarna av systemet var språket väl lämpat som ett allmänt programmeringsspråk. Detta ledde till att ett stort antal av dess implementeringar senare dök upp.

Funktioner

Språkets starka och statiska typsystem är baserat på lambdakalkylen , till vilken stark typning har lagts till . Det strikta typsystemet ger utrymme för optimering, så en språkkompilator dyker snart upp. Hindley-Milner-typsystemet har ett begränsat polymorft typsystem, där de flesta uttryckstyper kan härledas automatiskt . Detta gör det möjligt för programmeraren att inte explicit deklarera funktionstyper, utan att behålla en stark typkontroll.

ML är ett interaktivt språk. Varje sats som anges analyseras, kompileras och exekveras, och värdet som resulterar från körningen av satsen, tillsammans med dess typ, returneras till användaren. Språket stöder undantagshantering.

Exempel

Faktorberäkning i ML:

fun fac ( n ) = om n = 0 så 1 annat n * fac ( n- 1 );

Ett bra exempel på uttryckskraften hos ML är implementeringen av ternära sökträ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 => n

För uppgiften att söka efter en sträng i en ordbok, kombinerar det ternära sökträdet blixthastigheten för prefixträd med minneseffektiviteten för binära träd. ML-implementeringen är kompakt och självdokumenterande på grund av användningen av algebraiska typer , mönstermatchning , regeln "det sista uttrycket i den körbara kedjan är resultatet av hela funktionen " och möjligheten att bygga objekt av aggregerade typer utan föregående deklarationer . Det kännetecknas också av bevisad korrekthet  - i synnerhet eliminering av minnesläckor som är karakteristiska för C / C ++ ; eller risken för buggar i källkoden som leder till att programmet loopar i loop och minneskrävande lavin som är karakteristisk för dynamiskt typade språk.

Systemet av typen Hindley-Milner ger språk med en hög potential för optimering, så att minskning av komplexiteten och förbättring av stabiliteten hos program är "gratis" (utan förlust av effektivitet), förutsatt att en optimerande kompilator (som OCaml eller MLton) ) är tillgänglig.

Se även

Anteckningar

  1. ↑ Ml Language Arkiverad 10 oktober 2015 på Wayback Machine , c2.com
  2. ↑ Dana S. Scott. " Ett typteoretiskt alternativ till ISWIM, CUCH, OWHY Arkiverad 11 november 2020 på Wayback Machine ". Theoretical Computer Science , 121 :411–440, 1993. Kommenterad version av 1969 års manuskript.

Länkar


 Programmeringsspråk