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 fino 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 * xfun 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 )) finEl 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.0Cualquier 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 genera 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 | _ => verdaderoSi 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 xsUna 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 finCuando 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 finEl 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 de 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 finEsta 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 )) finEsta 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 finestructura 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 ) endOrdenació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 ) xsQuicksort 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 | BoolTydiversión unificar ( IntTy , IntTy ) = IntTy | unificar ( BoolTy , BoolTy ) = BoolTy | unificar (_, _) = generar TyErrtipo de datos exp = Verdadero | Falso | Int de int | No de exp | Suma de exp * exp | Si de exp * exp * expfun 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 => NINGUNOEjemplo 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 -> realEl 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 -> realEl 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
- d' ( fn x => x * x * x - x - 1.0 ) 3.0 ; val it = 25.9999996644 : realLa 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
Derivado
Investigación
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]
Acerca de ML estándar
Acerca del sucesor ML
Práctico
Académico