ML estándar

El lenguaje de programación estándar ( SML ) es un lenguaje de programación funcional , modular , de alto nivel y de propósito general con verificación de tipos en tiempo de compilación e inferencia de tipos . Es popular para escribir compiladores , para la investigación de lenguajes de programación y para desarrollar demostradores de teoremas .

El ML estándar es un dialecto moderno del ML , el lenguaje utilizado en el proyecto de demostración de teoremas de Lógica para Funciones Computables (LCF). Se distingue de los lenguajes más utilizados porque tiene una especificación formal , que se da como reglas de tipado y semántica operacional en La definición del ML estándar . ^[5]

Standard ML es un lenguaje de programación funcional con algunas características impuras. Los programas escritos en Standard ML consisten en expresiones en lugar de instrucciones o comandos, aunque algunas expresiones de tipo unit solo se evalúan por sus efectos secundarios .

Como todos los lenguajes funcionales, una característica clave del ML estándar es la función , que se utiliza para la abstracción. La función factorial se puede expresar de la siguiente manera:

 factorial  divertido n  =  
    si  n  =  0  entonces  1  de lo contrario  n  *  factorial  ( n  -  1 )

Un compilador SML debe inferir el tipo estático sin anotaciones de tipo proporcionadas por el usuario. Debe deducir que solo se utiliza con expresiones enteras y, por lo tanto, debe ser un entero, y que todas las expresiones terminales son expresiones enteras. val factorial : int -> intn

La misma función se puede expresar con definiciones de funciones clausulas donde el condicional if - then - else se reemplaza con plantillas de la función factorial evaluada para valores específicos:

 factorial  divertido 0  =  1 
  |  factorial  n  =  n  *  factorial  ( n  -  1 )

o iterativamente:

fun  factorial  n  =  sea  val  i  =  ref  n  y  acc  =  ref  1  en 
    while  !i  >  0  do  ( acc  :=  !acc  *  !i ;  i  :=  !i  -  1 );  !acc 
fin

o como función lambda:

val  rec  factorial  =  fn  0  =>  1  |  n  =>  n  *  factorial  ( n  -  1 )

Aquí, la palabra clave valintroduce una vinculación de un identificador a un valor, fnintroduce una función anónima y recpermite que la definición sea autorreferencial.

La encapsulación de un bucle estrecho recursivo de cola que preserva invariantes con uno o más parámetros acumuladores dentro de una función externa libre de invariantes, como se ve aquí, es un modismo común en el aprendizaje automático estándar.

Usando una función local, se puede reescribir en un estilo recursivo de cola más eficiente:

    bucle local fun  ( 0 , acc ) = acc | bucle ( m , acc ) = bucle ( m - 1 , m * acc ) en fun factorial n = bucle ( n , 1 ) fin    
                 

          

Un sinónimo de tipo se define con la palabra clave type. Aquí hay un sinónimo de tipo para puntos en un plano y funciones que calculan las distancias entre dos puntos y el área de un triángulo con los vértices dados según la fórmula de Heron . (Estas definiciones se utilizarán en ejemplos posteriores).

tipo  loc  =  real  *  real

 cuadrado  divertido ( x  :  real )  =  x  *  x

fun  dist  ( x ,  y )  ( x' ,  y' )  = 
    Math . sqrt  ( cuadrado  ( x'  -  x )  +  cuadrado  ( y'  -  y ))

fun  garza  ( a ,  b ,  c )  =  sea 
    val  x  =  dist  a  b 
    val  y  =  dist  b  c 
    val  z  =  dist  a  c 
    val  s  =  ( x  +  y  +  z )  /  2.0 
    en 
        Matemáticas . sqrt  ( s  *  ( s  -  x )  *  ( s  -  y )  *  ( s  -  z )) 
    fin

El ML estándar ofrece un sólido soporte para los tipos de datos algebraicos (ADT). Un tipo de datos puede considerarse como una unión disjunta de tuplas (o una "suma de productos"). Son fáciles de definir y de usar, en gran medida debido a la coincidencia de patrones y a la comprobación de exhaustividad de patrones y redundancia de patrones de la mayoría de las implementaciones del ML estándar.

