2008-10-13 15 views

Respuesta

15

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

Un ejemplo podría ser un sistema del tipo que realiza el seguimiento de archivos llaves: en lugar de tener una función close con el regreso de tipo void, el sistema de tipos registraría el efecto de close como la eliminación del archivo de recursos — cualquier intento de leer o escribir en el archivo después de llamar al 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 parecida 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 justa: los papeles son bastante teórico).

6

(Esto no es una respuesta autorizada;. Tratando de arrastre a mi memoria)

En cierto sentido, cada vez que el código A 'mónada estado en un idioma, que está utilizando el sistema de tipos 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 muy ondulado a mano nivel es cómo Java ha comprobado 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 para mainstream-y, ya que la capacidad de anotar funciones con información de efecto puede desbloquear la capacidad del compilador para realizar varias optimizaciones. impactar el impacto, 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.

+1

holy cow man, ¿se suponía que era inglés? intente comenzar con la definición de un 'efecto' y vaya desde allí. "estado mónada"? jaja! No creo que pueda suponer que el lector está familiarizado con Haskell ... –

+0

Steven, no soy un experto en programación monádica, pero tengo cierta familiaridad con Haskell. –

+1

@ [marxidad]: eso es genial, pero (a) no lo dijiste en la pregunta, así que era una suposición y (b) otras personas leerán las respuestas. –

4

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

Es una versión de Haskell implementar un sistema de efecto.

+0

Lamentablemente, haskell.org ha emprendido una reorganización y ¡el enlace se ha extinguido! – fatuhoku

+0

@fatuhoku: El enlace ha sido corregido. – chirlu

Cuestiones relacionadas