My question comes for the fact that I don't fully understand the nuances of declaring datatypes. I think I get lost in all the degrees of freedom out there: do I use GADT syntax or not? Do I spell out the kind signature of type ctor, or the kind of the type paremeter(s) of the type ctor?
Below is an example where it's natural for me to ask "what's the difference between these syntaxes?"
This tutorial on singletons features this code snippet demonstrating how to declare a dataype with a phantom type parameter:
data Door (s :: DoorState) = UnsafeMkDoor { doorMaterial :: String }
and later it gives an alternative way of writing that, using GADT syntax:
data Door :: DoorState -> Type where
UnsafeMkDoor :: { doorMaterial :: String } -> Door s
The way I understand it, both forms encode that
Dooris aTypector- the latter form explicitly via the
-> Type, - the former by virtue of providing a data contructor to form terms, and if something has a term, then it is a
Type;
- the latter form explicitly via the
the
Doortype ctor is unary and accepts a type of kindDoorState.
But I could also re-write the above like this:
data Door (s :: DoorState) where
UnsafeMkDoor :: { doorMaterial :: String } -> Door s
which feels like being in the middle of those two, in the sense that it uses where, just like the GADT syntax does, but it explicitly mentions the type parameter of Door, naming it s and annotating it with :: DoorState, just like the non-GADT syntax does.
Crucially, the latter s does not refer to the former, but still, is this way of defining Door fundamentally different in any way?
I suppose seeing the grammar of ADTs and GADTs would probably be helpful, but I'm not sure where to look for it. Once I incidentally asked, and the answer was that the Haskell Report is the canonical specification, but that is as long as one stays Haskell2010, which is not the case with the extensions that the code snippets above assume.
