haskell - ¿Por qué los constructores de datos existenciales/GADT no pueden usarse en patrones perezosos?

pattern-matching lazy-evaluation

Question

Hoy, recibí un error del compilador al intentar usar un patrón perezoso al hacer coincidencias en un constructor GADT existencial:

Un constructor de datos existencial o GADT no se puede usar dentro de un patrón perezoso (~)

¿Por qué es esa limitación? ¿Qué cosas "malas" podrían pasar, si se permitieran?

Answer 1

Con los datos "normales", puede omitir la comprobación del constructor durante la coincidencia de patrones, en el entendido de que cuando intenta utilizar los datos del patrón, puede que no exista, por lo que es una excepción.

Con un GADT, la firma de tipo cambia potencialmente dependiendo del constructor que esté presente. Necesitamos saber acerca de los tipos en tiempo de compilación ; no sirve de nada comprobar el constructor hasta que necesites los valores. Si lo hace, podría tener un error de falta de coincidencia de tipo. Y eso, potencialmente, significa que su programa falla con una falla de segmentación (o peor). Los programas de Haskell nunca deben segfault.

Answer 2

Considerar

data EQ a b where
  Refl :: EQ a a

Si pudiéramos definir

transport :: Eq a b -> a -> b
transport ~Refl a = a

entonces podríamos tener

transport undefined :: a -> b

y asi adquirir

transport undefined True = True :: Int -> Int

y luego un choque, en lugar del fallo más elegante que se obtiene al intentar normalizar lo undefined .

Los datos de GADT representan evidencia sobre los tipos, por lo que los datos falsos de GADT amenazan la seguridad de los tipos. Es necesario ser estricto con ellos para validar esa evidencia: no se puede confiar en cálculos no evaluados en presencia de fondo.