Tipo de singularidad

En informática , un tipo único garantiza que un objeto se utilice de forma monohilo , con una sola referencia como máximo. Si un valor tiene un tipo único, una función aplicada a él puede optimizarse para actualizar el valor directamente en el código objeto . Estas actualizaciones directas mejoran la eficiencia de los lenguajes funcionales , manteniendo la transparencia referencial . Los tipos únicos también pueden utilizarse para integrar la programación funcional e imperativa.

La tipificación de unicidad se explica mejor con un ejemplo. Consideremos una función readLineque lee la siguiente línea de texto de un archivo determinado:

La función readLine(File f) devuelve una cadena de caracteres. línea de retorno donde Cadena línea = doImperativeReadLineSystemCall(f) fin fin 

Ahora doImperativeReadLineSystemCalllee la siguiente línea del archivo usando una llamada al sistema a nivel del sistema operativo que tiene el efecto secundario de cambiar la posición actual en el archivo. Pero esto viola la transparencia referencial porque llamarla varias veces con el mismo argumento devolverá resultados diferentes cada vez a medida que se mueve la posición actual en el archivo. Esto a su vez hace que viole la transparencia referencial porque llama a .readLinedoImperativeReadLineSystemCall

Sin embargo, utilizando la tipificación de unicidad, podemos construir una nueva versión que readLinesea referencialmente transparente aunque esté construida sobre una función que no sea referencialmente transparente:

La función readLine2(archivo único f) devuelve (archivo único, cadena). devolver (diferenteF, línea) donde Cadena línea = doImperativeReadLineSystemCall(f) Archivo diferenteF = nuevoArchivoDesdeArchivoExistente(f) fin fin 

La uniquedeclaración especifica que el tipo de fes único; es decir, que fnunca más podrá ser referenciado por quien llama a readLine2después de readLine2que regrese, y esta restricción es impuesta por el sistema de tipos . Y dado que readLine2no devuelve fa sí mismo, sino un nuevo objeto de archivo diferente differentF, esto significa que es imposible que readLine2se vuelva a llamar con fcomo argumento, preservando así la transparencia referencial al tiempo que se permiten efectos secundarios.

Los tipos de unicidad se implementan en lenguajes de programación funcional como Clean , Mercury , SAC e Idris . En ocasiones, se utilizan para realizar operaciones de entrada/salida en lenguajes funcionales en lugar de mónadas .

Se ha desarrollado una extensión de compilador para el lenguaje de programación Scala que utiliza anotaciones para manejar la unicidad en el contexto del paso de mensajes entre actores. ^{[ 1 ]}

Un tipo único es muy similar a un tipo lineal , hasta el punto de que los términos se usan a menudo indistintamente, pero de hecho existe una distinción: la tipificación lineal real permite convertir un valor no lineal a una forma lineal, manteniendo al mismo tiempo múltiples referencias al mismo. La unicidad garantiza que un valor no tenga otras referencias, mientras que la linealidad garantiza que no se puedan hacer más referencias a un valor. ^{[ 2 ]}

La linealidad y la unicidad pueden considerarse particularmente distintas en relación con las modalidades de no linealidad y no unicidad, pero también pueden unificarse en un único sistema de tipos. ^{[ 3 ]}

• Tipo lineal
• Lógica lineal

• Bibliografía sobre lógica lineal
• Tipografía única simplificada