Pregunta sobre el subtipo de controladores en "Un sistema de efectos para efectos algebraicos y controladores"

Tenía una pregunta sobre el subtipo en el documento "Un sistema de efectos para efectos algebraicos y controladores" . Me preguntaba por qué no hay una regla de subtipo para agregar efectos en ambos lados de un tipo de controlador, algo como esto:

$$\frac{ }{ T!A \;\Rightarrow\; R!B \;\leqslant\; T!(A \cup C) \;\Rightarrow \;R!(B \cup C) }$$

Esto sería útil cuando aplique una variable con un tipo de controlador a un cálculo con más efectos que el tipo de controlador en su lado izquierdo.

Puede agregar efectos a ambos lados de un tipo de controlador utilizando la regla de escritura para controladores, pero eso no funcionará para las variables. Por ejemplo, cuando el controlador es un argumento para una función.

Me sorprende que no recibamos esta pregunta con más frecuencia, ya que Andrej y yo hemos considerado agregar esta regla durante bastante tiempo y creemos que ha demostrado su corrección. Pero al final, resultó ser falso, al menos en una configuración de llamada por valor (he oído que funciona mejor en llamada por valor de inserción).

Considere el controlador de estado, que se describe en la parte superior de la página 24 del mismo papel, que tiene un cálculo de estado de tipo en el estado y la transforma en una función pura a partir de a . ¡Su tipo es Tenga en cuenta los dos conjuntos vacíos en el lado derecho. El primero indica que la función resultante es pura, el segundo que no se producen efectos al producir esta función.A A B B ! { l o o k u p , u p d a t e } ⇒ ( A → B ! ∅ ) ! $B$$A$$A$$B$

$$B!\{\mathtt{lookup},\mathtt{update}\} \Rightarrow (A \to B ! \emptyset) ! \emptyset$$

Ahora suponga que aplicamos el controlador a un cálculo que puede llamar a otros efectos además de y . Aplicando la regla sugerida, obtendría el tipo pero, de hecho, el tipo correcto es como los efectos no controlados puede ocurrir antes de producir la función o después de llamarla.$\Delta$$\mathtt{lookup}$$\mathtt{update}$

$$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \emptyset) ! \Delta$$ $$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \Delta) ! \Delta$$ $\Delta$