ML (lenguaje de programación)

ML (Meta Language) es el metalenguaje desarrollado para el demostrador de teoremas Edinburgh LCF en la década de 1970. Es un lenguaje funcional de tipado estático temprano con inferencia de tipos polimórfica al estilo Hindley-Milner , y otras características como excepciones y variables mutables . ^{[ 1 ]} El diseño de ML en LCF inspiró directamente a la posterior familia ML (en particular Standard ML , Caml y sus derivados) e influyó en el desarrollo posterior de lenguajes funcionales. ^{[ 4 ]}

ML comenzó a desarrollarse por Robin Milner a su llegada a la Universidad de Edimburgo en 1973 con la ayuda de los asistentes de investigación Lockwood Morris y Malcolm Newey, ambos postdoctorandos de Stanford que fueron contratados por Milner. ^{[ 5 ]} Michael Gordon , Christopher Wadsworth y otros estudiantes de posgrado se unieron a la investigación en 1975. ^{[ 4 ]} Históricamente, ML fue concebido para desarrollar tácticas de prueba en el demostrador de teoremas LCF y suceder a la iteración anterior Stanford LCF , tratando de resolver problemas relacionados con la utilización del espacio y la extensibilidad de la prueba. ML actuó como un metalenguaje (de ahí el nombre) y un lenguaje de comandos ( REPL ) para el sistema LCF . PPLAMBDA , un lenguaje que era conceptualmente una combinación del cálculo de predicados de primer orden y el cálculo lambda polimórfico simplemente tipado , fue el lenguaje subyacente en el que se construyeron más directamente los enunciados de teoremas. ^{[ 1 ]}

Mientras se desarrollaba ML, Milner escribió el artículo «Una teoría del polimorfismo de tipos en la programación» en 1978, que exponía las ideas sobre lo que significaba que un programa estuviera bien tipado en el contexto de un sistema de tipos polimórfico (genérico). Utilizó ML como caso práctico de aplicación de los teoremas desarrollados y señaló los desafíos teóricos que surgieron durante el desarrollo y que aún no se habían resuelto. ^{[ 6 ]} El diseño de la primera versión de ML se finalizó y posteriormente se documentó en el libro «Edinburgh LCF» de 1979, escrito por Milner junto con Gordon y Wadsworth. ^{[ 5 ] [ 1 ]}

Después de que Edinburgh LCF se estableció con la publicación del mismo nombre, el interés en el lenguaje creció y varias implementaciones, todas con ligeras alteraciones en el diseño y las características, fueron desarrolladas por varias partes. Luca Cardelli creó Cardelli ML , o VAX ML , que eventualmente se convirtió en un dialecto independiente apto para la computación de propósito general, especificado con el artículo ML under Unix . ^{[ 7 ] [ 4 ]} Gérard Huet en Inria comenzó a portar el código fuente de Stanford Lisp a varios otros dialectos de Lisp en "Project Formel". La adaptación a Franz Lisp fue desarrollada posteriormente por Larry Paulson , cuya versión finalmente se denominó Cambridge LCF . ^{[ 8 ]} Esta versión de LCF fue posteriormente actualizada para usar una versión temprana de Standard ML , y se ha subido a GitHub . ^{[ 9 ]}

Debido a la atención y el entusiasmo que suscitaban en aquel momento ML, LCF y otras tecnologías relacionadas, como el lenguaje de programación contemporáneo Hope , tras el lanzamiento de Edinburgh LCF y otros avances de la época, se convocó una reunión titulada "ML, LCF y Hope" en noviembre de 1982. En dicha reunión se plantearon las preocupaciones sobre la fragmentación tanto del diseño como de la implementación, que conllevaba la duplicación de esfuerzos. Si bien Milner se mostró receptivo al espíritu de experimentación, Bernard Sufrin y Milner mantuvieron más conversaciones y reuniones, en las que Sufrin instó a Milner a unificar el diseño de ML. Estas correspondencias se citaron posteriormente en el segundo borrador de la propuesta de Milner para Standard ML. ^{[ 4 ]}

La inspiración más notable de la sintaxis de ML se remonta a ISWIM , un lenguaje descrito como " cálculo lambda con azúcar sintáctico". ^{[ 4 ]} ML fue diseñado con un sistema de tipos estático robusto que permitía al usuario definir tipos abstractos con polimorfismo paramétrico y se verificaba en tiempo de compilación. ^{[ 1 ]} También contaba con inferencia automática de tipos, lo que le otorgaba a ML la facilidad de uso de lenguajes dinámicos de la época, como Lisp o POP-2, al prescindir de la necesidad de anotaciones de tipo explícitas. ^{[ 4 ]}

Los siguientes ejemplos se derivan en gran medida del LCF de Edimburgo , y ofrecen una visión general de la sintaxis y las características de ML. El #carácter al inicio de una línea indica la entrada del usuario, y las líneas sin él son respuestas del sistema que muestran el valor y su tipo inferido. Cabe destacar que esta sección no pretende ser un conjunto exhaustivo de las características del lenguaje ML, sino un subconjunto para dar una idea general del mismo. Para una definición más rigurosa, consulte el LCF de Edimburgo . ^{[ 1 ]}

Las expresiones se evalúan escribiéndolas seguidas de ;;y un carácter de retorno. El identificador itcontiene el resultado de la última expresión evaluada. Las vinculaciones se introducen con let, y se pueden realizar múltiples vinculaciones simultáneamente uniéndolas con la andpalabra clave, o construyendo pares (que tiene un tipo de producto, explorado en un ejemplo posterior) en el lado derecho, que se compara con patrones a la izquierda:

