Sistema de tipo subestructural

Los sistemas de tipos subestructurales son una familia de sistemas de tipos análogos a las lógicas subestructurales donde una o más de las reglas estructurales están ausentes o solo se permiten bajo circunstancias controladas. Dichos sistemas pueden restringir el acceso a los recursos del sistema , como archivos , bloqueos y memoria , al realizar un seguimiento de los cambios de estado y prohibir los estados no válidos. ^{[1] : 4}

Han surgido varios sistemas tipo al descartar algunas de las reglas estructurales de intercambio, debilitamiento y contracción:

• Sistemas de tipos ordenados (descarte, intercambio, debilitamiento y contracción): cada variable se utiliza exactamente una vez en el orden en que fue introducida.
• Sistemas de tipo lineal (permiten intercambio, pero ni debilitamiento ni contracción): Cada variable se utiliza exactamente una vez.
• Sistemas de tipo afín (permiten intercambio y debilitamiento, pero no contracción): Cada variable se utiliza como máximo una vez.
• Sistemas de tipos relevantes (permiten intercambio y contracción, pero no debilitamiento): Cada variable se utiliza al menos una vez.
• Sistemas de tipo normal (permiten intercambio, debilitamiento y contracción): Cada variable puede ser utilizada arbitrariamente.

La explicación de los sistemas de tipos afines se entiende mejor si se reformula como “cada aparición de una variable se utiliza como máximo una vez”.

Los tipos ordenados corresponden a una lógica no conmutativa en la que se descartan el intercambio, la contracción y el debilitamiento. Esto se puede utilizar para modelar la asignación de memoria basada en la pila (en contraste con los tipos lineales que se pueden utilizar para modelar la asignación de memoria basada en el montón ). ^{[1] : 30–31} Sin la propiedad de intercambio, un objeto solo se puede utilizar cuando está en la parte superior de la pila modelada, después de lo cual se extrae, lo que da como resultado que cada variable se use exactamente una vez en el orden en que se introdujo.

Los tipos lineales corresponden a la lógica lineal y garantizan que los objetos se utilicen exactamente una vez. Esto permite que el sistema desasigne de forma segura un objeto después de su uso, ^{[1] : 6} o que diseñe interfaces de software que garanticen que un recurso no se pueda utilizar una vez que se haya cerrado o haya pasado a un estado diferente. ^[2]

El lenguaje de programación Clean utiliza tipos únicos (una variante de los tipos lineales) para ayudar a soportar la concurrencia, la entrada/salida y la actualización en el lugar de matrices . ^{[1] : 43}

Los sistemas de tipos lineales permiten referencias, pero no alias . Para hacer cumplir esto, una referencia queda fuera del ámbito después de aparecer en el lado derecho de una asignación , lo que garantiza que solo exista una referencia a cualquier objeto a la vez. Tenga en cuenta que pasar una referencia como argumento a una función es una forma de asignación, ya que al parámetro de la función se le asignará el valor dentro de la función y, por lo tanto, dicho uso de una referencia también hace que quede fuera del ámbito.

La propiedad de referencia única hace que los sistemas de tipos lineales sean adecuados como lenguajes de programación para la computación cuántica , ya que refleja el teorema de no clonación de estados cuánticos. Desde el punto de vista de la teoría de categorías , la no clonación es una afirmación de que no existe ningún funtor diagonal que pueda duplicar estados; de manera similar, desde el punto de vista de la lógica combinatoria , no existe ningún K-combinador que pueda destruir estados. Desde el punto de vista del cálculo lambda , una variable xpuede aparecer exactamente una vez en un término. ^[3]

Los sistemas de tipos lineales son el lenguaje interno de las categorías monoidales simétricas cerradas , de la misma manera que el cálculo lambda de tipos simples es el lenguaje de las categorías cartesianas cerradas . Más precisamente, se pueden construir funtores entre la categoría de sistemas de tipos lineales y la categoría de categorías monoidales simétricas cerradas. ^[4]

Los tipos afines son una versión de los tipos lineales que permiten descartar (es decir, no utilizar ) un recurso, lo que corresponde a la lógica afín . Un recurso afín se puede utilizar como máximo una vez, mientras que uno lineal se debe utilizar exactamente una vez.

Los tipos relevantes corresponden a una lógica relevante que permite el intercambio y la contracción, pero no el debilitamiento, lo que se traduce en que cada variable se utiliza al menos una vez.