En los lenguajes de programación orientados a objetos , una unión disjunta se puede expresar como jerarquías de clases . Sin embargo, a diferencia de las jerarquías de clases , los TAD son cerrados . Por lo tanto, la extensibilidad de los TAD es ortogonal a la extensibilidad de las jerarquías de clases. Las jerarquías de clases se pueden extender con nuevas subclases que implementan la misma interfaz, mientras que las funciones de los TAD se pueden extender para el conjunto fijo de constructores. Véase el problema de expresión .

Un tipo de datos se define con la palabra clave datatype, como en:

tipo de datos  forma 
    =  Círculo    de  loc  *  real       (* centro y radio *) 
    |  Cuadrado    de  loc  *  real       (* esquina superior izquierda y longitud del lado; alineado al eje *) 
    |  Triángulo  de  loc  *  loc  *  loc  (* esquinas *)

Tenga en cuenta que un sinónimo de tipo no puede ser recursivo; los tipos de datos son necesarios para definir constructores recursivos. (Esto no es un problema en este ejemplo).

Los patrones se comparan en el orden en el que se definen. Los programadores de C pueden usar uniones etiquetadas , que se despachan en valores de etiqueta, para hacer lo que ML hace con los tipos de datos y la comparación de patrones. Sin embargo, si bien un programa en C decorado con las comprobaciones adecuadas será, en cierto sentido, tan robusto como el programa ML correspondiente, esas comprobaciones serán necesariamente dinámicas; las comprobaciones estáticas de ML brindan garantías sólidas sobre la corrección del programa en el momento de la compilación.

Los argumentos de función se pueden definir como patrones de la siguiente manera:

 área  divertida ( Círculo  (_,  r ))  =  Math . pi  *  cuadrado  r 
  |  área  ( Cuadrado  (_,  s ))  =  cuadrado  s 
  |  área  ( Triángulo  p )  =  garza  p  (* ver arriba *)

La denominada "forma clausular" de definición de función, donde los argumentos se definen como patrones, es meramente una sintaxis simplificada para una expresión de caso:

 Forma del área  de diversión = forma del caso del Círculo (_, r ) => Matemáticas . pi * cuadrado r | Cuadrado (_, s ) => cuadrado s | Triángulo p => garza p    
           
        
       

La verificación de exhaustividad de patrones garantizará que cada constructor del tipo de datos coincida con al menos un patrón.

El siguiente patrón no es exhaustivo:

diversión  centro  ( Círculo  ( c ,  _))  =  c 
  |  centro  ( Cuadrado  (( x ,  y ),  s ))  =  ( x  +  s  /  2.0 ,  y  +  s  /  2.0 )

No existe ningún patrón para el Trianglecaso en la centerfunción. El compilador emitirá una advertencia indicando que la expresión del caso no es exhaustiva y, si Trianglese pasa a esta función en tiempo de ejecución, se generará . exception Match

El patrón en la segunda cláusula de la siguiente función (sin sentido) es redundante:

fun  f  ( Círculo  (( x ,  y ),  r ))  =  x  +  y 
  |  f  ( Círculo  _)  =  1.0 
  |  f  _  =  0.0

Cualquier valor que coincida con el patrón de la segunda cláusula también coincidiría con el patrón de la primera cláusula, por lo que la segunda cláusula es inalcanzable. Por lo tanto, esta definición en su conjunto presenta redundancia y provoca una advertencia en tiempo de compilación.

La siguiente definición de función es exhaustiva y no redundante:

val  tieneEsquinas  =  fn  ( Círculo  _)  =>  falso  |  _  =>  verdadero

Si el control pasa el primer patrón ( Circle), sabemos que la forma debe ser a Squareo a Triangle. En cualquiera de esos casos, sabemos que la forma tiene esquinas, por lo que podemos regresar truesin discernir la forma real.

Las funciones pueden consumir funciones como argumentos:

 mapa  divertido f  ( x ,  y )  =  ( f  x ,  f  y )

Las funciones pueden producir funciones como valores de retorno:

 constante  de diversión k  =  ( fn  _  =>  k )

