Qu'est-ce que les données ... où signifie dans Haskell?

Question

J'ai vu cet extrait au devlog d'omegagb:

Qu'est-ce que ça veut dire ? Je pensais que le mot clé est utilisé pour définir un nouveau type.

Answer 1

Il définit un nouveau type, la syntaxe est appelé généralisée algébrique de type de données.

Il est plus général que la normale de la syntaxe. Vous pouvez écrire n'importe quel type de définition (ADT) à l'aide de GADTs:

data E a = A a | B Integer

peut être écrite comme:

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

Mais vous pouvez également restreindre ce qui est sur la droite:

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

ce qui n'est pas possible avec une normale de l'ADT de la déclaration.

Pour plus de détails, voir Haskell wiki ou cette vidéo.

---

La raison en est le type de sécurité. ExecutionAST t est censé être le type de déclarations de revenir t. Si vous écrivez un normal ADT

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

ensuite, ReadMemory 5 sera polymorphe valeur de type ReadMemory t, au lieu de monomorphe ReadMemory Word8, et cette volonté de contrôle de type:

x :: M_Register2
x = ...

a = Bind (ReadMemory 1) (WriteRegister2 x)

Cette déclaration doit se lire de la mémoire à partir de l'emplacement 1 et write pour enregistrer x. Cependant, la lecture de la mémoire donne 8-bits des mots et de l'écriture à l' x exige des mots de 16 bits. À l'aide d'un GADT, vous pouvez être sûr que ce ne sera pas compilé. Des erreurs de compilation sont mieux que les erreurs d'exécution.

GADTs également inclure existentielle types. Si vous avez essayé d'écrire lier de cette façon:

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

ensuite, il ne compile pas car "oldres" n'est pas dans le champ d'application, vous devez écrire:

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

Si vous êtes confus, cochez la vidéo liée de plus simple, liées exemple.

Answer 2

Notez qu'il est également possible de mettre des contraintes de classe :