La nomenclatura que ofrecen los sistemas de tipos subestructurales es útil para caracterizar los aspectos de gestión de recursos de un lenguaje. La gestión de recursos es el aspecto de la seguridad del lenguaje que se ocupa de garantizar que cada recurso asignado se desasigne exactamente una vez. Por lo tanto, la interpretación de recursos solo se ocupa de los usos que transfieren la propiedad ( movimiento , donde la propiedad es la responsabilidad de liberar el recurso).

Los usos que no transfieren propiedad ( préstamos ) no están dentro del alcance de esta interpretación, pero la semántica de duración de vida restringe aún más estos usos a entre la asignación y la desasignación.

Según la interpretación de recursos, un tipo afín no se puede gastar más de una vez.

A modo de ejemplo, la misma variante de la máquina expendedora de Hoare se puede expresar en inglés, lógica y en Rust :

fn  buy_candy ( _ : Moneda )  -> Caramelo { Caramelo {} } fn buy_drink ( _ : Moneda ) -> Bebida { Bebida {} }        

Lo que significa que Coin sea un tipo afín en este ejemplo (que lo es a menos que implemente el rasgo Copy ) es que intentar gastar la misma moneda dos veces es un programa no válido que el compilador tiene derecho a rechazar:

let coin = Coin {}; let candy = buy_candy ( coin ); // El tiempo de vida de la variable coin termina aquí. let drink = buy_drink ( coin ); // Error de compilación: Uso de una variable movida que no posee el rasgo Copiar.           

En otras palabras, un sistema de tipos afines puede expresar el patrón typestate : las funciones pueden consumir y devolver un objeto envuelto en diferentes tipos, actuando como transiciones de estado en una máquina de estados que almacena su estado como un tipo en el contexto del llamador: un typestate . Una API puede aprovechar esto para hacer cumplir estáticamente que sus funciones se llamen en un orden correcto.

Lo que esto no significa, sin embargo, es que no se pueda utilizar una variable sin agotarla:

// Esta función simplemente toma prestada una moneda: el ampersand significa tomar prestada. fn  validar ( _ : & Moneda )  -> Resultado < (), () > { Ok (()) }    // La misma variable moneda se puede usar infinitas veces // siempre que no se mueva. let coin = Coin {}; loop { validar ( & coin ) ? ; }     

Lo que Rust no puede expresar es un tipo de moneda que no pueda salir de su alcance; eso requeriría un tipo lineal.

Según la interpretación de recursos, un tipo lineal no solo se puede mover, como un tipo afín, sino que se debe mover (salir del ámbito es un programa no válido).

{ // Debe transmitirse, no descartarse. let token = HotPotato {};      // Supongamos que no todas las ramas lo eliminan: if ( ! queue . is_full ()) { queue . push ( token ); }      // Error de compilación: Se mantiene un objeto que no se puede eliminar cuando finaliza el alcance. }

Una de las ventajas de los tipos lineales es que los destructores se convierten en funciones regulares que pueden tomar argumentos, pueden fallar, etc. ^[5] Esto puede, por ejemplo, evitar la necesidad de mantener un estado que solo se utiliza para la destrucción. Una ventaja general de pasar dependencias de funciones explícitamente es que el orden de las llamadas de función (orden de destrucción) se vuelve estáticamente verificable en términos de la duración de los argumentos. En comparación con las referencias internas, esto no requiere anotaciones de duración como en Rust.

Al igual que con la gestión manual de recursos, un problema práctico es que cualquier retorno temprano , como es típico en el manejo de errores, debe lograr la misma limpieza. Esto se vuelve pedante en lenguajes que tienen desenrollado de pila , donde cada llamada de función es un retorno temprano potencial. Sin embargo, como una analogía cercana, la semántica de las llamadas de destructor insertadas implícitamente se puede restaurar con llamadas de función diferidas. ^[6]

Según la interpretación de recursos, un tipo normal no restringe la cantidad de veces que se puede mover una variable. C++ (específicamente, la semántica de movimiento no destructivo) cae en esta categoría.

auto moneda = std :: unique_ptr < Moneda > (); auto caramelo = comprar_caramelo ( std :: mover ( moneda )); auto bebida = comprar_bebida ( std :: mover ( moneda )); // Esto es C++ válido.          

Los siguientes lenguajes de programación admiten tipos lineales o afines ^{[ cita requerida ]} :

• Sistema de efectos
• Lógica lineal
• Lógica afín