haskell - ¿Mensaje de error extraño, "Mi cerebro acaba de explotar"?

gadt arrows

Question

Cuando trato de un patrón de GADT en una sintaxis de proc (con Netwire y Vinyl):

sceneRoot = proc inputs -> do
let (Identity camera :& Identity children) = inputs
returnA -< (<*>) (map (rGet draw) children) . pure

Recibo el error del compilador (bastante extraño), de ghc-7.6.3

My brain just exploded I can''t handle pattern bindings for existential or GADT data constructors. Instead, use a case-expression, or do-notation, to unpack the constructor. In the pattern: Identity cam :& Identity childs

Recibo un error similar cuando coloco el patrón en el patrón proc (...) . ¿Por qué es esto? ¿Es defectuoso, o simplemente no implementado?

Answer 1

Considera el GADT

data S a where
S :: Show a => S a

y la ejecución del código.

foo :: S a -> a -> String
foo s x = case s of
S -> show x

En una implementación de Haskell basada en un diccionario, uno esperaría que el valor s tenga un diccionario de clase, y que el case extraiga la función show de dicho diccionario para que se pueda show x .

Si ejecutamos

foo undefined (/x::Int -> 4::Int)

obtenemos una excepción Operativamente, esto se espera, porque no podemos acceder al diccionario. Más en general, el case (undefined :: T) of K -> ... producirá un error porque obliga a la evaluación de undefined (siempre que T no sea un tipo newtype ).

Considere ahora el código (vamos a pretender que esto se compila)

bar :: S a -> a -> String
bar s x = let S = s in show x

y la ejecución de

bar undefined (/x::Int -> 4::Int)

¿Qué debería hacer esto? Se podría argumentar que debería generar la misma excepción que con foo . Si este fuera el caso, la transparencia referencial implicaría que

let S = undefined :: S (Int->Int) in show (/x::Int -> 4::Int)

falla también con la misma excepción. Esto significaría que let está evaluando la expresión undefined , a diferencia de, por ejemplo,

let [] = undefined :: [Int] in 5

el cual se evalúa a 5 .

De hecho, los patrones en un let son flojos : no obligan a la evaluación de la expresión, a diferencia del case . Por eso, por ejemplo,

let (x,y) = undefined :: (Int,Char) in 5

Evalúa con éxito a 5 .

Uno podría querer hacer let S = e in e'' evalúe e si se necesita un show en e'' , pero se siente bastante raro. Además, al evaluar let S = e1 ; S = e2 in show ... let S = e1 ; S = e2 in show ... no estaría claro si evaluar e1 , e2 o ambos.

Por el momento, GHC elige prohibir todos estos casos con una regla simple: no hay patrones perezosos al eliminar un GADT.