Qu'est ce que le typestate?

Question

Qu'est-ce que TypeState fait référence à la conception de langage? Je l'ai vu mentionné dans certaines discussions concernant un nouveau langage de mozilla appelé Rust.

Answer 1

Remarque: Typestate a été abandonné à partir de la Rouille, seulement une version limitée (suivi non initialisée et déplacé de variables) est à gauche. Voir ma note à la fin.

Je n'aime pas les lien-seulement des réponses, alors le fait de se plonger dans la Rouille dernièrement (et vraiment aimer le "roman d'idées", au moins pour les langues).

La motivation derrière TypeState est que les types sont immuables, cependant certaines de leurs propriétés dynamiques, sur une base variable.

L'idée est donc de créer de simples prédicats sur un type, et utiliser le Contrôle de Flux de l'analyse que le compilateur exécuter pour de nombreuses autres raisons pour statiquement décorer le type avec ces prédicats.

Ces prédicats ne sont pas réellement vérifié par le compilateur lui-même, il pourrait être trop coûteux, au lieu de cela, le compilateur simplement des raisons en termes de graphe.

Comme exemple simple, vous créez un prédicat even, ce qui renvoie true si un nombre est pair.

Maintenant, vous pouvez créer deux fonctions:

• halve, qui n'agit que sur even nombre
• double, ce qui peut prendre un nombre, et de retourner une even nombre.

Notez que le type number n'est pas modifié, vous ne créez pas un evennumber type et de dupliquer l'ensemble de ces fonctions qui, auparavant, a agi sur number. Vous venez de composer number avec un prédicat appelés even.

Maintenant, nous allons construire un certain nombre de graphiques:

a: number -> halve(a)  #! error: `a` is not `even`

a: number, even -> halve(a)  # ok

a: number -> b = double(a) -> b: number, even

Simple, n'est-ce pas ?

Bien sûr, il devient un peu plus compliqué quand vous avez plusieurs chemins possibles:

a: number -> a = double(a) -> a: number, even -> halve(a) #! error: `a` is not `even`
          \___________________________________/

Cela montre que vous raisonnez en termes d'ensembles de prédicats:

• lors de la jonction de deux chemins, le nouvel ensemble de prédicats est l'intersection des ensembles de prédicats donné par ces deux chemins

Ce peut être augmentée par le générique de la règle d'une fonction:

• pour appeler une fonction, l'ensemble des prédicats il nécessite doivent être satisfaits
• après qu'une fonction est appelée, seulement l'ensemble des prédicats il est établi satisfaits (note: les arguments pris en valeur ne sont pas concernés)

Et donc le bloc de construction de TypeState dans la Rouille:

• check: vérifie que le prédicat est titulaire, si ce n'est pas fail, sinon ajoute le prédicat à un ensemble de prédicats

A noter que depuis la Rouille exige que les prédicats sont des fonctions pures, il peut éliminer redondant check des appels, si elle peut prouver que le prédicat détient déjà à ce stade.

---

Ce Typestate absence est simple: la composabilité.

Si vous lisez attentivement le descriptif, on peut noter ceci:

• après qu'une fonction est appelée, seulement l'ensemble des prédicats il est établi satisfaits (note: les arguments pris en valeur ne sont pas concernés)

Cela signifie que les prédicats pour un types sont inutiles en eux-mêmes, l'utilitaire est à partir de l'annotation des fonctions. Par conséquent, l'introduction d'un nouveau prédicat dans une base de code existante est un trou, comme les fonctions existantes ont besoin d'être revue et modifié pour répondre à expliquer si oui ou non ils ont besoin/de préserver l'invariant.

Et cela peut conduire à la duplication de fonctions à un rythme exponentiel lorsque de nouveaux prédicats pop-up: les prédicats ne sont pas, malheureusement, composable. La conception même problème qu'elles étaient adresse (prolifération de types, ainsi que les fonctions), ne semblent pas être abordées.

Answer 2

Il s’agit essentiellement d’une extension de types, dans laquelle vous ne vérifiez pas seulement si une opération est autorisée en général, mais dans ce contexte spécifique. Tout cela au moment de la compilation.

Le document original est en fait assez lisible.

Answer 3

Il existe un vérificateur de texte écrit pour Java et la page explicative d'Adam Warski fournit des informations utiles. Je viens juste de découvrir ce matériel moi-même, mais si vous connaissez bien QuickCheck pour Haskell, l'application de QuickCheck à un état monadique semble similaire: catégorisez les états et expliquez comment ils changent lorsqu'ils sont mutés via l'interface.