Type d'unicité - Uniqueness type

Systèmes de types
Concepts généraux
Principales catégories
Catégories mineures

En informatique , un type unique garantit qu'un objet est utilisé de manière monothread , avec au plus une seule référence. Si une valeur a un type unique, une fonction qui lui est appliquée peut être optimisée pour mettre à jour la valeur en place dans le code objet . De telles mises à jour sur place améliorent l'efficacité des langages fonctionnels tout en maintenant la transparence référentielle . Les types uniques peuvent également être utilisés pour intégrer la programmation fonctionnelle et impérative.

introduction

Le typage d'unicité est mieux expliqué à l'aide d'un exemple. Considérons une fonction readLinequi lit la ligne de texte suivante à partir d'un fichier donné : 

function readLine(File f) returns String
    return line where
        String line = doImperativeReadLineSystemCall(f)
    end
end

Maintenant , doImperativeReadLineSystemCalllit la ligne suivante du fichier en utilisant un système d' exploitation -level appel système qui a pour effet secondaire de changer la position actuelle dans le fichier. Mais cela viole la transparence référentielle car l'appeler plusieurs fois avec le même argument renverra des résultats différents à chaque fois que la position actuelle dans le fichier est déplacée. Ceci à son tour fait readLinevioler la transparence référentielle car elle appelle doImperativeReadLineSystemCall.

Cependant, en utilisant le typage d'unicité, nous pouvons construire une nouvelle version readLinequi est référentiellement transparente même si elle est construite au-dessus d'une fonction qui n'est pas référentiellement transparente : 

function readLine2(unique File f) returns (unique File, String)
    return (differentF, line) where
        String line = doImperativeReadLineSystemCall(f)
        File differentF = newFileFromExistingFile(f)
    end
end

La uniquedéclaration spécifie que le type de fest unique ; c'est-à-dire qui fne peut plus jamais être référencé par l'appelant de readLine2after readLine2return, et cette restriction est imposée par le type system . Et puisque readLine2ne renvoie pas flui-même mais plutôt un nouvel objet fichier différent differentF, cela signifie qu'il est impossible readLine2d'être appelé à nouveau avec fcomme argument, préservant ainsi la transparence référentielle tout en permettant aux effets secondaires de se produire.

Langages de programmation

Les types d'unicité sont implémentés dans des langages de programmation fonctionnels tels que Clean , Mercury , SAC et Idris . Ils sont parfois utilisés pour effectuer des opérations d' E/S dans des langages fonctionnels au lieu de monades .

Une extension de compilateur a été développée pour le langage de programmation Scala qui utilise des annotations pour gérer l'unicité dans le contexte de la transmission de messages entre les acteurs.

Relation avec le typage linéaire

Un type unique est très similaire à un type linéaire , au point que les termes sont souvent utilisés de manière interchangeable, mais il y a en fait une distinction : le typage linéaire réel permet à une valeur non linéaire d'être transtypée sous une forme linéaire, tout en conservant plusieurs références à celui-ci. L'unicité garantit qu'une valeur n'a pas d'autres références à elle, tandis que la linéarité garantit qu'aucune autre référence ne peut être faite à une valeur.

Voir également

Les références

Liens externes

Discussions sur le typage d'unicité dans les langages de programmation

Expériences de typage d'unicité (du point de vue des performances)