What does data ... where mean in Haskell?

Question

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

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

score 74 · Accepted Answer · edited Nov 20 '16 at 09:03

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

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

which is not possible with a normal ADT declaration.

For more, check Haskell wiki or this video.

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
                         | ...

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)

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.

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

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

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.

I find your explanation is better than the video clip. Thanks. — wliao, Nov 24 '11 at 13:18

score 19 · Answer 2 · answered Nov 23 '11 at 16:33

19

Note that it is also possible to put class constraints:

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

answered Nov 23 '11 at 16:33

nponeccop

13,527
1
44
106

10

And more importantly, unlike in regular `data` declarations, this actually causes the instance dictionary to be stored in the type, allowing you to recover it through pattern matching, just like with existential types. – hammar Nov 23 '11 at 17:10
2

@hammar I don't understand what your comment imply. I don't understand this wording (with my rephrasing) 'to recover the instance dictionary through pattern matching because it is stored in the type'. When I pattern match, I deconstruct according the shape of the structure, and I don't see how this translates to a "instance dictionary", and why it is different that it is store in the type. What should I read/learn to understand the sense of this ? – Stephane Rolland Jun 17 '18 at 19:06

What does data ... where mean in Haskell?

2 Answers2