Las funciones también pueden consumir y producir funciones:

diversión  componer  ( f ,  g )  =  ( fn  x  =>  f  ( g  x ))

La función List.mapde la biblioteca base es una de las funciones de orden superior más utilizadas en ML estándar:

 mapa  divertido _  []  =  [] 
  |  mapa  f  ( x  ::  xs )  =  f  x  ::  mapa  f  xs

Una implementación más eficiente con tail-recursive List.foldl:

fun  map  f  =  Lista . rev  o  Lista . foldl  ( fn  ( x ,  acc )  =>  f  x  ::  acc )  []

Las excepciones se generan con la palabra clave raisey se manejan con la handleconstrucción de coincidencia de patrones. El sistema de excepciones puede implementar una salida no local; esta técnica de optimización es adecuada para funciones como las siguientes.

    excepción  local Cero ; 
    val  p  =  fn  ( 0 ,  _)  =>  raise  Cero  |  ( a ,  b )  =>  a  *  b 
en 
    fun  prod  xs  =  List . foldl  p  1  xs  manejador  Cero  =>  0 
fin

Cuando se activa, el control abandona la función por completo. Considere la alternativa: se devolvería el valor 0, se multiplicaría por el siguiente entero de la lista, se devolvería el valor resultante (inevitablemente 0), y así sucesivamente. La activación de la excepción permite que el control se salte toda la cadena de cuadros y evite el cálculo asociado. Observe el uso del guión bajo ( ) como patrón comodín. exception ZeroList.foldl_

La misma optimización se puede obtener con una llamada de cola .

    diversión  local p  a  ( 0  ::  _)  =  0 
      |  p  a  ( x  ::  xs )  =  p  ( a  *  x )  xs 
      |  p  a  []  =  a 
en 
    val  prod  =  p  1 
fin

El sistema de módulos avanzado de ML estándar permite descomponer los programas en estructuras organizadas jerárquicamente de definiciones de tipo y valor relacionadas lógicamente. Los módulos no solo proporcionan control del espacio de nombres , sino también abstracción, en el sentido de que permiten la definición de tipos de datos abstractos . Tres construcciones sintácticas principales comprenden el sistema de módulos: firmas, estructuras y funtores.

Una firma es una interfaz , generalmente considerada como un tipo para una estructura; especifica los nombres de todas las entidades proporcionadas por la estructura, la aridad de cada componente de tipo, el tipo de cada componente de valor y la firma de cada subestructura. Las definiciones de los componentes de tipo son opcionales; los componentes de tipo cuyas definiciones están ocultas son tipos abstractos .

Por ejemplo, la firma de una cola puede ser:

firma  COLA  =  sig 
    tipo  'una  cola 
    excepción  QueueError ; 
    val  vacío      :  'una  cola 
    val  está Vacío    :  'una  cola  ->  bool 
    val  singleton  :  'a  ->  'una  cola 
    val  fromList   :  'una  lista  ->  'una  cola 
    val  insertar     :  'a  *  'una  cola  ->  'una  cola 
    val  peek       :  'una  cola  ->  'a 
    val  eliminar     :  'una  cola  ->  'a  *  '  una cola 
fin

Esta firma describe un módulo que proporciona un tipo polimórfico , y valores que definen operaciones básicas en colas. 'a queueexception QueueError

Una estructura es un módulo; consiste en una colección de tipos, excepciones, valores y estructuras (llamadas subestructuras ) empaquetadas juntas en una unidad lógica.

Una estructura de cola se puede implementar de la siguiente manera:

estructura  TwoListQueue  :>  QUEUE  =  struct 
    type  'una  cola  =  'una  lista  *  'una  lista

    excepción  QueueError ;

    val  vacio  =  ([],  [])

    fun  isEmpty  ([],  [])  =  verdadero 
      |  isEmpty  _  =  falso

    diversión  singleton  a  =  ([],  [ a ])

    diversión  deLista  a  =  ([],  a )

    fun  insert  ( a ,  ([],  []))  =  singleton  a 
      |  insert  ( a ,  ( entradas ,  salidas ))  =  ( a  ::  entradas ,  salidas )

    diversión  peek  (_,  [])  =  generar  QueueError 
      |  peek  ( entradas ,  salidas )  =  List . hd  salidas

    diversión  eliminar  (_,  [])  =  generar  QueueError 
      |  eliminar  ( ins ,  [ a ])  =  ( a ,  ([],  List . rev  ins )) 
      |  eliminar  ( ins ,  a  ::  outs )  =  ( a ,  ( ins ,  outs )) 
