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

Question

我在omegagb的devlog上看到了这个片段:

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

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

它比普通语法更通用.您可以使用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
                         | ...

然后ReadMemory 5将是类型的多态值ExecutionAST t,而不是单态ExecutionAST Word8,这将键入检查:

x :: M_Register2
x = ...

a = Bind (ReadMemory 1) (WriteRegister2 x)

该语句应从位置1读取内存并写入寄存器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)

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

Answer 2

请注意,也可以放置类约束:

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