什麼數據...在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