fin

Esta definición declara que implementa . Además, la atribución opaca denotada por establece que cualquier tipo que no esté definido en la firma (es decir, ) debe ser abstracto, lo que significa que la definición de una cola como un par de listas no es visible fuera del módulo. La estructura implementa todas las definiciones en la firma. structure TwoListQueuesignature QUEUE:>type 'a queue

Se puede acceder a los tipos y valores de una estructura con "notación de puntos":

val  q  :  cadena  TwoListQueue . queue  =  TwoListQueue . empty 
val  q'  =  TwoListQueue . insert  ( Real . toString  Math . pi ,  q )

Un funtor es una función de estructuras a estructuras; es decir, un funtor acepta uno o más argumentos, que suelen ser estructuras de una firma determinada, y produce una estructura como resultado. Los funtores se utilizan para implementar estructuras de datos y algoritmos genéricos .

Un algoritmo popular ^[6] para la búsqueda en amplitud de árboles utiliza colas. A continuación se muestra una versión de ese algoritmo parametrizada sobre una estructura de cola abstracta:

(*según Okasaki, ICFP, 2000*) 
functor  BFS  ( Q :  QUEUE )  =  struct 
  tipo de datos  'un  árbol  =  E  |  T  de  'un  *  'un  árbol  *  'un  árbol

  
    fun  local bfsQ  q  =  si  Q . isEmpty  q  entonces  []  de lo contrario  buscar  ( Q . remove  q ) 
    y  buscar  ( E ,  q )  =  bfsQ  q 
      |  buscar  ( T  ( x ,  l ,  r ),  q )  =  x  ::  bfsQ  ( insertar  ( insertar  q  l )  r ) 
    e  insertar  q  a  =  Q . insertar  ( a ,  q ) 
  en 
    fun  bfs  t  =  bfsQ  ( Q . singleton  t ) 
  fin 
fin

estructura  QueueBFS  =  BFS  ( TwoListQueue )

Dentro de , la representación de la cola no es visible. Más concretamente, no hay forma de seleccionar la primera lista en la cola de dos listas, si esa es de hecho la representación que se está utilizando. Este mecanismo de abstracción de datos hace que la búsqueda en amplitud sea verdaderamente independiente de la implementación de la cola. Esto es deseable en general; en este caso, la estructura de la cola puede mantener de manera segura cualquier invariante lógica de la que dependa su corrección detrás del muro a prueba de balas de la abstracción. functor BFS

Los fragmentos de código SML se estudian más fácilmente ingresándolos en un archivo de nivel superior interactivo .

El siguiente es un programa "¡Hola, mundo!" :

La ordenación por inserción (ascendente) se puede expresar de forma concisa de la siguiente manera: int list

fun  insert  ( x ,  [])  =  [ x ]  |  insert  ( x ,  h  ::  t )  =  ordenar  x  ( h ,  t ) 
y  ordenar  x  ( h ,  t )  =  si  x  <  h  entonces  [ x ,  h ]  @  t de  lo contrario  h  ::  insert  ( x ,  t ) 
val  insertionsort  =  List.foldl insert [ ]  

Aquí, el algoritmo clásico de ordenación por fusión se implementa en tres funciones: split, merge y mergesort. Observe también la ausencia de tipos, con excepción de la sintaxis y que significan listas. Este código ordenará listas de cualquier tipo, siempre que se defina una función de ordenación consistente. Mediante la inferencia de tipos de Hindley-Milner , se pueden inferir los tipos de todas las variables, incluso los tipos complicados como el de la función . op ::[]cmpcmp

Dividir

