¿Qué es el tipo de estado?

Question

¿A qué se refiere TypeState con respecto al diseño del lenguaje?Lo vi mencionado en algunas discusiones sobre un nuevo lenguaje de Mozilla llamado Rust.

Answer 1

Nota: Typestate se eliminó de Rust, solo queda una versión limitada (seguimiento no inicializado y movido desde variables).Vea mi nota al final.

La motivación detrás TipoEstado es que los tipos son inmutables, sin embargo, algunas de sus propiedades son dinámicas, por variable.

Por lo tanto, la idea es crear simples predicados sobre un tipo y utilizar el análisis Control-Flow que el compilador ejecuta por muchas otras razones para decorar estáticamente el tipo con esos predicados.

En realidad, el compilador no verifica esos predicados; podría ser demasiado oneroso; en cambio, el compilador simplemente razonará en términos de gráficos.

Como ejemplo simple, creas un predicado even, que regresa true si un número es par.

Ahora, creas dos funciones:

• halve, que sólo actúa sobre even números
• double, que toma cualquier número y devuelve un even número.

Tenga en cuenta que el tipo number no se modifica, no se crea un evennumber escriba y duplique todas aquellas funciones que actuaron anteriormente number.tu solo compones number con un predicado llamado even.

Ahora, construyamos algunos gráficos:

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

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

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

Sencillo, ¿no?

Por supuesto, se vuelve un poco más complicado cuando tienes varios caminos posibles:

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

Esto demuestra que razonas en términos de conjuntos de predicados:

• al unir dos caminos, el nuevo conjunto de predicados es la intersección de los conjuntos de predicados dados por esos dos caminos

Esto puede verse aumentado por la regla genérica de una función:

• Para llamar a una función, se debe satisfacer el conjunto de predicados que requiere.
• después de llamar a una función, solo se satisface el conjunto de predicados que estableció (nota:los argumentos tomados por valor no se ven afectados)

Y así, el componente básico de TipoEstado en Óxido:

• check:comprueba que el predicado se cumple, si no es así fail, de lo contrario agrega el predicado al conjunto de predicados

Tenga en cuenta que desde Óxido requiere que los predicados sean funciones puras, puede eliminar funciones redundantes check llama si puede probar que el predicado ya se cumple en este punto.

---

Lo que le falta a Typestate es simple:componibilidad.

Si lees atentamente la descripción, notarás esto:

• después de llamar a una función, solo se satisface el conjunto de predicados que estableció (nota:los argumentos tomados por valor no se ven afectados)

Esto significa que los predicados de un tipo son inútiles en sí mismos, la utilidad proviene de la anotación de funciones.Por lo tanto, introducir un nuevo predicado en una base de código existente es aburrido, ya que las funciones existentes deben revisarse y ajustarse para explicar si necesitan/preservan o no el invariante.

Y esto puede llevar a duplicar funciones a un ritmo exponencial cuando aparecen nuevos predicados:Desafortunadamente, los predicados no son componibles.La cuestión de diseño que debían abordar (proliferación de tipos y, por tanto, de funciones) no parece abordarse.

Answer 2

Es básicamente una extensión de los tipos, donde no solo verifica si se permite alguna operación en general, pero en este contexto específico.Todo eso en el tiempo de compilación.

The Papel original es en realidad bastante legible.

Answer 3

Hay un verificador de tipestato escrito para Java, y Página explicativa de Adam Warski daalguna información útil.Solo estoy descubriendo este material a mí mismo, pero si está familiarizado con Quickcheck para Haskell, la aplicación de QuickCheck al Estado Monádico parece ser similar: categoriza los estados y explica cómo cambian cuando se mutan a través de la interfaz.