Sistema de efectos

Sistema que describe los efectos computacionales de programas informáticos.

En informática , un sistema de efectos es un sistema formal que describe los efectos computacionales de programas informáticos, como los efectos secundarios . Se puede utilizar 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 suele ser una extensión de un sistema de tipos . En este caso se utiliza a veces el término " sistema de tipos y efectos ". A menudo, un tipo de valor se indica junto con su efecto como tipo. effect , 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). El término "efecto algebraico" se deriva 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 la memoria, pero el tipo de función no menciona la región, entonces el efecto correspondiente puede borrarse de la memoria. efecto de la función. ^[1]

Ejemplos

Algunos ejemplos de comportamientos que pueden describirse mediante sistemas de efectos incluyen:

• Lectura, escritura o asignación de memoria: el tipo de efecto es lectura , escritura , asignación o liberación , 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 memoria en realidad serán polimórficas en la variable de región: por ejemplo, una función que intercambia 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 ir a (es decir, el fragmento de código puede realizar un salto) y venir desde (es decir, el fragmento de código puede ser el objetivo de un salto), y la región denota el punto del programa desde 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 pregunta de nombre puede leerse desde la consola, abrir una ventana o simplemente devolver un valor predeterminado. El flujo de control se puede describir 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 controla). ^[2]

Implementaciones

Característica principal

• Koka es un lenguaje de programación funcional de tipo estático con controladores de efectos algebraicos como característica principal. ^[3]
• Eff es un lenguaje de programación funcional de tipo estático centrado en controladores de efectos algebraicos. ^[4]
• Unison es un lenguaje de programación funcional de tipo estático con controladores de efectos algebraicos (llamados "habilidades" en el lenguaje) como parte central del sistema de tipos. ^[5]
• Effekt es un lenguaje de investigación centrado en manejadores de efectos y efectos polimórficos. ^[6]

Apoyo total

• Haskell es un lenguaje de programación funcional de tipo estático con varios paquetes que permiten la codificación de efectos. ^[7] Sin embargo, Haskell generalmente se centra más en las mónadas .
• OCaml 5.0 introdujo soporte para primitivas de manejo de efectos experimentales, ^[8] con planes para introducir una sintaxis adecuada de alto nivel en el futuro.

Soporte Parcial y Prototipos

• Scala 3.1 es un lenguaje de programación orientado a objetos , funcional y de tipo estático con soporte experimental para efectos que se limita a excepciones , en forma de CanThrowcapacidad. ^[9]
• Java es un lenguaje de programación orientado a objetos y de tipo estático; sus excepciones marcadas son un ejemplo relativamente limitado de un sistema de efectos. Solo throwsestá disponible un tipo de efecto, no hay forma de reanudar con un valor y no se pueden usar con funciones (solo métodos) a menos que la función implemente un archivo personalizado @FunctionalInterface. ^[10]
• JavaScript es un lenguaje tipado dinámicamente , tiene una propuesta que implementa efectos algebraicos. ^[11]

Referencias

1. Albin., Turbak, Franklyn (2010). Conceptos de diseño en lenguajes de programación. Aprendizaje de PHI. ISBN 978-81-203-3996-5. OCLC  1261053520.{{cite book}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )
2. Abramov, Dan. "Efectos algebraicos para el resto de nosotros". exagerado.io .
3. "El Manual Koka". koka-lang.github.io .
4. Pretnar, Matija (7 de diciembre de 2021), efectivo , consultado el 11 de diciembre de 2021
5. "El lenguaje del unísono". www.unisonweb.org . Consultado el 7 de diciembre de 2021 .
6. El equipo de investigación de Effekt. "Lenguaje Effectt: conceptos y características". Lenguaje de efectos . Consultado el 13 de junio de 2023 .
7. 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 gratuitas.
8. "OCaml - Extensiones de idioma". v2.ocaml.org . Consultado el 13 de junio de 2023 .
9. "Habilidades de CanThrow". Documentación de Scala . Consultado el 7 de diciembre de 2021 .
10. "¿Función Lambda de Java 8 que genera una excepción?". Desbordamiento de pila . Consultado el 25 de diciembre de 2021 .
11. Macabeo, Bruno (16 de septiembre de 2020). "macabeus/js-proposal-algebraic-effects: 📐Que haya efectos algebraicos en JS". GitHub .

Capítulos de libros de texto

• Hankin, Chris; Nielson, Fleming; 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, Masa: MIT Press. ISBN 978-0-262-20175-9.

Documentos generales

• Nielson, Fleming; Nielson, Hanne Riis (1999). «Sistemas de tipos y efectos» . Diseño correcto del sistema: avances y conocimientos recientes . Apuntes de conferencias sobre informática . 1710 . Springer-Verlag: 114-136. doi :10.1007/3-540-48092-7_6. ISBN 978-3-540-66624-0.

Otras lecturas

• Marino, Daniel; Millstein, Todd (2009). "Un sistema genérico de tipos y efectos". Actas del cuarto taller internacional sobre tipos en el diseño e implementación de lenguajes (PDF) . ACM . pag. 39. CiteSeerX  10.1.1.157.8373 . doi :10.1145/1481861.1481868. ISBN 9781605584201. S2CID  14538045.
• Lucassen, John M.; Gifford, David K. (1988). "Sistemas de efectos polimórficos". Actas del 15º simposio ACM SIGPLAN-SIGACT sobre principios de los lenguajes de programación - POPL '88. ACM . págs. 47–57. CiteSeerX  10.1.1.73.4916 . doi :10.1145/73560.73564. ISBN 978-0897912525. S2CID  13015611.