fun splitse implementa con un cierre con estadotrue que alterna entre y false, ignorando la entrada:

 alternador  divertido {}  =  let  val  estado  =  ref  verdadero 
    en  fn  a  =>  !estado  antes de  estado  :=  no  ( !estado )  fin

(* Dividir una lista en mitades casi iguales que tendrán la misma longitud, 
* o la primera tendrá un elemento más que la otra. * Se ejecuta en tiempo O(n), donde n = | 
xs |. 
*) 
fun  split  xs  =  List .partition ( alternator  {}) xs  

Unir

Merge utiliza un bucle de función local para lograr eficiencia. La función interna loopse define en términos de casos: cuando ambas listas no están vacías ( ) y cuando una lista está vacía ( ). x :: xs[]

Esta función fusiona dos listas ordenadas en una sola lista ordenada. Observe cómo el acumulador accse construye al revés y luego se invierte antes de ser devuelto. Esta es una técnica común, ya que se representa como una lista enlazada ; esta técnica requiere más tiempo de reloj, pero las asintóticas no son peores. 'a list

(* Fusionar dos listas ordenadas usando el orden cmp. 
* Pre: cada lista ya debe estar ordenada por cmp. 
* Se ejecuta en tiempo O(n), donde n = |xs| + |ys|. 
*) 
fun  merge  cmp  ( xs ,  [])  =  xs 
  |  merge  cmp  ( xs ,  y  ::  ys )  =  let 
    fun  loop  ( a ,  acc )  ( xs ,  [])  =  List . revAppend  ( a  ::  acc ,  xs ) 
      |  loop  ( a ,  acc )  ( xs ,  y  ::  ys )  = 
        if  cmp  ( a ,  y ) 
        then  loop  ( y ,  a  ::  acc )  ( ys ,  xs ) 
        else  loop  ( a ,  y  ::  acc )  ( xs ,  ys ) 
    in 
        loop  ( y ,  [])  ( ys ,  xs ) 
    end

Ordenación por fusión

La función principal:

diversión  ap  f  ( x ,  y )  =  ( f  x ,  f  y )

(* Ordena una lista según la operación de ordenación dada cmp. 
* Se ejecuta en tiempo O(n log n), donde n = |xs|. 
*) 
fun  mergesort  cmp  []  =  [] 
  |  mergesort  cmp  [ x ]  =  [ x ] 
  |  mergesort  cmp  xs  =  ( merge  cmp  o  ap  ( mergesort  cmp )  o  split )  xs

Quicksort se puede expresar de la siguiente manera. es un cierre que consume un operador de orden . fun partop <<

infijo  <<

fun  quicksort  ( op  << )  =  let 
    fun  part  p  =  List .partition ( fn x => x << p ) fun sort  [] = [ ] | sort ( p :: xs ) = join p ( part p xs ) y join p ( l , r ) = sort l @ p :: sort r en sort end     
        
                
                
    
        
    

Observe la relativa facilidad con la que se puede definir y procesar un lenguaje de expresión pequeño:

excepción  TyErr ;

tipo de datos  ty  =  IntTy  |  BoolTy

diversión  unificar  ( IntTy ,  IntTy )  =  IntTy 
  |  unificar  ( BoolTy ,  BoolTy )  =  BoolTy 
  |  unificar  (_,  _)  =  generar  TyErr

tipo de datos  exp 
    =  Verdadero 
    |  Falso 
    |  Int  de  int 
    |  No  de  exp 
    |  Suma  de  exp  *  exp 
    |  Si   de  exp  *  exp  *  exp

fun  infer  True  =  BoolTy 
  |  inferir  False  =  BoolTy 
  |  inferir  ( Int  _)  =  IntTy 
  |  inferir  ( Not  e )  =  ( assert  e  BoolTy ;  BoolTy ) 
  |  inferir  ( Add  ( a ,  b ))  =  ( assert  a  IntTy ;  assert  b  IntTy ;  IntTy ) 
  |  inferir  ( If  ( e ,  t ,  f ))  =  ( assert  e  BoolTy ;  unificar  ( inferir  t ,  inferir  f )) 
