Antecedentes

Estoy diseñando un lenguaje, como un proyecto paralelo. Tengo un ensamblador que funciona, un analizador estático y una máquina virtual para ello. Como ya puedo compilar y ejecutar programas no triviales utilizando la infraestructura que he construido, pensé en hacer una presentación en mi universidad.

Durante mi charla, mencioné que la VM proporciona un sistema de tipos, me preguntaron " ¿Para qué es su sistema de tipos? ". Después de responder, la persona que me hizo la pregunta se rió de mí.

Por lo tanto, aunque seguramente perderé reputación por hacer esta pregunta, recurro a los Programadores.

Mi punto de vista

Según tengo entendido, los sistemas de tipos se utilizan para proporcionar una capa adicional de información sobre entidades en un programa, de modo que el tiempo de ejecución, o el compilador, o cualquier otra pieza de maquinaria, sepa qué hacer con las cadenas de bits en las que opera. También ayudan a mantener los contratos: el compilador (o el analizador de código, o el tiempo de ejecución, o cualquier otro programa) puede verificar que en cualquier punto dado el programa opere con los valores que los programadores esperan que opere.

Los tipos también se pueden usar para proporcionar información a esos programadores humanos. Por ejemplo, encuentro esta declaración:

function sqrt(double n) -> double;

más útil que este

sqrt(n)

El primero proporciona mucha información: que el sqrtidentificador es una función, toma un solo doublecomo entrada y produce otro doublecomo salida. Este último le dice que probablemente es una función que toma un solo parámetro.

Mi respuesta

Entonces, después de preguntar "¿Para qué es su sistema de tipos?" Respondí lo siguiente:

El sistema de tipos es dinámico (los tipos se asignan a valores, no a variables que los contienen), pero fuerte sin reglas de coerción sorprendentes (no puede agregar una cadena al entero ya que representan tipos incompatibles, pero puede agregar un entero al número de coma flotante) .

La máquina virtual utiliza el sistema de tipos para garantizar que los operandos para las instrucciones sean válidos; y pueden ser utilizados por los programadores para garantizar que los parámetros pasados ​​a sus funciones sean válidos (es decir, del tipo correcto).
El sistema de tipos admite subtipos y herencia múltiple (ambas funciones están disponibles para los programadores), y los tipos se consideran cuando se usa el despacho dinámico de métodos en objetos: VM usa tipos para verificar por qué función se implementa un mensaje dado para un tipo dado.

La pregunta de seguimiento fue "¿Y cómo se asigna el tipo a un valor?". Así que le expliqué que todos los valores están encuadrados y tienen un puntero que apunta a una estructura de definición de tipo que proporciona información sobre el nombre del tipo, a qué mensajes responde y de qué tipos hereda.

Después de eso, me reí, y mi respuesta fue rechazada con el comentario "Ese no es un sistema de tipos real".

Entonces, si lo que describí no califica como un "sistema de tipos real", ¿qué lo haría? ¿Tenía razón esa persona de que lo que proporciono no puede considerarse un sistema de tipos?

Todo eso parece una buena descripción de lo que proporcionan los sistemas de tipos. Y su implementación suena bastante razonable para lo que está haciendo.

Para algunos idiomas, no necesitará la información de tiempo de ejecución ya que su idioma no realiza el envío de tiempo de ejecución (o lo hace solo a través de vtables u otro mecanismo, por lo que no necesita la información de tipo). Para algunos idiomas, solo tener un símbolo / marcador de posición es suficiente ya que solo le importa la igualdad de tipos, no su nombre o herencia.

Dependiendo de su entorno, la persona puede haber querido más formalismo en su sistema de tipos. Quieren saber qué puedes probar con él, no qué pueden hacer los programadores con él. Desafortunadamente, esto es bastante común en la academia. Aunque los académicos hacen tales cosas porque es bastante fácil tener fallas en su sistema de tipos que permiten que las cosas escapen de la corrección. Es posible que hayan visto uno de estos.

Si tenía más preguntas, Tipos y lenguajes de programación es el libro canónico sobre el tema y puede ayudarlo a aprender algo del rigor que necesitan los académicos, así como parte de la terminología para ayudar a describir las cosas.

Me gusta la respuesta de @ Telastyn especialmente por la referencia al interés académico en el formalismo.

