数据是什么......在Haskell中意味着什么？ [英] What does data ... where mean in Haskell?

问题描述

我在 omegagb的devlog 上看到了这段代码：

I saw this snippet at 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 用于定义一个新类型。

What does the data ... where mean? I thought the keyword data is used to define a new type.

推荐答案

它定义了一个新类型，语法叫做广义代数数据类型。

It defines a new type, the syntax is called generalized algebraic data type.

它比正常语法更普遍。您可以使用GADT编写任何常规类型定义（ADT）：

It is more general than the normal syntax. You can write any normal type definition (ADT) using GADTs:

data E a = A a | B Integer

可以写成：

can be written as:

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

但是您也可以限制右侧的内容：

But you can also restrict what is on right hand side:

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

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

which is not possible with a normal ADT declaration.

如需更多信息，请查看Haskell wiki或此视频。

For more, check Haskell wiki or this video.

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

The reason is type safety. ExecutionAST t is supposed to be type of statements returning t. If you write a normal ADT

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

然后 ReadMemory 5 将会一个类型为code> ExecutionAST t 的多态值，而不是单态执行ASTWord8 ，这样就会检查：

then ReadMemory 5 will be a polymorphic value of type ExecutionAST t, instead of monomorphic ExecutionAST Word8, and this will type check:

x :: M_Register2
x = ...

a = Bind (ReadMemory 1) (WriteRegister2 x)

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

That statement should read memory from location 1 and write to register x. However, reading from memory gives 8-bit words, and writing to x requires 16-bit words. By using a GADT, you can be sure this won't compile. Compile-time errors are better than run-time errors.

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

GADTs also include existential types. If you tried to write bind this way:

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

因为oldres不在范围内，所以你必须编写：

then it won't compile since "oldres" is not in scope, you have to write:

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

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

If you are confused, check the linked video for simpler, related example.

这篇关于数据是什么......在Haskell中意味着什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！