y  assert  e  t  =  unificar  ( inferir  e ,  t )

fun  eval  Verdadero  =  Verdadero 
  |  eval  Falso  =  Falso 
  |  eval  ( Int  n )  =  Int  n 
  |  eval  ( Not  e )  =  si  eval  e  =  Verdadero  entonces  Falso  de lo contrario  Verdadero 
  |  eval  ( Add  ( a ,  b ))  =  ( case  ( eval  a ,  eval  b )  de  ( Int  x ,  Int  y )  =>  Int  ( x  +  y )) 
  |  eval  ( Si  ( e ,  t ,  f ))  =  eval  ( si  eval  e  =  Verdadero  entonces  t  de lo contrario  f )

fun  run  e  =  ( inferir  e ;  ALGUNOS  ( evaluar  e ))  manejar  TyErr  =>  NINGUNO

Ejemplo de uso en expresiones bien tipificadas y mal tipificadas:

val  SOME  ( Int  3 )  =  run  ( Add  ( Int  1 ,  Int  2 ))  (* bien tipado *) 
val  NONE  =  run  ( If  ( Not  ( Int  1 ),  True ,  False ))  (* mal tipado *)

El IntInfmódulo proporciona aritmética de números enteros con precisión arbitraria. Además, los literales enteros se pueden utilizar como números enteros con precisión arbitraria sin que el programador tenga que hacer nada.

El siguiente programa implementa una función factorial de precisión arbitraria:

Las funciones currificadas tienen muchas aplicaciones, como la eliminación de código redundante. Por ejemplo, un módulo puede requerir funciones de tipo , pero es más conveniente escribir funciones de tipo donde exista una relación fija entre los objetos de tipo y . Una función de tipo puede factorizar esta característica común. Este es un ejemplo del patrón adaptador . ^{[ cita requerida ]}a -> ba * c -> bacc -> (a * c -> b) -> a -> b

En este ejemplo, calcula la derivada numérica de una función dada en el punto : fun dfx

-  fun  d  delta  f  x  =  ( f  ( x  +  delta )  -  f  ( x  -  delta ))  /  ( 2.0  *  delta )
 val  d  =  fn  :  real  ->  ( real  ->  real )  ->  real  ->  real

El tipo de indica que asigna un "float" a una función con el tipo . Esto nos permite aplicar argumentos parcialmente, lo que se conoce como currying . En este caso, la función se puede especializar aplicándola parcialmente con el argumento . Una buena opción para usar este algoritmo es la raíz cúbica de la máquina épsilon . ^{[ cita requerida ]}fun d(real -> real) -> real -> realddeltadelta

-  val  d'  =  d  1E~8 ;
 val  d'  =  fn  :  ( real  ->  real )  ->  real  ->  real

El tipo inferido indica que d'se espera una función con el tipo como primer argumento. Podemos calcular una aproximación a la derivada de en . La respuesta correcta es . real -> real${\displaystyle f(x)=x^{3}-x-1}$${\displaystyle x=3}$${\displaystyle f'(3)=27-1=26}$

-  d'  ( fn  x  =>  x  *  x  *  x  -  x  -  1.0 )  3.0 ;
 val  it  =  25.9999996644  :  real

La biblioteca Basis ^[7] se ha estandarizado y se incluye en la mayoría de las implementaciones. Proporciona módulos para árboles, matrices y otras estructuras de datos, así como interfaces de entrada/salida y de sistema.

Para el cálculo numérico , existe un módulo Matrix (pero actualmente no funciona), https://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html.

Para gráficos, cairo-sml es una interfaz de código abierto para la biblioteca de gráficos Cairo . Para aprendizaje automático, existe una biblioteca para modelos gráficos.

Las implementaciones de ML estándar incluyen lo siguiente:

Estándar

