¿Qué significa data... where mean en Haskell?

syntax gadt

Question

Vi este fragmento en el devlog de omegagb :

data ExecutionAST result where
  Return :: result -> ExecutionAST result
  Bind :: (ExecutionAST oldres) -> (oldres -> ExecutionAST result) ->
          ExecutionAST result
  WriteRegister :: M_Register -> Word8 -> ExecutionAST ()
  ReadRegister :: M_Register -> ExecutionAST Word8
  WriteRegister2 :: M_Register2 -> Word16 -> ExecutionAST ()
  ReadRegister2 :: M_Register2 -> ExecutionAST Word16
  WriteMemory :: Word16 -> Word8 -> ExecutionAST ()
  ReadMemory :: Word16 -> ExecutionAST Word8

¿Qué significa la data ... where significa? Pensé que los data palabra clave se utilizan para definir un nuevo tipo.

Answer 1

Tenga en cuenta que también es posible poner restricciones de clase:

data E a where
  A :: Eq b => b -> E b

Answer 2

Define un nuevo tipo, la sintaxis se llama tipo de datos algebraicos generalizados .

Es más general que la sintaxis normal. Puede escribir cualquier definición de tipo normal (ADT) usando GADT:

data E a = A a | B Integer

Se puede escribir como:

data E a where
  A :: a -> E a
  B :: Integer -> E a

Pero también puedes restringir lo que está en el lado derecho:

data E a where
  A :: a -> E a
  B :: Integer -> E a
  C :: Bool -> E Bool

que no es posible con una declaración ADT normal.

Para obtener más información, consulte la wiki de Haskell o este video .

La razón es tipo de seguridad. ExecutionAST t se supone que es un tipo de declaraciones que devuelve t . Si escribe un ADT normal

data ExecutionAST result = Return result 
                         | WriteRegister M_Register Word8
                         | ReadRegister M_Register
                         | ReadMemory Word16
                         | WriteMemory Word16
                         | ...

entonces ReadMemory 5 será un valor polimórfico de tipo ExecutionAST t , en lugar de monomórfico ExecutionAST Word8 , y esto escribirá check:

x :: M_Register2
x = ...

a = Bind (ReadMemory 1) (WriteRegister2 x)

Esa declaración debe leer la memoria de la ubicación 1 y escribir para registrar x . Sin embargo, leer desde la memoria da palabras de 8 bits, y escribir en x requiere palabras de 16 bits. Al usar un GADT, puede estar seguro de que esto no se compilará. Los errores de tiempo de compilación son mejores que los errores de tiempo de ejecución.

Las GADT también incluyen tipos existenciales . Si trataste de escribir un enlace de esta manera:

data ExecutionAST result = ... 
                           | Bind (ExecutionAST oldres)
                                  (oldres -> ExecutionAST result)

entonces no compilará porque "oldres" no está en el alcance, tienes que escribir:

data ExecutionAST result = ...
                           | forall oldres. Bind (ExecutionAST oldres)
                                                 (oldres -> ExecutionAST result)

Si está confundido, consulte el video vinculado para obtener un ejemplo más simple y relacionado.