52

我在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是用来定义新类型的。

4

2 回答 2

73

它定义了一种新类型，语法称为广义代数数据类型。

它比普通语法更通用。您可以使用 GADT 编写任何普通类型定义 (ADT)：

data E a = A a | B Integer

可以写成：

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 或此视频。

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

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

thenReadMemory 5将是 type 的多态值ExecutionAST t，而不是 monomorphic ExecutionAST Word8，这将进行类型检查：

x :: M_Register2
x = ...

a = Bind (ReadMemory 1) (WriteRegister2 x)

该语句应该从位置 1 读取内存并写入 register x。但是，从内存读取需要 8 位字，而写入x需要 16 位字。通过使用 GADT，您可以确定这不会编译。编译时错误优于运行时错误。

GADT 还包括存在类型。如果您尝试以这种方式编写绑定：

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

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

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

如果您感到困惑，请查看链接的视频以获取更简单、相关的示例。

于 2011-11-23T16:08:54.347 回答
19

请注意，也可以放置类约束：

data E a where
  A :: Eq b => b -> E b
于 2011-11-23T16:33:05.960 回答