Permítame agregar a la discusión.

¿Qué es un sistema de tipos?

Un sistema de tipos es un mecanismo para definir, detectar y prevenir estados de programa ilegales. Funciona definiendo y aplicando restricciones. Las definiciones de restricciones son tipos y las aplicaciones de restricciones son usos de tipos , por ejemplo, en declaración de variable.

Las definiciones de tipo generalmente admiten operadores de composición (por ejemplo, varias formas de conjunción, como en estructuras, subclases y disyunción, como en enumeraciones, uniones).

Las restricciones, los usos de los tipos, a veces también permiten operadores de composición (por ejemplo, al menos esto, exactamente esto, esto o aquello, siempre que haya algo más).

Si el sistema de tipos está disponible en el idioma y se aplica en tiempo de compilación con el objetivo de poder emitir errores en tiempo de compilación, es un sistema de tipo estático; Esto evita que se compilen muchos programas ilegales y mucho menos que se ejecuten, por lo tanto, impide los estados de programas ilegales.

(Un sistema de tipo estático detiene la ejecución de un programa independientemente de si se sabe (o no se puede decidir) que el programa alcanzará ese código incorrecto del que se queja. Un sistema de tipo estático detecta ciertos tipos de tonterías (violaciones de las restricciones declaradas) y juzga el programa por error antes de que se ejecute).

Si se aplica un sistema de tipos en tiempo de ejecución, es un sistema de tipos dinámico que evita estados de programa ilegales: pero al detener el programa a mitad de ejecución, en lugar de evitar que se ejecute en primer lugar.

Una oferta de sistema de tipos bastante común es proporcionar características estáticas y dinámicas.

Oh hombre, estoy emocionado de tratar de responder esta pregunta lo mejor que puedo. Espero poder ordenar mis pensamientos correctamente.

Como @Doval mencionó y el interrogador señaló (aunque groseramente), realmente no tiene un sistema de tipos. Tiene un sistema de comprobaciones dinámicas que utiliza etiquetas, que en general es mucho más débil y también mucho menos interesante.

La cuestión de "qué es un sistema de tipos" puede ser bastante filosófica, y podríamos llenar un libro con diferentes puntos de vista sobre el tema. Sin embargo, como este es un sitio para programadores, trataré de mantener mi respuesta lo más práctica posible (y realmente, los tipos son extremadamente prácticos en la programación, a pesar de lo que algunos puedan pensar).

Visión de conjunto

Comencemos con una comprensión del asiento de los pantalones de para qué sirve un sistema de tipos, antes de sumergirse en las bases más formales. Un sistema de tipos impone estructura a nuestros programas . Nos dicen cómo podemos conectar varias funciones y expresiones juntas. Sin estructura, los programas son insostenibles y extremadamente complejos, listos para causar daño ante el más mínimo error del programador.

Escribir programas con un sistema tipo es como conducir un cuidado en perfecto estado: los frenos funcionan, las puertas se cierran de manera segura, el motor está engrasado, etc. Escribir programas sin un sistema tipo es como conducir una motocicleta sin casco y con ruedas hechas fuera de espagueti. No tienes absolutamente ningún control sobre tu.

Para fundamentar la discusión, digamos que tenemos un lenguaje con expresión literal num[n]y str[s]que representa el número n y la cadena s, respectivamente, y funciones primitivas plusy concat, con el significado deseado. Claramente, no quieres poder escribir algo como plus "hello" "world"o concat 2 4. Pero, ¿cómo podemos evitar esto? A priori , no existe un método para distinguir el número 2 de la cadena literal "mundo". Lo que nos gustaría decir es que estas expresiones deben usarse en diferentes contextos; Tienen diferentes tipos.

Idiomas y tipos

Retrocedamos un poco: ¿qué es un lenguaje de programación? En general, podemos dividir un lenguaje de programación en dos capas: la sintaxis y la semántica. También se denominan estática y dinámica , respectivamente. Resulta que el sistema de tipos es necesario para mediar la interacción entre estas dos partes.

Sintaxis

Un programa es un árbol. No se deje engañar por las líneas de texto que escribe en una computadora; estas son solo las representaciones legibles por humanos de un programa. El programa en sí es un árbol de sintaxis abstracta . Por ejemplo, en C podríamos escribir:

