tutorial poner plantillas instalar imagen fondo examples español app types effects type-systems type-theory effect-systems

types - poner - ¿Qué es un sistema de tipo y efecto?



plantillas django (3)

El artículo de Wikipedia sobre el sistema de efectos es actualmente solo un trozo corto y me he estado preguntando durante un tiempo qué es un sistema de efectos.

  • ¿Hay algún idioma que tenga un sistema de efectos además de un sistema de tipos?
  • ¿Qué aspecto tendría con los efectos una notación (hipotética) posible en un idioma principal , con el que esté familiarizado?

(Esta no es una respuesta autoritativa, solo estoy tratando de rastrear mi memoria).

En cierto sentido, cada vez que codifica una ''mónada de estado'' en un idioma, está utilizando el sistema de tipo como un sistema de efecto potencial. Entonces "State" o "IO" en Haskell capturan esta noción (IO captura muchos otros efectos también). Recuerdo vagamente leer artículos sobre varios idiomas que usan sistemas de tipo avanzado que incluyen cosas como "tipos dependientes" para controlar el manejo de los efectos de manera más precisa, de modo que el sistema de tipo / efecto podría capturar información sobre qué ubicaciones de memoria se modificarían en una tipo de datos dado Esto es útil, ya que proporciona formas de permitir que dos funciones que modifican bits de estado mutuamente exclusivos se "conmuten" (las mónadas no suelen conmutar, y las mónadas diferentes no siempre se combinan bien entre sí, lo que a menudo lo hace difícil de escribir (léase: asignar un tipo estático a) programas "razonables") ...

Una analogía en un nivel muy ondulado es cómo Java ha verificado las excepciones. Usted expresa información adicional en el sistema de tipos sobre ciertos efectos (puede pensar en una excepción como un "efecto" para el propósito de la analogía), pero estos "efectos" típicamente se filtran en todo su programa y no se componen bien en practica (terminas con un millón de cláusulas de ''throws'' o recurres a muchos tipos de excepciones de tiempo de ejecución no revisadas).

Creo que se están realizando muchas investigaciones en esta área, tanto para los lenguajes de investigación como de mainstream, ya que la capacidad de anotar funciones con información de efecto puede desbloquear la capacidad del compilador para realizar varias optimizaciones, puede afectar la concurrencia y puede hacer grandes cosas para varios análisis de programas y herramientas. Personalmente, no tengo muchas esperanzas en ello pronto, ya que creo que mucha gente inteligente ha estado trabajando en ello durante mucho tiempo y todavía hay muy poco que mostrar.

Un "sistema de tipo y efecto" describe no solo los tipos de valores en un programa, sino también los cambios en esos valores. La verificación "tipo de estado" es una idea relacionada.

Un ejemplo podría ser un sistema de tipo que rastrea los manejadores de archivos: en lugar de tener una función close con return type void , el sistema tipo registrará el efecto de close como deshacerse del recurso de archivo, cualquier intento de leer o escribir en el archivo después de Llamar close se convertiría en un error de tipo.

No conozco ningún sistema de tipo y efecto que aparezca en un lenguaje de programación convencional. Se han utilizado para definir análisis estáticos (por ejemplo, es bastante natural definir un análisis para un bloqueo / desbloqueo adecuado en términos de efectos). Como tal, los sistemas de efectos generalmente se definen usando esquemas de inferencia en lugar de sintaxis concreta. Se podría imaginar una sintaxis que se parezca a algo como

File open(String name) [+File]; // open creates a new file handle void close(File f) [-f] ; // close destroys f

Si desea obtener más información, los siguientes documentos pueden ser interesantes (advertencia justa: los documentos son bastante teóricos).