Hola a todos!
A pesar de la extravagancia y cierta abstracción del tema considerado hoy, esperamos que pueda diversificar su fin de semana. Al final de la publicación, colocamos tres enlaces del autor, lo que le permite familiarizarse con la escritura dependiente en Idris, F * y JavaScript
A veces parece que los lenguajes de programación no han cambiado mucho desde los años 60. Cuando me cuentan sobre esto, a menudo recuerdo cuántas herramientas y funciones interesantes tenemos ahora a nuestra disposición y cómo simplifican nuestras vidas. De antemano: se trata de depuradores integrados, y pruebas unitarias, y analizadores estáticos, e IDE geniales, así como matrices escritas y mucho más. El desarrollo de los idiomas es un proceso largo y progresivo, y no existen tales "balas de plata" con las cuales el desarrollo de los idiomas cambiaría de una vez por todas.
Hoy quiero contarles sobre una de las últimas etapas de este proceso continuo. La tecnología que se discutirá aún se está estudiando activamente, pero todo indica que pronto se arraigará en los idiomas principales. Y nuestra historia comienza con uno de los conceptos más fundamentales en informática: con los
tipos .
Mundo de tipos
Escribir es una de esas cosas que son tan inseparables de nuestro pensamiento que apenas pensamos en el concepto de tipos como tal. ¿Por qué es 1 un
int , pero si solo pones este valor entre comillas y se convierte en una
string ? ¿Qué es un "tipo" en esencia? Como suele ser el caso en la programación, la respuesta depende de la redacción de la pregunta.
Los tipos son diversos. En algunos sistemas de tipos, existen límites muy claros entre tipos y valores. Entonces, 3, 2 y 1 son valores
integer , pero
integer no es un valor. Esta construcción está "incrustada" en el lenguaje y fundamentalmente diferente del significado. Pero, de hecho, esa diferencia no es necesaria y solo puede limitarnos.
Si libera los tipos y los convierte en otra categoría de valores, se abren una serie de posibilidades sorprendentes. Los valores se pueden almacenar, convertir y pasar a funciones. Por lo tanto, sería posible hacer una función que tome un tipo como parámetro, creando funciones generalizadas: aquellas que pueden funcionar con muchos tipos sin sobrecargas. Puede tener una matriz de valores de un tipo dado, en lugar de hacer una extraña aritmética de puntero y conversión de tipo, como debe hacer en C. También puede recopilar nuevos tipos a medida que se ejecuta el programa y proporcionar características como la deserialización JSON automática. Pero, incluso si trata los tipos como valores, aún no puede hacer todo lo que los tipos pueden hacer con los valores. Entonces, al operar con instancias de usuario, puede, por ejemplo, comparar sus nombres, verificar su edad o identificador, etc.
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
Sin embargo, cuando intenta hacer lo mismo con el tipo de
User , solo puede comparar nombres de tipos y posiblemente nombres de propiedades. Dado que este es un tipo, no una instancia, no puede verificar los valores de sus propiedades.
if typeof(user) == User { print("Well, it's a user. That's all I know") }
¿Qué tan genial sería si tuviéramos una función capaz de recibir solo una lista no vacía de usuarios? ¿O una función que aceptaría una dirección de correo electrónico solo si está registrada en el formato correcto? Para estos fines, necesitaría los tipos "matriz no vacía" o "dirección de correo electrónico". En este caso, es un tipo dependiente del valor, es decir sobre el
tipo dependiente En los idiomas principales, esto no es posible.
Para que se puedan usar los tipos, el compilador debe verificarlos. Si afirma que la variable contiene un entero, sería mejor si no hubiera una
string , de lo contrario el compilador jurará. En principio, esto es bueno, porque no nos permite cortejar. La comprobación de tipos es bastante simple: si una función devuelve un
integer e intentamos devolver
"Marin" , entonces esto es un error.
Sin embargo, con los tipos dependientes, las cosas se vuelven más complicadas. El problema es cuando exactamente el compilador verifica los tipos. ¿Cómo puede asegurarse de que haya exactamente tres valores en la matriz, si el programa aún no se está ejecutando? ¿Cómo asegurarse de que un número entero sea mayor que 3, si aún no está asignado? Hay
magia en esto ... o, en otras palabras,
matemáticas . Si se puede demostrar matemáticamente que el conjunto de números siempre es mayor que 3, entonces el compilador puede verificar esto.
Matemáticas en el estudio!
La inducción matemática se usa para formular evidencia. La inducción nos permite confirmar incondicionalmente la verdad de una declaración. Por ejemplo, queremos demostrar que la siguiente fórmula matemática es válida para cualquier número positivo:
1 + 2 + 3 + ... + x = x * (x + 1) / 2
Hay un número infinito de x posibles, por lo que nos llevaría mucho tiempo verificar todos los números manualmente. Afortunadamente, esto no es necesario. Solo necesitamos probar dos cosas:
- Esta declaración se observa para el primer día. (Generalmente es 0 o 1)
- Si esta afirmación es verdadera para el número
n , entonces será verdadera para el siguiente número n + 1
Dado que la declaración se observa tanto para el primer número como para todos los números siguientes, sabemos que es cierto para todos los números posibles.
Probar esto no es difícil:
1 = 1 * (1 + 1) / 2 1 = 1
Ahora también tenemos que demostrar que la declaración es válida para todos los demás números. Para hacer esto, suponga que funciona para algún número n, y luego asegúrese de que también funcione para n + 1.
Asumiendo que la siguiente expresión es verdadera:
1 + 2 + 3 + ... + n = n * (n + 1) / 2
Compruébalo para
n + 1 :
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
Por lo tanto, podemos reemplazar
"(1 + 2 + 3 + ... + n)" igualdad anterior:
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
y simplificar a
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
Como ambas partes de la expresión son iguales, nos aseguramos de que esta afirmación sea verdadera. Esta es una de las formas en que puede verificar la verdad de las declaraciones sin calcular manualmente cada caso, y es sobre la base de este principio que funcionan los tipos dependientes. Escribe una declaración matemática para asegurarse de que la tesis de tipo sea verdadera.
La belleza de este enfoque radica en el hecho de que cualquier prueba matemática puede emitirse en forma de un programa de computadora, ¡y esto es lo que necesitamos!
De vuelta a la programación
Entonces, descubrimos que algunas cosas pueden probarse primero y luego pasar a valores específicos. Para hacer esto en un lenguaje de programación, necesita una forma de expresar estas declaraciones en código que se escribirá en el sistema de tipos en sí, es decir, el sistema de tipos debe mejorarse.
Considera un ejemplo. Aquí tenemos una función append que toma dos matrices y las combina. Como regla general, la firma de dicha función se verá así:
append: (arr1: Array, arr2: Array) -> Array
Sin embargo, con solo mirar la firma, no podemos estar seguros de la implementación correcta. El hecho de que la función devuelva una matriz no significa que haya hecho algo. Una forma de verificar el resultado es asegurarse de que la longitud de la matriz resultante sea igual a la suma de las longitudes de las matrices de parámetros.
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
Pero, ¿por qué verificar esto en tiempo de ejecución si puede crear una restricción que se verificará en tiempo de compilación?
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
Declaramos que
append es una función que toma dos argumentos de
Array y devuelve un nuevo argumento de
Array , que llamamos
newArray . Solo que esta vez agregamos una advertencia de que la longitud de la nueva matriz debe ser igual a la suma de las longitudes de todos los argumentos de la función. La declaración que teníamos arriba en tiempo de ejecución se convierte a tipo en tiempo de compilación.
El código anterior se refiere al mundo de los tipos, no a los valores, es decir, el signo
== indica una comparación de la
length tipo devuelto, y no su valor. Para que dicho mecanismo funcione, la longitud del tipo devuelto debe proporcionarnos información sobre el número real.
Para garantizar el funcionamiento de dicho mecanismo, debe asegurarse de que cada número sea de un tipo diferente. Un tipo puede contener solo un valor: 1. Lo mismo se aplica a Dos, Tres y todos los demás números. Naturalmente, tal trabajo es muy agotador, pero es para ese trabajo que tenemos programación. Puede escribir un compilador que lo haga por nosotros.
Una vez hecho esto, puede crear tipos separados para matrices que contienen 1, 2, 3 y un número diferente de elementos.
ArrayOfOne ,
ArrayOfTwo , etc.
Por lo tanto, puede definir la función de longitud, que tomará uno de los tipos de matriz anteriores y tendrá un tipo de retorno dependiente de
One para
ArrayOfOne ,
Two para
ArrayOfTwo , etc. para cada número
Ahora que tenemos un tipo separado para cualquier longitud específica de la matriz, podemos verificar (en tiempo de compilación) que ambas matrices tienen la misma longitud. Para hacer esto, compare sus tipos. Y dado que los tipos tienen los mismos valores que cualquier otro, puede asignarles operaciones. Puede determinar la adición de dos tipos específicos especificando que la suma de
ArrayOfOne y
ArrayOfTwo es igual a
ArrayOfThree .
Esa es toda la información que el compilador necesita para asegurarse de que el código que escribió sea correcto.
Supongamos que queremos crear una variable de tipo
ArrayOfThree :
result: ArrayOfThree = append([1], [2, 3])
El compilador puede determinar que [1] solo tiene un valor, por lo que puede asignar el tipo
ArrayOfOne . También puede asignar
ArrayOfTwo a [2, 3].
El compilador sabe que el tipo de resultado debe ser igual a la suma de los tipos del primer y segundo argumento. También sabe que ArrayOfOne + ArrayOfTwo es igual a ArrayOfThree, es decir, sabe que toda la expresión en el lado derecho de la identidad es del tipo ArrayOfThree. Coincide con la expresión de la izquierda y el compilador está satisfecho.
Si escribimos lo siguiente:
result: ArrayOfTwo = append([1], [2, 3])
entonces el compilador estaría completamente insatisfecho, ya que sabría que el tipo es incorrecto.
La escritura dependiente es genial
En este caso, una gran cantidad de errores es simplemente imposible de permitir. Con la escritura dependiente, se pueden evitar errores por unidad, accesos a índices de matriz inexistentes, excepciones de puntero nulo, bucles infinitos y código roto.
Usando tipos dependientes, puede expresar casi cualquier cosa. La función factorial solo aceptará números naturales, la función de
login no aceptará líneas vacías, la función
removeLast solo aceptará matrices no vacías. Además, todo esto se verifica antes de iniciar el programa.
El problema con las comprobaciones de tiempo de ejecución es que fallan si el programa ya se está ejecutando. Esto es normal si el programa lo ejecuta solo usted, pero no el usuario. Los tipos dependientes le permiten llevar tales controles al nivel de tipos, por lo que la falla de este tipo durante la ejecución del programa se vuelve imposible.
Creo que la escritura dependiente es el futuro de los lenguajes de programación convencionales, ¡y no puedo esperar para esperarlo!
→
Idris→
F *→
Agregar tipos dependientes a JavaScript