8

Is there a difference between these two GADT declarations?

data A a b where
    ...

data A :: * -> * -> * where
    ...
  • 4
    Excellent question. This is a pet peeve of mine -- I always wondered why we need to name the indexes when the names seem to be irrelevant elsewhere. This is very unlike indices vs parameters in the inductive types used in dependent systems like Agda/Coq for instance. – chi Nov 24 '16 at 13:45
  • 2
    Note that, on the contrary, in type families we do have a difference between `type family A :: * -> * -> *` and `type family A a :: * -> *` -- the first one allows instances like `A Int Bool = Char ; A Int Char = Bool` while the latter does not, only allowing e.g. `A Int = Maybe`. (the name `a` is still irrelevant, though in `type family A a :: * -> *`) – chi Nov 24 '16 at 13:51
  • 1
    ...whereas `type family B b :: *` doesn't allow you to use e.g. `MaybeT B a`, which is possible with `type family B :: * -> *`. The former would be a [partial type synonym application](http://stackoverflow.com/a/4923883/745903). (`LiberalTypeSynonyms` can sometimes circumvent this restriction.) – leftaroundabout Nov 24 '16 at 20:21
  • There is a difference with `TypeInType` enabled - you cannot write e.g `X :: (a :: k) -> P a -> *` while `X (a :: k) (p :: P a)` is valid. There is also a difference in terms of which *kind* parameters are actually indices (again only with `TypeInType`) - the declaration `data X0 :: Fin n -> * where X0 :: X0 Fz` is invalid (because the `n` is actually a parameter, and `X0` is not parametric in `n`), while `data X0 (q :: Fin n) where X0 :: X0 Fz` is valid. However, `data X0 :: forall n . Fin n -> *` makes the `n` an index as well. – user2407038 Nov 25 '16 at 00:56
  • Here is another strange discrepancy.. with TypeInType enabled, `data X1 :: k -> *` is parametric on the kind `k`, but without TypeInType, it is indexed on the kind `k`. And yet another... `data X2 :: forall k . k -> forall k' . k' -> *` and `data X2 :: forall k . k -> forall k' . k' -> *` have *completely different kinds* - the judgment `X1 ~ X2` is not even well typed! But it isn't even possible to express `X2` with the first syntax. Everywhere else in Haskell (except perhaps TypeApplications), the order of `forall` bound type variables does not matter. – user2407038 Nov 25 '16 at 01:10
  • 1
    @user2407038 Interesting. I'm not too familiar with the consequences of `TypeInType`. You could turn your comments into an expanded answer. – chi Nov 25 '16 at 10:20

1 Answers1

8

There is no difference. One might think that not mentioning the type variables in the header would be needed to use different names for them in the constructor signatures, as in:

data A :: * -> * -> * where
    AN :: Num x => x -> b -> A x b
    AS :: IsString s => s -> b -> A s b

However, as the GHC Users Guide says...

Unlike a Haskell-98-style data type declaration, the type variable(s) in the data Set a where header have no scope.

... and so this also works:

data A a b where
    AN :: Num x => x -> b -> A x b
    AS :: IsString s => s -> b -> A s b
duplode
  • 33,731
  • 7
  • 79
  • 150
  • 2
    Indeed, I like the first one the most, but always end up writing the second since it's shorter and I'm lazy. I _guess_ it could be useful for documentation to give them evocative names. – chi Nov 24 '16 at 13:48
  • 1
    I prefer the second style because I don't like writing kind signatures. – Benjamin Hodgson Nov 24 '16 at 14:03
  • I guess it would've been possible to omit the type variables from the syntax, but then we would've wanted partial kind signatures. – dfeuer Nov 24 '16 at 19:55