52

私は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キーワードは新しいタイプを定義するために使用されると思いました。

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宣言では不可能です。

詳細については、Haskellwikiまたはこのビデオを確認してください。

その理由は型安全性です。ExecutionAST tを返すステートメントのタイプであると想定されていますt。通常のADTを作成する場合

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

次に、モノモーフィックではなく、ReadMemory 5タイプのポリモーフィック値になります。これにより、タイプチェックが行われます。ExecutionAST tExecutionAST 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)

混乱している場合は、リンクされたビデオで、より簡単で関連性のある例を確認してください。

于 2011-11-23T16:08:54.347 に答える
19

クラス制約を設定することもできることに注意してください。

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