La linealidad no es una restricción suficiente para precisar una representación con estado única, por lo que la respuesta a su pregunta depende de cómo interprete la lógica lineal en términos de estado. Esto normalmente se reflejará en cómo debe interpretar la modalidad!A
Si su semántica de referencias prevista dice que todos los punteros son valores únicos (es decir, hay como máximo una sola referencia a un objeto), entonces las estructuras de gráficos y dags no son expresables, por el tipo de razón tautológica de que un dag puede contener múltiples referencias a El mismo objeto. En este caso, debe ser un cálculo que crea un nuevo valor de tipo , ya que desea mapas Y .!AAδA:!A⊸!A⊗!AϵA:!A⊸A
Sin embargo, suponga que quiere para representar compartir . Luego, los objetos se pueden recolectar con el recuento de referencias, con los mapas y se pueden realizar como operaciones que solo aumentan los recuentos de referencias. En este caso, no puede usar la linealidad para suponer que siempre es seguro mutar valores, ya que se comparte. Pero puede asegurarse de que toda la asignación de memoria sea explícita en su programa y que no haya ciclos en el montón.!AδA:!A⊸!A⊗!AϵA:!A⊸A
La mayoría de las implementaciones prácticas de tipos lineales no utilizan ninguna de estas dos interpretaciones. En cambio, las referencias se ven como entidades libremente duplicables, y lo que rastreamos linealmente son, de hecho, capacidades . Las capacidades no son valores de tiempo de ejecución; son entidades puramente conceptuales que pretenden representar el permiso para acceder a una referencia. La idea es que programe en un estilo de aprobación de permisos, por lo que incluso si hay muchas referencias al mismo objeto, una lectura o modificación de un estado solo puede ocurrir si también tiene la capacidad de acceder a él. Y dado que la capacidad es lineal, sabe que solo usted puede cambiarla.
newgetsetcopy::::∀α.α⊸∃c:ι.cap(c)⊗ref(α,c)∀α,c:ι.cap(c)⊗ref(α,c)⊸α⊗cap(c)⊗ref(α,c)∀α,c:ι.cap(c)⊗ref(α,c)⊗α⊸cap(c)⊗ref(α,c)∀α,c:ι.ref(α,c)⊸ref(α,c)⊗ref(α,c)
En la API esbozada anteriormente, varía sobre , algunos dominios de índices de tiempo de compilación y varía sobre tipos. Tenemos un tipo que es una capacidad indexada por , y un tipo , que es un tipo de referencias a accede una capacidad . Llamar a y en una referencia requiere la capacidad , y llamar a crea una nueva referencia y una nueva capacidad que comparte un índice común. Sin embargo,cιαcap(c)cref(α,c)αcgetsetcnewcopy-ing una referencia no requiere acceso a ninguna capacidad, por lo que cualquiera puede copiar una referencia siempre que no mire dentro de ella.