Sistema de tipos subestructurales

Los tipos ordenados corresponden a la lógica no conmutativa donde se descartan el intercambio, la contracción y el debilitamiento. Esto se puede usar para modelar la asignación de memoria basada en pila (en contraste con los tipos lineales que se pueden usar para modelar la asignación de memoria basada en montón ). ^{[ 1 ] : 30–31} Sin la propiedad de intercambio, un objeto solo se puede usar cuando está en la parte superior de la pila modelada, después de lo cual se extrae, lo que resulta en 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 aseguran que los objetos se utilicen exactamente una vez. Esto permite que el sistema libere 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 de unicidad (una variante de los tipos lineales) para ayudar a soportar la concurrencia, la entrada/salida y la actualización in situ de matrices . ^{[ 1 ] : 43}

Los sistemas de tipos lineales permiten referencias , pero no alias . Para garantizar esto, una referencia queda fuera de ámbito tras aparecer en el lado derecho de una asignación , asegurando así que solo exista una referencia a cualquier objeto a la vez. Cabe destacar que pasar una referencia como argumento a una función es una forma de asignación, ya que el parámetro de la función recibirá el valor dentro de la misma; por lo tanto, dicho uso de una referencia también provoca que quede fuera de á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 los 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 functor 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 forma muy similar a como el cálculo lambda simplemente tipado es el lenguaje de las categorías cartesianas cerradas . Más precisamente, se pueden construir functores 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 permite descartar (es decir, no usar ) un recurso, lo que corresponde a la lógica afín . Un recurso afín se puede usar como máximo una vez, mientras que uno lineal debe usarse exactamente una vez.

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

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

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

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

let coin = Coin {}; let candy = buy_candy ( coin ); // La vida útil 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 Copy.

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 garantizar estáticamente que sus funciones se llamen en el orden correcto.

Sin embargo, esto no significa que una variable no pueda utilizarse sin consumirse:

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

Lo que Rust no puede expresar es un tipo de moneda que no pueda salirse del ámbito; para eso se necesitaría un tipo lineal.

Según la interpretación de recursos, un tipo lineal no solo puede moverse, como un tipo afín, sino que debe moverse; salir del ámbito de aplicación constituye un programa inválido.

{ // Debe transmitirse, no descartarse. let token = HotPotato {};// Supongamos que no todas las ramas lo eliminan: si ! cola . está_llena () { cola . empujar ( token ); }// Error de compilación: Se está reteniendo un objeto que no se puede soltar cuando finaliza el ámbito. }

Una ventaja de los tipos lineales es que los destructores se convierten en funciones regulares que pueden aceptar argumentos, 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 explícitamente las dependencias de las funciones es que el orden de las llamadas a funciones (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 anticipado , 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 a función es un retorno anticipado potencial. Sin embargo, como analogía cercana, la semántica de las llamadas a destructores insertadas implícitamente se puede restaurar con llamadas a funciones 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) entra en esta categoría.

auto coin = std :: unique_ptr <Coin> ( ); auto candy = buy_candy ( std :: move ( coin ) ); auto drink = buy_drink ( std :: move ( coin )); // Esto es C++ válido.