Qu'est-ce qu'un système de type et d'effet?

Question

Le article de Wikipedia sur Système d'effets est actuellement bref. stub et je me demandais depuis un moment de savoir ce qu'est un système d'effet.

• Existe-t-il des langues ayant un système d’effet en plus d’un système de types?
• À quoi ressemblerait une notation (hypothétique) possible dans une langue traditionnelle , avec laquelle vous êtes familier, avec des effets?

Answer 1

Un "système de type et d'effet" décrit non seulement les types de valeurs dans un programme, mais aussi les modifications apportées à ces valeurs. " Typestate " la vérification est une idée liée.

Un exemple pourrait être un système de types qui suit les descripteurs de fichiers: au lieu d'avoir une fonction close avec le type de retour void , le système de types enregistre l'effet . de close en tant que suppression de la ressource de fichier - toute tentative de lecture ou d'écriture dans le fichier après l'appel de close deviendrait une erreur de type.

Je ne connais aucun type ni système d'effet apparaissant dans un langage de programmation traditionnel. Ils ont été utilisés pour définir des analyses statiques (par exemple, il est tout à fait naturel de définir une analyse pour un verrouillage / déverrouillage correct en termes d'effets). En tant que tels, les systèmes d'effets sont généralement définis à l'aide de schémas d'inférence plutôt que d'une syntaxe concrète. Vous pouvez imaginer une syntaxe ressemblant à quelque chose comme

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

Si vous souhaitez en savoir plus, les articles suivants pourraient être intéressants (bon avertissement: les articles sont assez théoriques).

• Types d'atomicité: vérification statique et inférence pour Java . Flanagan, Freund, Lipshin et Qadeer.
• Application de protocoles de haut niveau dans les logiciels de bas niveau . Robert DeLine et Manuel Fändrich.
• Systèmes de type et d'effet . Nielson et Nielson.

Answer 2

(Ce n'est pas une réponse faisant autorité; j'essaie simplement de fouiller ma mémoire.)

En un sens, chaque fois que vous codez une "monade d'état" dans une langue, vous utilisez le système de types comme système à effets potentiels. Donc, "Etat" ou " IO " dans Haskell capturer cette notion (IO capture beaucoup d'autres effets). Je me souviens vaguement d'avoir lu des articles sur diverses langues qui utilisent des systèmes de types avancés, tels que "types dépendants". pour contrôler une gestion plus fine des effets, afin que, par exemple, le système type / effet puisse capturer des informations sur les emplacements de mémoire qui seraient modifiés dans un type de données donné. Ceci est utile car il permet de "permuter" deux fonctions modifiant des bits d’État mutuellement exclusifs. (les monades ne font pas habituellement la navette, et les différentes monades ne se composent pas toujours bien, ce qui rend souvent difficile la frappe (lire: affecter un type statique à) des programmes 'raisonnables') ...

Une analogie à un niveau très très vague est la façon dont Java a vérifié les exceptions. Vous exprimez des informations supplémentaires dans le système de types à propos de certains effets (vous pouvez considérer une exception comme un "effet" aux fins de l'analogie), mais ces "effets" se répercutent généralement sur votre programme et ne composent pas bien. pratique (vous vous retrouvez avec un million de clauses de type "jets" ou bien vous avez recours à de nombreux types d’exceptions non contrôlées).

Je pense que de nombreuses recherches sont en cours dans ce domaine, aussi bien pour les langages de recherche que pour les langages grand public, car la possibilité d'annoter des fonctions avec des informations sur les effets peut permettre au compilateur de réaliser plusieurs optimisations, ce qui peut avoir une incidence sur simultanéité, et peut faire de grandes choses pour diverses analyses de programmes et d’outils. Personnellement, je ne mets pas beaucoup d'espoir dans l'avenir, cependant, car je pense que beaucoup de personnes intelligentes y travaillent depuis longtemps et qu'il y a encore très peu à démontrer.

Answer 3

Vous pouvez consulter http://www.haskell.org/haskellwiki/DDC

C’est une version de Haskell implémentant un système d’effet.