tipos sintaxis semantico semantica objetivo linguistica gramatica ejemplos contenido rust move-semantics mercury clean-language

sintaxis - ¿Cómo se relaciona la semántica de propiedad de Rust con la tipificación de la singularidad que se encuentra en Clean and Mercury?



semantica y sintaxis (1)

El concepto de propiedad en Rust no es lo mismo que la singularidad de Mercury y Clean, aunque están relacionados en el sentido de que ambos pretenden proporcionar seguridad a través de la verificación estática, y ambos se definen en términos del número de referencias dentro de un alcance. Las diferencias clave son:

  • La singularidad es un concepto más abstracto. Si bien se puede interpretar que dice que una referencia a una ubicación de memoria es única, como los lvalues de Rust, también se puede aplicar a valores abstractos como el estado de cada objeto en el universo, para dar un ejemplo extremo pero típico. No hay un puntero correspondiente a ese valor (no se puede abrir e inspeccionar dentro de un depurador ni nada de eso), pero se puede usar a través de una interfaz como cualquier otro tipo de resumen. El objetivo es dar una semántica orientada al valor que permanezca consistente en presencia de estado de estado.

  • En Mercury, al menos (no puedo hablar en nombre de Clean), la unicidad es un concepto más limitado que la propiedad, ya que debe haber exactamente una referencia. No puede compartir varias copias de una referencia con la condición de que no se escriban, como se puede hacer en Rust. Tampoco puede prestar una referencia para escribir, pero recupérela más tarde después de que el prestatario haya terminado con ella.

  • Declarar algo único en Mercury no garantiza que la escritura a las referencias ocurrirá, solo que el compilador verificará que sea seguro hacerlo; sigue siendo válido para una implementación copiar el contenido de una referencia única en lugar de actualizarlo en su lugar. El compilador se encargará de la actualización en su lugar si lo considera apropiado en su nivel de optimización dado. Alternativamente, los autores de tipos abstractos pueden realizar optimizaciones similares (o, a veces, drásticamente mejores) manualmente, con la certeza de que los usuarios se verán obligados a usar el tipo abstracto de una manera que sea consistente con ellos. La propiedad en Rust, por otro lado, está más directamente conectada al modelo de memoria y ofrece garantías más sólidas sobre el comportamiento.

Noté que en Rust, el movimiento se aplica a los valores, y se aplica de manera estática que los objetos movidos desde no se usan.

¿Cómo se relacionan estas semánticas con la tipificación de la singularidad que se encuentra en Clean and Mercury? ¿Son el mismo concepto? Si no, ¿en qué se diferencian?