Standard ML

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
v • d • r

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.

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]

Standard 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.

Tipsinonimon 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.

La 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.

• Alice
• ML
• Concurrent ML
• Dependent ML
• Extensible ML
• Extended ML
• F#
• OCaml
• Ur/Web

• 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