haskell - ¿Se pueden reemplazar de forma segura todas las ocurrencias de verificación de tipo de ''coerce'' por ''inseguroCoerce''?
set (2)
Esto debería ser seguro.
Un
coerce @a @b
válido
coerce @a @b
siempre se puede reemplazar por un
unsafeCoerce @a @b
válido
unsafeCoerce @a @b
.
¿Por qué?
Porque, en el nivel Core, son la misma función,
coerce
(que solo devuelve su entrada, como
id
).
La cuestión es que la
coerce
toma, como argumento, una prueba de que las dos cosas que se están coaccionando tienen la misma representación.
Con
coerce
normal, esta prueba es una prueba real, pero con
unsafeCoerce
, esta prueba es solo un token que dice "confía en mí".
Esta prueba se pasa como un argumento de tipo y, por lo tanto, por borrado de tipo, no tiene ningún efecto sobre el comportamiento del programa.
Por
unsafeCoerce
tanto,
unsafeCoerce
y
coerce
son equivalentes siempre que ambos sean posibles.
Ahora, este no es el final de la historia de
Set
, porque la
coerce
no funciona en
Set
.
¿Por qué?
Echemos un vistazo a su definición.
data Set a = Bin !Size !a !(Set a) !(Set a) | Tip
A partir de esta definición, vemos que
a
no aparece dentro de ningún tipo de igualdad, etc. Esto significa que tenemos congruencia de igualdad de representación en
Set
: si
a ~#R b
(si
a
tiene la misma representación que
b
-
~#R
está en caja
Coercible
), luego
Coercible
Set a ~#R Set b
.
Entonces, desde la definición de
Set
solo,
coerce
debería
funcionar en
Set
y, por lo tanto, su
unsafeCoerce
debería
ser seguro.
La biblioteca de
containers
tiene que usar un específico
type role Set nominal
para ocultar este hecho del mundo, deshabilitando artificialmente la
coerce
.
unsafeCoerce
embargo, nunca puede deshabilitar
unsafeCoerce
y, reiterando,
unsafeCoerce
(en este contexto) es seguro.
(¡
unsafeCoerce
cuidado de que el
unsafeCoerce
y el
coerce
tengan el mismo tipo! Vea la respuesta de @ dfeuer para ver un ejemplo de una situación en la que la inferencia de tipos "excesivamente celosa" deforma todo).
Creo que lo siguiente es tan seguro como
Set.mapMonotonic coerce
.
es decir, lo peor que puede pasar es que rompa los invariantes de
Set
si
b
tienen diferentes instancias de
Ord
:
coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce
¿Es eso correcto?
EDITAR
: problema de función relevante para
Set
:
https://github.com/haskell/containers/issues/308
Sí, esto debería ser seguro en circunstancias realistas típicas. Sin embargo, es posible encontrar ejemplos artificiales donde no es así. Aquí hay uno que usa valores predeterminados. Me imagino que podría ser posible utilizar instancias superpuestas u otras características extrañas para hacer algo similar, pero no lo sé.
{-# language GADTs, TypeOperators, ExistentialQuantification #-}
import Data.Coerce
import Unsafe.Coerce
import Data.Type.Equality
data Buh a = Buh (a :~: Rational) a
data Bah = forall a. Bah (a :~: Rational) a
instance Show Bah where
show (Bah Refl x) = show x
goo :: Rational -> Bah
goo x = case coerce p of
Buh pf m ->
let _q = truncate m
in Bah pf 12
where
p = Buh Refl x
Si llamas
goo
, todo estará bien.
Si reemplaza
coerce
con
unsafeCoerce
, llamar a
goo
segfault o hará algo malo.