The page has not been checked
Standard ML | |
---|---|
dialekto de programlingvo • proceda programlingvo • interpretata programlingvo • funkcia programlingvo | |
Paradigmo: | plurparadigma:funkcia,ordonema |
Paradigmo(j): proceda programado • ordonema programado • modula programado • funkcia programado | |
Tipa sistemo: | forta,statika,dedukta |
Ĉefaj realigoj: | MLKit,MLton,MLWorks,Moscow ML,Poly/ML,SML/NJ,MLj,SML.NET |
Programlingva(j) dialekto(j): | Alice,Concurrent ML,Dependent ML |
Kreita sub la influo de: | ML,Hope |
Havas influon sur: | Elm,F*,OCaml,Rust,Scala |
Standard ML (SML;angle Standard Meta Language) estas ĝeneralcela,modula,funkcia programlingvo kuncompile-time type checking kajtype inference. Ĝi popularas inter skribistoj detradukiloj kajprogramlingvaj esploristoj, kaj ankaŭ ĉe la ellaborado deteorempruviloj.
SML estas moderna dialekto deML, la programlingvo uzita en la teorempruvila projektoLogic for Computable Functions (LCF). Ĝi distingindas inter vaste uzataj lingvoj pro tio, ke ĝi havas formalan specifigon, donitan kieltipreguloj kajoperaciaj semantikoj enThe Definition of Standard ML (1990, reviziita kaj simpligita kielThe Definition of Standard ML (Revised) en 1997).[1]
Standard ML estas funkcia programlingvo kun kelkaj malpuraj funkcioj. Programoj skribitaj en Standard ML konsistas elesprimoj evaluotaj, kontraste kun ordonoj aŭ komandoj, kvankam kelkaj esprimoj liveras trivialan valoron “unit” kaj evaluiĝas nur pro siaj flankefikoj.
Samkiel ĉiuj funkciaj programlingvoj, nepra trajto de Standard ML estasfunkcioj, ili uziĝas por abstraktigo. Ekzemple, lafaktorialan funkcion oni povas esprimi per:
funfaktorialon=ifn=0then1elsen*faktorialo(n-1)
Tradukilo de Standard ML devas dedukta la statikan tiponint -> int
de tiu funkcio sen tipnotoj donitaj de la uzanto. Ekz., ĝi devas dedukti, ken nur uziĝas kun entjeraj esprimoj, kaj do ĝi mem devas esti entjero, kaj ke ĉiuj valorproduktaj esprimoj ene de la funkcio liveras entjerojn.
La saman funkcion oni povas esprimi perklaŭzaj funkcidifinoj, kie la kondiĉilojif-then-else anstataŭiĝas de sinsekvo de ŝablonoj de la faktoriala funkcio evaluata por specifaj valoroj. La ŝablonoj disas per '|' kaj evaluiĝas unu post unu laŭ la ordo skribita, ĝis kongruo troviĝas:
funfaktorialo0=1|faktorialon=n*faktorialo(n-1)
Oni povas reskribi ĉi tion percase-esprimo, kiel jene:
valrecfaktorialon=casenof0=>1|n=>n*factorial(n-1)
aŭ kiel sennoman funkcion (lambdofunkcion):
valrecfaktorialo=fn0=>1|n=>n*faktorialo(n-1)
Ĉi tie, la ŝlosilvortoval
enkondukas ligon de identigilo al valoro,fn
enkondukas la difinon desennoma funkcio, kajcase
enkondukas sinsekvon de modeloj kaj korespondaj esprimoj.
Per uzo de loka funkcio, ĉi tiun funkcion oni povas reskribi en pli rendimentanvostorikuran stilon.
funfaktorialon=letfunlp(0,akum)=akum|lp(m,akum)=lp(m-1,m*akum)inlp(n,1)end
(La valoro delet-esprimo estas tiu de la esprimo interin kajend.) La enkapsuligo de invariantodaŭriga vostorikura strikta iteraciado per unu aŭ pliaj akumulaj parametroj ene de seninvarianta ekstera funkcio, kiel vidite ĉi tie, estas komuna idiomo en Standard ML, kaj aperas ege ofte en SML-kodo.
Tipsinonimon oni difinas per la ŝlosilvortotype. Jen tipsinonimo por punktoj el plano, kaj funkcioj, kiuj komputas la distancon inter du punktoj kaj la areon de triangulo kun la donitaj anguloj laŭ laformulo de Heron.
typeloc=real*realfundist((x0,y0),(x1,y1))=letvaldx=x1-x0valdy=y1-y0inMath.sqrt(dx*dx+dy*dy)endfunheron(a,b,c)=letvalab=dist(a,b)valbc=dist(b,c)valac=dist(a,c)valperim=ab+bc+acvals=perim/2.0inMath.sqrt(s*(s-ab)*(s-bc)*(s-ac))end
La tipoj dedist
kajheron
estasloc * loc -> real
kajloc * loc * loc -> real
respektive.
La la tutakompania arĥitekturo de la Universitato de Kopenhago realiĝis per ĉirkaŭ 100000 linioj de SML, inkluzive registroj de oficistaro, salajroj, kursadministrado kaj prisondo, administrado de studentaj projektoj, kaj TTT-aj memservaj interfacoj.
La pruvhelpiloIsabelle estas skribita en SML.
SML vaste uzatas interne fare de dizajnistoj de tradukiloj kaj blatoj, ekzemple deARM.