En informática , un sistema de efectos es un sistema formal que describe los efectos computacionales de los programas informáticos, como los efectos secundarios . Se puede usar un sistema de efectos para proporcionar una verificación en tiempo de compilación de los posibles efectos del programa.
El sistema de efectos amplía la noción de tipo para que tenga un componente de "efecto", que comprende un tipo de efecto y una región . El tipo de efecto describe lo que se está haciendo y la región describe con qué (parámetros) se está haciendo.
Un sistema de efectos es típicamente una extensión de un sistema de tipos . En este caso, a veces se utiliza el término " sistema de tipos y efectos ". A menudo, un tipo de valor se indica junto con su efecto como tipo. efecto , donde tanto el componente de tipo como el componente de efecto mencionan ciertas regiones (por ejemplo, un tipo de celda de memoria mutable está parametrizado por la etiqueta de la región de memoria en la que reside la celda). Los términos " efecto algebraico " se derivan del sistema de tipos.
Los sistemas de efectos pueden usarse para probar la pureza externa de ciertas definiciones internamente impuras: por ejemplo, si una función asigna y modifica internamente una región de memoria, pero el tipo de función no menciona la región, entonces el efecto correspondiente puede borrarse de la efecto de la función.
Ejemplos de
Algunos ejemplos de los comportamientos que pueden describirse mediante sistemas de efectos incluyen:
- Lectura, escritura o asignación de memoria: el tipo de efecto es de lectura , escritura , asignación o libre , y la región es el punto del programa donde se realizó la asignación (es decir, a cada punto del programa donde se realiza la asignación se le asigna una etiqueta única y una región la información se propaga estáticamente a lo largo del flujo de datos). La mayoría de las funciones que trabajan con la memoria serán polimórficas en la variable de región: por ejemplo, una función que intercambie dos ubicaciones en la memoria tendrá tipo
forall r1 r2, unit ! {read r1, read r2, write r1, write r2}
. - Trabajar con recursos, como archivos: por ejemplo, el tipo de efecto puede ser abrir , leer y cerrar , y nuevamente, la región es el punto del programa donde se abre el recurso.
- Transferencias de control con continuaciones y saltos largos: el tipo de efecto puede ser goto (es decir, el fragmento de código puede realizar un salto) y venir de (es decir, el fragmento de código puede ser el objetivo de un salto), y la región denota el punto del programa desde el cual o hacia el cual se puede realizar el salto.
Desde el punto de vista de un programador, los efectos son útiles ya que permiten separar la implementación ( cómo ) de acciones específicas de la especificación de qué acciones realizar. Por ejemplo, un efecto de preguntar nombre puede leerse desde la consola, abrir una ventana o simplemente devolver un valor predeterminado. El flujo de control puede describirse como una combinación de rendimiento (en el sentido de que la ejecución continúa) y lanzamiento (en el sentido de que un efecto no controlado se propaga hacia abajo hasta que se maneja). [1]
Implementaciones
- Haskell tiene varios paquetes que permiten la codificación de efectos. [2]
- Las excepciones marcadas de Java son un ejemplo de un sistema de efectos: el tipo de efecto es lanzamientos y la región es el tipo de excepción que se lanza.
- Koka es un lenguaje de programación con efectos diseñados en mente. [3]
- ECMAScript tiene una propuesta (y un pase de Babel) que implementa efectos algebraicos. [4]
Referencias
Capítulos de libros de texto
- Hankin, Chris; Nielson, Flemming; Nielson, Hanne Riis (1999). Principios del análisis de programas . Berlín: Springer. ISBN 978-3-540-65410-0.
- Gifford, David; Turbak, Franklyn A .; Sheldon, Mark A. (2008). "dieciséis". Conceptos de diseño en lenguajes de programación . Cambridge, Mass: MIT Press. ISBN 978-0-262-20175-9.
Documentos de descripción general
- Nielson, Flemming; Nielson, Hanne Riis (1999). Sistemas de tipos y efectos . Diseño correcto del sistema: conocimientos y avances recientes . Apuntes de conferencias en Ciencias de la Computación . 1710 . Springer-Verlag. págs. 114-136 . doi : 10.1007 / 3-540-48092-7_6 . ISBN 978-3-540-66624-0.
Otras lecturas
- Marino, Daniel; Millstein, Todd (2008). Un sistema genérico de tipos y efectos (PDF) . Actas del IV Taller Internacional sobre Tipos en Diseño e Implementación de Lenguaje . ACM . pag. 39. CiteSeerX 10.1.1.157.8373 . doi : 10.1145 / 1481861.1481868 . ISBN 9781605584201.
- Lucassen, John M .; Gifford, David K. (1988). Sistemas de efectos polimórficos . Actas del 15º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM . págs. 47–57. CiteSeerX 10.1.1.73.4916 . doi : 10.1145 / 73560.73564 . ISBN 978-0897912525.
- ^ Abramov, Dan. "Efectos algebraicos para el resto de nosotros" . exagerado.io .
- ^ Vera, Josh (18 de abril de 2020). "joshvera / freemonad-benchmark" . GitHub .
Un punto de referencia que compara el rendimiento de diferentes implementaciones de mónadas libres.
- ^ "El Manual de Koka" . koka-lang.github.io .
- ^ Macabeus, Bruno (16 de septiembre de 2020). "macabeus / js-propuesta-efectos-algebraicos: 📐 Que haya efectos algebraicos en JS" . GitHub .