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 están permitidas bajo circunstancias controladas. Dichos sistemas son útiles para restringir el acceso a los recursos del sistema , como archivos , bloqueos y memoria , al realizar un seguimiento de los cambios de estado que ocurren y evitar estados no válidos. [1]
Han surgido varios sistemas tipo al descartar algunas de las reglas estructurales de intercambio, debilitamiento y contracción:
La explicación de los sistemas de tipos afines se entiende mejor si se reformula como "cada ocurrencia de una variable se usa como máximo una vez".
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 la pila (en contraste con los tipos lineales que se pueden usar para modelar la asignación de memoria basada en el almacenamiento dinámico). [2] Sin la propiedad de intercambio, un objeto solo se puede usar cuando se encuentra 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 manera segura un objeto después de su uso, [3] o diseñe interfaces de software que garanticen que un recurso no se puede usar una vez que se haya cerrado o haya pasado a un estado diferente. [4]
El lenguaje de programación Clean hace uso de tipos únicos (una variante de los tipos lineales) para ayudar a admitir la concurrencia, la entrada/salida y la actualización in situ de matrices. [5]