Co dane ... gdzie oznacza w Haskell?

Question

Widziałem ten fragment na 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 

Czego data ... where oznacza? Myślałem, że słowo kluczowe data służy do definiowania nowego typu.

Answer 1

Definiuje nowy typ, składnia nosi nazwę generalized algebraic data type.

Jest bardziej ogólny niż zwykła składnia. Można napisać żadnej definicji typu normalnego (ADT), używając GADTs:

data E a = A a | B Integer 

można zapisać jako:

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

Ale można też ograniczać to, co znajduje się na prawej stronie:

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

, co nie jest możliwe przy normalnej deklaracji ADT.

Aby uzyskać więcej informacji, sprawdź wiki Haskella lub this video.

---

Powodem jest bezpieczeństwo typu. ExecutionAST t ma być typem instrukcji zwracających t. Jeśli piszesz normalne ADT

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

następnie ReadMemory 5 będzie polimorficzny wartość typu ExecutionAST t zamiast jednokształtnym ExecutionAST Word8, a to będzie typ kontroli:

x :: M_Register2 
x = ... 

a = Bind (ReadMemory 1) (WriteRegister2 x) 

że oświadczenie należy czytać pamięć od lokalizacji 1 i napisz do rejestracji x. Jednak odczyt z pamięci daje 8-bitowe słowa, a pisanie do x wymaga 16-bitowych słów. Korzystając z GADT, możesz być pewien, że to się nie skompiluje. Błędy czasu kompilacji są lepsze niż błędy w czasie wykonywania.

GADT zawierają także existential types. Jeśli próbował pisać wiążą ten sposób:

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

to nie będzie kompilować, ponieważ „oldres” nie jest w zakresie, trzeba napisać:

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

jeśli są zdezorientowani, sprawdź połączone wideo dla prostszego, pokrewnego przykładu.

Answer 2

Należy pamiętać, że jest to również możliwe, aby umieścić ograniczeń Klasa:

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