什么数据...在Haskell中意味着什么？

Question

我看到这个片段在the devlog of 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 

什么是data ... where是什么意思？我认为关键字data用于定义新类型。

Answer 1

它定义了一个新类型，语法叫generalized algebraic data type。

它比普通语法更普遍。

data E a = A a | B Integer 

可以写为：可以使用GADTs写任何正常的类型定义（ADT）

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

但你也可以限制哪些是右手边：

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

这对于正常的ADT声明是不可能的。

欲了解更多信息，请查看Haskell wiki或this video。

---

原因是类型安全。 ExecutionAST t应该是返回t的语句类型。如果你写一个正常的ADT

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

然后ReadMemory 5将ExecutionAST t类型的多态值，而不是单态ExecutionAST Word8，这将类型检查：

x :: M_Register2 
x = ... 

a = Bind (ReadMemory 1) (WriteRegister2 x) 

这种说法应该从位置1读取内存并致信注册x。但是，从内存中读取的内容为8位字，写入x需要16位字。通过使用GADT，您可以确定这不会被编译。编译时错误比运行时错误好。

GADT还包括existential types。如果你试着写结合这种方式：

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

那么因为“oldres”它不会编译不在范围内，你必须写：

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

如果你弄糊涂了，请检查链接视频更简单，相关的例子。

Answer 2

注意，也有可能把类的限制：

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