Re: [ghc-steering-committee] Proposal #402 (changes to GADT syntax); rec: accept

My intuition behind GADT syntax has always been that it looks like type syntax because sometimes we really just want to write down the constructor's type. The original motivation was to let us specify the result type, but this proposal gives us another reason around controlling the placement of foralls. If GADT signatures are supposed to feel like types, then we should seek to minimize the differences. That would mean keeping optional parens and allowing control over the placement of foralls. Iavor's example of type synonyms is another inconsistency that doesn't seem to be motivated by a technical reason. On the other hand, if we want to convey that GADTs signatures are not types, then we should not reuse the `->`. We could instead write something like data T a where C1 Int :: T Int C2 !Bool :: T Bool C3 { a :: Int, b :: !Bool } :: T (Int, Bool) Those signatures are very clearly not types. Eric On Fri, Mar 19, 2021, at 14:38, Richard Eisenberg wrote:

...

On Mar 19, 2021, at 12:18 PM, Iavor Diatchki wrote:

type T = Int -> S data S where C :: T

It's true that this doesn't work today -- and that there are no plans for something like that working. If we were clearer that constructor signatures weren't types, then this case would be easier to understand. Perhaps this is why I'm in favor of dropping the parentheses; allowing them is actually an exception to the general rule here. (The general rule: the thing after the :: is a `->`-separated list of arguments, terminated by the return type.)

Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee%40haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee