En informática , un tipo único garantiza que un objeto se utilice de forma monohilo , con una única referencia a él como máximo. Si un valor tiene un tipo único, se puede optimizar una función que se le aplique para actualizar el valor en el código del objeto . Estas actualizaciones en el lugar mejoran la eficiencia de los lenguajes funcionales al tiempo que mantienen la transparencia referencial . Los tipos únicos también se pueden utilizar para integrar la programación funcional e imperativa.
La tipificación unívoca se explica mejor con un ejemplo. Considere una función readLineque lee la siguiente línea de texto de un archivo determinado:
La función readLine(File f) devuelve una cadena línea de retorno donde Cadena línea = doImperativeReadLineSystemCall(f) finfinAhora doImperativeReadLineSystemCalllee la siguiente línea del archivo mediante una llamada al sistema a nivel de SO que tiene el efecto secundario de cambiar la posición actual en el archivo. Pero esto viola la transparencia referencial porque al llamarlo varias veces con el mismo argumento se obtendrán resultados diferentes cada vez, ya que la posición actual en el archivo se mueve. Esto, a su vez, viola la transparencia referencial porque llama a .readLinedoImperativeReadLineSystemCall
Sin embargo, al utilizar la tipificación de unicidad, podemos construir una nueva versión readLineque sea 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) devuelve (diferenteF, línea) donde Cadena línea = doImperativeReadLineSystemCall(f) Archivo diferenteF = newFileFromExistingFile(f) finfinLa uniquedeclaración especifica que el tipo de fes único, es decir, que fel invocador de nunca más podrá hacer referencia a él readLine2después de readLine2que retorna, y esta restricción la aplica el sistema de tipos . Y dado que readLine2no retorna fa sí mismo sino a un nuevo objeto de archivo diferente differentF, esto significa que es imposible que readLine2se lo invoque con fcomo argumento nunca más, lo que preserva la transparencia referencial y permite 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 del compilador para el lenguaje de programación Scala que utiliza anotaciones para gestionar 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 hay una distinción: la tipificación lineal real permite que un valor no lineal se convierta a una forma lineal, mientras que aún se conservan múltiples referencias a él. La unicidad garantiza que un valor no tenga otras referencias a él, 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]