¿Qué es un sistema de tipo y efecto?

Question

El artículo de Wikipedia sobre Sistema de efectos es actualmente un breve trozo y me he estado preguntando por un tiempo sobre qué es un sistema de efectos.

• ¿Hay algún idioma que tenga un sistema de efectos además de un sistema de tipos?
• ¿Cuál sería una posible notación (hipotética) en un lenguaje mainstream , con el que esté familiarizado, con efectos similares?

Answer 1

A " tipo y sistema de efectos " describe no solo los tipos de valores en un programa, sino también los cambios en esos valores. "Tipo de letra" verificar es una idea relacionada.

Un ejemplo podría ser un sistema de tipos que rastrea los identificadores de archivos: en lugar de tener una función close con el tipo de retorno void , el sistema de tipos registraría el efecto de close como disposición del recurso de archivo; cualquier intento de leer o escribir en el archivo después de llamar a close se convertiría en un error de tipo.

No conozco ningún tipo de sistema de efectos 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 el bloqueo / desbloqueo adecuado en términos de efectos). Como tal, los sistemas de efectos generalmente se definen utilizando esquemas de inferencia en lugar de sintaxis concreta. Podrías imaginar una sintaxis similar a

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 razonable: los documentos son bastante teóricos).

• Tipos de atomicidad: comprobación estática e inferencia para Java . Flanagan, Freund, Lipshin y Qadeer.
• Aplicación de protocolos de alto nivel en software de bajo nivel . Robert DeLine y Manuel Fändrich.
• Sistemas de tipo y efecto . Nielson y Nielson.

Answer 2

(Esta no es una respuesta autorizada; solo trato de rastrear mi memoria).

En cierto sentido, cada vez que codifica una 'mónada de estado' en un idioma, está utilizando el sistema de tipos como un sistema de efectos potenciales. Entonces '' Estado '' o "IO" en Haskell captura esta noción (IO también captura muchos otros efectos). Recuerdo vagamente haber leído documentos sobre varios idiomas que usan sistemas de tipos avanzados que incluyen cosas como "tipos dependientes". para controlar la gestión más precisa de los efectos, de modo que, por ejemplo, el sistema de tipo / efecto pueda capturar información sobre qué ubicaciones de memoria se modificarían en un tipo de datos determinado. Esto es útil, ya que proporciona formas de hacer que dos funciones que modifican bits de estado mutuamente excluyentes puedan "conmutar". (las mónadas no suelen conmutar, y las diferentes mónadas no siempre se componen bien entre sí, lo que a menudo dificulta la escritura (léase: asigne un tipo estático a) programas 'razonables') ...

Una analogía en un nivel muy ondulado a mano es cómo Java ha verificado las excepciones. 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' generalmente se filtran en todo su programa y no componen bien práctica (terminas con un millón de cláusulas de 'tiros' o de lo contrario recurres a muchos tipos de excepciones de tiempo de ejecución no controladas).

Creo que se está haciendo mucha investigación en esta área, tanto para los lenguajes y-research como para mainstream-y, ya que la capacidad de anotar funciones con información de efectos puede desbloquear la capacidad del compilador para hacer una serie de optimizaciones, puede afectar concurrencia, y puede hacer grandes cosas para varios análisis de programas y herramientas. Sin embargo, personalmente no tengo grandes esperanzas en el futuro, ya que creo que muchas personas inteligentes han estado trabajando en ello durante mucho tiempo y todavía hay muy poco que mostrar.

Answer 3

Puede echar un vistazo a http://www.haskell.org/haskellwiki/DDC

Es una versión de Haskell que implementa un sistema de efectos.