Sistema de tipo subestructura - Substructural type system
| Sistemas de tipos |
|---|
| Conceptos generales |
| Categorías mayores |
|
| Categorías menores |
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. Estos sistemas son útiles para restringir el acceso a los recursos del sistema , como archivos , bloqueos y memoria, realizando un seguimiento de los cambios de estado que se producen y evitando estados no válidos.
Diferentes sistemas de tipo subestructura
Han surgido varios tipos de sistemas al descartar algunas de las reglas estructurales de intercambio, debilitamiento y contracción:
| Intercambio | Debilitamiento | Contracción | Usar | |
|---|---|---|---|---|
| Ordenado | - | - | - | Exactamente una vez en orden |
| Lineal | Permitido | - | - | Exactamente una vez |
| Afín | Permitido | Permitido | - | Como máximo una vez |
| Pertinente | Permitido | - | Permitido | Al menos una vez |
| Normal | Permitido | Permitido | Permitido | Arbitrariamente |
- Sistemas de tipo ordenado (intercambio de descartes, debilitamiento y contracción): Cada variable se utiliza exactamente una vez en el orden en que se introdujo.
- Sistemas de tipo lineal (permiten el intercambio, pero ni el debilitamiento ni la contracción): Cada variable se usa exactamente una vez.
- Sistemas de tipo afín (permiten el intercambio y el debilitamiento, pero no la contracción): cada variable se utiliza como máximo una vez.
- Sistemas de tipo relevante (permiten el intercambio y la contracción, pero no el debilitamiento): Cada variable se usa al menos una vez.
- Sistemas de tipo normal (permiten el intercambio, el debilitamiento y la contracción): cada variable puede usarse arbitrariamente.
La explicación de los sistemas de tipos afines se comprende mejor si se reformula como "cada aparición de una variable se utiliza como máximo una vez".
Sistema de tipo ordenado
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 pilas (en contraste con los tipos lineales que se pueden usar para modelar la asignación de memoria basada en pilas). 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 da como resultado que cada variable se use exactamente una vez en el orden en que se introdujo.
Sistemas de tipo lineal
Los tipos lineales corresponden a la lógica lineal y garantizan que los objetos se utilicen exactamente una vez, lo que permite que el sistema desasigne de forma segura un objeto después de su uso.
El lenguaje de programación Clean hace uso de tipos de unicidad (una variante de los tipos lineales) para ayudar a admitir la concurrencia, la entrada / salida y la actualización in situ de las matrices.
Los sistemas de tipo lineal permiten referencias pero no alias . Para hacer cumplir esto, una referencia queda fuera de alcance 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 salga del alcance.
Un sistema de tipo lineal es similar a la clase unique_ptr de C ++ , que se comporta como un puntero pero solo se puede mover (es decir, no copiar) en una asignación. Aunque la restricción de linealidad se comprueba en tiempo de compilación , desreferenciar un unique_ptr invalidado provoca un comportamiento indefinido en tiempo de ejecución .
La propiedad de referencia única hace que los sistemas de tipo lineal 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 un funtor diagonal que pueda duplicar estados; de manera similar, desde el punto de vista del combinador , no existe un combinador K que pueda destruir estados. Desde el punto de vista del cálculo lambda , una variable x puede aparecer exactamente una vez en un término.
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 mecanografiado es el lenguaje de las categorías cerradas cartesianas . Más precisamente, se pueden construir functores entre la categoría de sistemas de tipo lineal y la categoría de categorías monoidales simétricas cerradas.
Sistemas de tipo afín
Los tipos afines son una versión de los tipos lineales que permiten descartar (es decir, no usar ) un recurso, correspondiente a la lógica afín . Un recurso afín puede usarse como máximo una vez, mientras que uno lineal debe usarse exactamente una vez.
Sistema de tipos relevantes
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.
Lenguajes de programación
Los siguientes lenguajes de programación admiten tipos lineales o afines:
Ver también
Notas
Referencias
- Walker, David (2002). "Sistemas de tipo subestructura". En Pierce, Benjamin C. (ed.). Temas avanzados en tipos y lenguajes de programación (PDF) . Prensa del MIT. págs. 3-43. ISBN 0-262-16228-8.