2+3;;
 5: int 
sea ​​x = ello;;
 x = 5 : int 
sea ​​y = 2*5 y z = 7;;
 y = 10 : int z = 7 : int 
sea ​​x,y,z = y,x,2;;
 x = 10 : int y = 5 : int z = 2 : int

Las funciones se definen con let. La aplicación de funciones tiene mayor precedencia que los operadores matemáticos, por lo que f 3 + 4significa (f 3) + 4. Las funciones definidas con múltiples parámetros se currifican , por lo que pasar un parámetro a la función devolverá una función que aceptará el segundo, y así sucesivamente. Las funciones recursivas requieren letrecpara que el nombre de la función esté dentro del ámbito de su cuerpo. La sintaxis para una función anónima es similar al cálculo lambda, con \para lambda y .separando los argumentos de la expresión:

sumemos xy = x+y;;
 sumar = - : (int -> (int -> int)) 
sumar 3;;
 - : (int -> int) 
es 4;;
 7: int 
letrec fact n = if n = 0 then 1 else n * fact(n-1);;
 hecho = - : (int -> int) 
hecho 4;;
 24: int 
(\x.x+1) 3;;
 4: int

Las listas usan punto y coma entre los elementos. hdy tlson funciones integradas que devuelven la cabeza y la cola; .es cons (anteponer); @es añadir. Las funciones como hdson polimórficas: ML usa variables de tipo genérico ( *, **, etc.) para expresar esto:

sea ​​m = [1;2;3;4];;
 m = [1; 2; 3; 4] : (lista de enteros) 
hd m, tl m;;
 1, [2; 3; 4] : (int # (int lista)) 
0.m @ [5;6];;
 [0; 1; 2; 3; 4; 5; 6] : (lista de enteros) 
HD;;
 - : ((* lista) -> *) 
mapa (\xx*x) [1;2;3;4];;
 [1; 4; 9; 16] : (lista de enteros)

Las variables mutables se declaran con letrefy se actualizan con :=. La looppalabra clave pertenece a la estructura de bucle if-then, que se ejecuta cada vez que iffalla la condición:

sea ​​hecho n =
letref count = n y result = 1
en si count = 0
entonces resultado
bucle count,result := count-1, count*result;;
 hecho = - : (int -> int) 
hecho 4;;
 24: int

Los tokens son del tipo de cadena de ML, delimitados por `; las comillas invertidas dobles crean listas de tokens. Un uso común de los tokens era identificar fallos con failwith, una palabra clave utilizada para generar excepciones con un token explícito, y ?se utiliza para capturarlo:

`este es un token`;;
 `este es un token` : tok 
``esta es una lista de tokens``;;
 [`esto`; `es`; `un`; `token`; `lista`] : (lista de tokens) 
sea ​​la mitad de n =
Si n = 0, entonces falla con `cero`.
de lo contrario, sea m = n/2
en si n = 2*m entonces m sino fallar con `odd`;;
 mitad = - : (int -> int) 
mitad 4;;
 2: int 
mitad 3;;
 EVALUACIÓN FALLIDA impar 
mitad 3 ? 0;;
 0: int

Los tipos abstractos se declaran con abstype, que crea un nuevo tipo y define las funciones que trabajan con él, manteniendo oculta la estructura interna (el tipo concreto a partir del cual se construye). Los tipos abstractos recursivos se declaran con absrectype, que permite que el tipo se utilice en su propia definición. Existe una palabra clave similar lettype, , que se utiliza para alias de tipos más básicos . Aquí hay un tipo abstracto recursivo que define un árbol binario con algunas operaciones básicas:

absrectype (*, **) árbol = * + ** # (*, **) árbol # (*, **) árbol
con tiptree x = abstree(inl x)
y comptree (y, t1, t2) = abstree(inr(y, t1, t2))
y istip t = isl(reptree t)
y tipof t = outl(reptree t) ? failwith `tipof`
y labelof t = fst(outr(reptree t)) ? failwith `labelof`
y sonsof t = snd(outr(reptree t)) ? fallar con `sonsof`;;
 tiptree = - : (* -> (*, **) árbol) comptree = - : ((** # (*, **) árbol # (*, **) árbol) -> (*, **) árbol) istip = - : ((*, **) árbol -> bool) tipof = - : ((*, **) árbol -> *) etiqueta de = - : ((*, **) árbol -> **) hijos de = - : ((*, **) árbol -> ((*, **) árbol # (*, **) árbol))

Dentro de las definiciones de operación (el withbloque), el nombre del tipo puede ir precedido de abspara encapsular valores en el tipo y reppara desencapsular valores. Los caracteres +y #en las definiciones de tipo significan tipos suma (uniones etiquetadas) y tipos producto (tuplas), respectivamente, con #una precedencia mayor.

ML en LCF proporcionó varias funciones auxiliares utilizadas en el ejemplo anterior. Operando en tipos suma +, las funciones inly inrinyectan valores en el lado izquierdo o derecho de un tipo suma. outlextrae de inyecciones izquierdas (falla si se le da una inyección derecha), y outrextrae de inyecciones derechas (falla si se le da una inyección izquierda). Para tipos producto #, las funciones de extracción son fsty snd, que extraen el primer y segundo componente de un par. Los tipos producto se construyen utilizando el operador infijo coma. En el ejemplo de árbol anterior, comptreetoma un único parámetro que es un patrón de par (y, t1, t2), que desestructura el par en sus tres componentes.

• HOL (asistente de pruebas)
• Esperanza (lenguaje de programación)
• Isabelle (ayudante de corrección)
• Nuprl