rust - usar - ¿Qué es typestate?

rust lenguaje español

Question

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

Answer 1

Es básicamente una extensión de tipos, en la que no solo se comprueba si se permite alguna operación en general, sino en este contexto específico. Todo eso a la hora de compilar.

El papel original es bastante legible.

Answer 2

Hay un verificador de tipo de letra escrito para Java, y la página explicativa de Adam Warski brinda información útil. Solo estoy descubriendo este material yo mismo, pero si está familiarizado con QuickCheck for Haskell, la aplicación de QuickCheck al estado monádico parece similar: categorice los estados y explique cómo cambian cuando se mutan a través de la interfaz.

Answer 3

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

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

Por lo tanto, la idea es crear predicados simples 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.

Esos predicados no son realmente comprobados por el compilador en sí mismo, podría ser demasiado oneroso, en lugar de eso el compilador simplemente razonará en términos de gráfico.

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

Ahora, creas dos funciones:

• halve , que solo actúa en números even .
• double , que toma cualquier número, y devuelve un número even .

Tenga en cuenta que el number tipo no se modifica, no crea un tipo de número evennumber y duplica todas las funciones que actuaron anteriormente en el number . Solo tienes que componer un number con un predicado llamado even .

Ahora, vamos a construir 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

Simple, ¿no es así?

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 rutas, el nuevo conjunto de predicados es la intersección de los conjuntos de predicados dados por esas dos rutas

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

• para llamar a una función, el conjunto de predicados que requiere debe cumplirse
• 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 bloque de construcción de TypeState en Rust :

• check : verifica que el predicado se mantenga, si no fail , de lo contrario agrega el predicado al conjunto de predicados

Tenga en cuenta que dado que Rust requiere que los predicados sean funciones puras, puede eliminar llamadas de check redundantes si puede probar que el predicado ya se cumple en este punto.

Lo que falta en Typestate es simple: composabilidad.

Si lees la descripción cuidadosamente, 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 para un tipo son inútiles en sí mismos, la utilidad proviene de funciones de anotación. Por lo tanto, la introducción de un nuevo predicado en una base de código existente es un aburrimiento, ya que las funciones existentes necesitan ser revisadas y ajustadas para atender a fin de explicar si necesitan o preservar el invariante.

Y esto puede llevar a la duplicación de funciones a una velocidad exponencial cuando aparecen nuevos predicados: los predicados no son, por desgracia, comprobables. El mismo problema de diseño que debían abordar (proliferación de tipos, por lo tanto funciones), no parece ser abordado.