Standard ML
Standard ML (SML; angle Standard Meta Language) estas ĝeneralcela, modula, funkcia programlingvo kun compile-time type checking kaj type inference. Ĝi popularas inter skribistoj de tradukiloj kaj programlingvaj esploristoj, kaj ankaŭ ĉe la ellaborado de teorempruviloj.
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 |
SML estas moderna dialekto de ML, la programlingvo uzita en la teorempruvila projekto Logic for Computable Functions (LCF). Ĝi distingindas inter vaste uzataj lingvoj pro tio, ke ĝi havas formalan specifigon, donitan kiel tipreguloj kaj operaciaj semantikoj en The Definition of Standard ML (1990, reviziita kaj simpligita kiel The Definition of Standard ML (Revised) en 1997).[1]
Lingvo
redaktiStandard ML estas funkcia programlingvo kun kelkaj malpuraj funkcioj. Programoj skribitaj en Standard ML konsistas el esprimoj 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 estas funkcioj, ili uziĝas por abstraktigo. Ekzemple, la faktorialan funkcion oni povas esprimi per:
fun faktorialo n = if n = 0 then 1
else n * faktorialo (n - 1)
Tradukilo de Standard ML devas dedukta la statikan tipon int -> int
de tiu funkcio sen tipnotoj donitaj de la uzanto. Ekz., ĝi devas dedukti, ke n 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 per klaŭzaj funkcidifinoj, kie la kondiĉiloj if-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:
fun faktorialo 0 = 1
| faktorialo n = n * faktorialo (n - 1)
Oni povas reskribi ĉi tion per case-esprimo, kiel jene:
val rec faktorialo n =
case n of 0 => 1
| n => n * factorial (n - 1)
aŭ kiel sennoman funkcion (lambdofunkcion):
val rec faktorialo = fn 0 => 1
| n => n * faktorialo (n - 1)
Ĉi tie, la ŝlosilvorto val
enkondukas ligon de identigilo al valoro, fn
enkondukas la difinon de sennoma funkcio, kaj case
enkondukas sinsekvon de modeloj kaj korespondaj esprimoj.
Per uzo de loka funkcio, ĉi tiun funkcion oni povas reskribi en pli rendimentan vostorikuran stilon.
fun faktorialo n =
let fun lp (0, akum) = akum
| lp (m, akum) = lp (m - 1, m * akum)
in
lp (n, 1)
end
(La valoro de let-esprimo estas tiu de la esprimo inter in kaj end.) 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.
Tipsinonimoj
redaktiTipsinonimon oni difinas per la ŝlosilvorto type. 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ŭ la formulo de Heron.
type loc = real * real
fun dist ((x0, y0), (x1, y1)) =
let val dx = x1 - x0
val dy = y1 - y0
in
Math.sqrt (dx * dx + dy * dy)
end
fun heron (a, b, c) =
let val ab = dist (a, b)
val bc = dist (b, c)
val ac = dist (a, c)
val perim = ab + bc + ac
val s = perim / 2.0
in
Math.sqrt (s * (s - ab) * (s - bc) * (s - ac))
end
La tipoj de dist
kaj heron
estas loc * loc -> real
kaj loc * loc * loc -> real
respektive.
Grandaj projektoj uzantaj SML
redaktiLa la tuta kompania 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 pruvhelpilo Isabelle estas skribita en SML.
SML vaste uzatas interne fare de dizajnistoj de tradukiloj kaj blatoj, ekzemple de ARM.
Vidu ankaŭ
redaktiReferencoj
redakti- ↑ MILNER, Robin; TOFTE, Mads; HARPER, Robert; MACQUEEN, David. (1997) The Definition of Standard ML (Revised) (angle). ISBN 0-262-63181-4.
Eksteraj ligiloj
redakti- Standard ML Family GitHub Project Arkivigite je 2020-02-20 per la retarkivo Wayback Machine
- Standard ML language Mads Tofte, Scholarpedia, 4(2):7515. doi:10.4249/scholarpedia.7515
- What is SML?
- What is SML '97?
- successor ML (sML) Arkivigite je 2009-01-07 per la retarkivo Wayback Machine is intended to provide a vehicle for the continued evolution of ML, using Standard ML as a starting point.
- Programming in Standard ML
- Programming in Standard ML '97: An On-line Tutorial
- Univ. of Chicago - SML tutorial (slides)
- CSE341: Programming Languages, Dan Grossman, University of Washington. Ankaŭ en Coursera kaj YouTube