• HaMLet: un intérprete ML estándar que pretende ser una implementación de referencia precisa y accesible del estándar
• MLton (mlton.org): un compilador optimizador de programas completos que se ajusta estrictamente a la Definición y produce código muy rápido en comparación con otras implementaciones de ML, incluidos los backends para LLVM y C
• Moscow ML: una implementación liviana, basada en el motor de ejecución Caml Light que implementa el lenguaje ML estándar completo, incluidos módulos y gran parte de la biblioteca básica.
• Poly/ML: una implementación completa de ML estándar que produce código rápido y admite hardware multinúcleo (a través de subprocesos de Interfaz de sistema operativo portátil ( POSIX )); su sistema de ejecución realiza una recolección de basura paralela y un intercambio en línea de subestructuras inmutables.
• ML estándar de Nueva Jersey (smlnj.org): un compilador completo, con bibliotecas asociadas, herramientas, un shell interactivo y documentación con soporte para ML concurrente
• SML.NET: un compilador ML estándar para Common Language Runtime con extensiones para vincularse con otro código del marco .NET
• ML Kit Archivado el 7 de enero de 2016 en Wayback Machine : una implementación basada muy de cerca en la Definición, que integra un recolector de elementos no utilizados (que se puede desactivar) y una gestión de memoria basada en regiones con inferencia automática de regiones, con el objetivo de soportar aplicaciones en tiempo real

Derivado

• Alice : un intérprete para ML estándar de la Universidad de Saarland con soporte para programación paralela utilizando futuros , evaluación diferida , computación distribuida a través de llamadas a procedimientos remotos y programación de restricciones
• SML#: una extensión de SML que proporciona polimorfismo de registros e interoperabilidad con el lenguaje C. Es un compilador nativo convencional y su nombre no es una alusión a que se ejecuta en el marco .NET.
• SOSML: una implementación escrita en TypeScript , que admite la mayor parte del lenguaje SML y partes seleccionadas de la biblioteca básica

Investigación

• CakeML es una versión REPL de ML con tiempo de ejecución verificado formalmente y traducción al ensamblador.
• Isabelle (Isabelle/ML Archivado el 30 de agosto de 2020 en Wayback Machine ) integra Poly/ML paralelo en un demostrador de teoremas interactivo, con un IDE sofisticado (basado en jEdit ) para el ML estándar oficial (SML'97), el dialecto Isabelle/ML y el lenguaje de prueba. A partir de Isabelle2016, también hay un depurador de nivel de fuente para ML.
• Poplog implementa una versión de Standard ML, junto con Common Lisp y Prolog , lo que permite la programación en lenguajes mixtos; todos están implementados en POP-11 , que se compila de forma incremental .
• TILT es un compilador de certificación completo para ML estándar que utiliza lenguajes intermedios tipados para optimizar el código y garantizar la corrección, y puede compilar en lenguaje ensamblador tipado .

Todas estas implementaciones son de código abierto y están disponibles de forma gratuita. La mayoría se implementan en Standard ML. Ya no existen implementaciones comerciales; Harlequin , ahora descontinuada, alguna vez produjo un IDE y compilador comercial llamado MLWorks que pasó a manos de Xanalys y luego se convirtió en código abierto después de que Ravenbrook Limited lo adquiriera el 26 de abril de 2013.

Toda la arquitectura empresarial de la Universidad de TI de Copenhague está implementada en alrededor de 100.000 líneas de SML, incluidos registros de personal, nómina, administración y retroalimentación de cursos, gestión de proyectos de estudiantes e interfaces de autoservicio basadas en la web. ^[8]

Los asistentes de prueba HOL4 , Isabelle , LEGO y Twelf están escritos en ML estándar. También lo utilizan los programadores de compiladores y los diseñadores de circuitos integrados , como ARM . ^[9]

• Programación declarativa

Acerca de ML estándar

• Definición revisada
• Proyecto de GitHub de la familia Standard ML Archivado el 20 de febrero de 2020 en Wayback Machine
• ¿Qué es SML?
• ¿Qué es SML '97?

Acerca del sucesor ML

• Sucesor de ML (sML): evolución de ML utilizando ML estándar como punto de partida
• HaMLet en GitHub: implementación de referencia para el ML sucesor

Práctico

• Tutorial básico de introducción
• Ejemplos en el código Rosetta

Académico

• Programación en ML estándar
• Programación en Standard ML '97: un tutorial en línea