En informática , un tipo único garantiza que un objeto se utilice en un solo subproceso , con como máximo una única referencia al mismo. Si un valor tiene un tipo único, una función que se le aplica se puede optimizar para actualizar el valor in situ en el código objeto . Estas actualizaciones locales mejoran la eficiencia de los lenguajes funcionales al tiempo que mantienen la transparencia referencial . También se pueden utilizar tipos únicos para integrar la programación funcional e imperativa.
La tipificación de unicidad se explica mejor con un ejemplo. Considere una función readLineque lee la siguiente línea de texto de un archivo determinado:
función readLine(Archivo f) devuelve Cadena línea de retorno donde Línea de cadena = doImperativeReadLineSystemCall(f) finfinAhora doImperativeReadLineSystemCalllee la siguiente línea del archivo mediante 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 llamarlo varias veces con el mismo argumento arrojará resultados diferentes cada vez que se mueva la posición actual en el archivo. Esto a su vez hace violar la transparencia referencial porque llama .readLinedoImperativeReadLineSystemCall
Sin embargo, usando tipos de unicidad, podemos construir una nueva versión readLineque sea referencialmente transparente aunque esté construida sobre una función que no sea referencialmente transparente:
función readLine2 (archivo único f) devuelve (archivo único, cadena) retorno (diferente F, línea) donde Línea de cadena = doImperativeReadLineSystemCall(f) Archivo diferenteF = newFileFromExistingFile(f) finfinLa uniquedeclaración especifica que el tipo de fes único; es decir, fla persona que llama nunca puede volver a hacer referencia a él readLine2después de readLine2las devoluciones, y esta restricción la aplica el sistema de tipos . Y dado que readLine2no devuelve fsí mismo sino un objeto de archivo nuevo y diferente differentF, esto significa que es imposible volver readLine2a llamarlo fcomo argumento, preservando así la transparencia referencial y permitiendo que se produzcan efectos secundarios.
Los tipos de unicidad se implementan en lenguajes de programación funcionales como Clean , Mercury , SAC e Idris . A veces se utilizan para realizar operaciones de E/S en lenguajes funcionales en lugar de mónadas .
Se ha desarrollado una extensión de compilación 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 a menudo se usan indistintamente, pero de hecho existe una distinción: el tipo lineal real permite encasillar un valor no lineal en una forma lineal, sin dejar de conservarlo. múltiples referencias al mismo. La unicidad garantiza que un valor no tiene otras referencias a él, mientras que la linealidad garantiza que no se pueden hacer más referencias a un valor. [2]
La linealidad y la unicidad pueden verse como particularmente distintas en relación con las modalidades de no linealidad y no unicidad, pero luego también pueden unificarse en un solo sistema de tipos. [3]