Cosa significa data ... dove significa in Haskell?

Question

Ho visto questo frammento in 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 

Cosa significa il data ... where significa? Ho pensato che la parola chiave data fosse usata per definire un nuovo tipo.

Answer 1

Definisce un nuovo tipo, la sintassi è denominata generalized algebraic data type.

È più generale della sintassi normale. È possibile scrivere qualsiasi definizione di tipo normale (ADT) utilizzando GADTs:

data E a = A a | B Integer 

può essere scritta come:

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

Ma si può anche limitare ciò che è sul lato destro:

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

che non è possibile con una normale dichiarazione ADT.

Per ulteriori informazioni, consultare Haskell wiki o this video.

---

Il motivo è la sicurezza del tipo. ExecutionAST t dovrebbe essere il tipo di dichiarazioni che restituiscono t. Se si scrive un normale ADT

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

poi ReadMemory 5 sarà un valore polimorfico di tipo ExecutionAST t, invece di monomorfa ExecutionAST Word8, e questo tipo di controllo:

x :: M_Register2 
x = ... 

a = Bind (ReadMemory 1) (WriteRegister2 x) 

Tale dichiarazione dovrebbe leggere la memoria dalla posizione 1 e scrivere per registrare x. Tuttavia, la lettura dalla memoria fornisce parole a 8 bit e la scrittura su x richiede parole a 16 bit. Usando un GADT, puoi essere certo che questo non verrà compilato. Gli errori di compilazione sono migliori degli errori di runtime.

GADT include anche existential types. Se si è tentato di scrivere legare in questo modo:

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

allora non verrà compilato dal "oldres" non è nel campo di applicazione, si deve scrivere:

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

Se siete confusi, controllare la video collegato per un esempio più semplice e correlato.

Answer 2

Si noti che è anche possibile mettere vincoli di classe:

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