int square(int x) { 
    return x * x;
 }

Esa es la sintaxis concreta para el programa (fragmento). La representación del árbol es:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

Un lenguaje de programación proporciona una gramática que define los árboles válidos de ese lenguaje (se puede usar sintaxis concreta o abstracta). Esto generalmente se hace usando algo como la notación BNF. Supongo que has hecho esto para el idioma que has creado.

Semántica

Bien, sabemos lo que es un programa, pero es solo una estructura de árbol estática. Presumiblemente, queremos que nuestro programa realmente calcule algo. Necesitamos semántica.

La semántica de los lenguajes de programación es un rico campo de estudio. En términos generales, hay dos enfoques: semántica denotacional y semántica operativa . La semántica de denominación describe un programa al mapearlo en alguna estructura matemática subyacente (por ejemplo, los números naturales, funciones continuas, etc.). eso le da sentido a nuestro programa. La semántica operacional, por el contrario, define un programa al detallar cómo se ejecuta. En mi opinión, la semántica operativa es más intuitiva para los programadores (incluyéndome a mí), así que sigamos con eso.

No explicaré cómo definir una semántica operativa formal (los detalles son un poco complicados), pero básicamente queremos reglas como las siguientes:

1. num[n] es un valor
2. str[s] es un valor
3. Si num[n1]y num[n2]evalúa los enteros n_1$ and $n_2$, thenmás (num [n1], num [n2]) `evalúa el entero $ n_1 + n_2 $.
4. Si str[s1]y se str[s2]evalúa en las cadenas s1 y s2, se concat(str[s1], str[s2])evalúa en la cadena s1s2.

Etc. Las reglas son en la práctica mucho más formales, pero entiendes la esencia. Sin embargo, pronto nos encontramos con un problema. Qué sucede cuando escribimos lo siguiente:

concat(num[5], str[hello])

Hm. Esto es todo un enigma. No hemos definido una regla en ninguna parte sobre cómo concatenar un número con una cadena. Podríamos intentar crear dicha regla, pero intuitivamente sabemos que esta operación no tiene sentido. No queremos que este programa sea válido. Y así nos llevan inexorablemente a los tipos.

Tipos

Un programa es un árbol definido por la gramática de un lenguaje. Los programas reciben significado por las reglas de ejecución. Pero algunos programas no pueden ejecutarse; es decir, algunos programas no tienen sentido . Estos programas están mal escritos. Por lo tanto, la escritura caracteriza programas significativos en un idioma. Si un programa está bien escrito, podemos ejecutarlo.

Demos algunos ejemplos. Nuevamente, al igual que con las reglas de evaluación, presentaré las reglas de mecanografía de manera informal, pero pueden hacerse rigurosas. Aquí hay algunas reglas:

1. Una ficha del formulario num[n]tiene tipo nat.
2. Una ficha del formulario str[s]tiene tipo str.
3. Si expresión e1tiene tipo naty expresión e2tiene tipo nat, entonces la expresión plus(e1, e2)tiene tipo nat.
4. Si la expresión e1tiene tipo stry la expresión e2tiene tipo str, entonces la expresión concat(e1, e2)tiene tipo str.

Por lo tanto, de acuerdo con estas reglas, hay un plus(num[5], num[2])tipo has nat, pero no podemos asignarle un tipo plus(num[5], str["hello"]). Decimos que un programa (o expresión) está bien escrito si podemos asignarle cualquier tipo, y de lo contrario está mal escrito. Un sistema de tipos es válido si se pueden ejecutar todos los programas bien escritos. Haskell es sano; C no lo es.

Conclusión

Hay otras opiniones sobre tipos. Los tipos en cierto sentido corresponden a la lógica intuicionista, y también pueden verse como objetos en la teoría de categorías. Comprender estas conexiones es fascinante, pero no es esencial si uno simplemente quiere escribir o incluso diseñar un lenguaje de programación. Sin embargo, comprender los tipos como una herramienta para controlar las formaciones de programas es esencial para el diseño y desarrollo del lenguaje de programación. Solo he arañado la superficie de qué tipos pueden expresar. Espero que pienses que vale la pena incorporarlo a tu idioma.