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

[Eric Seidel]

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 <iavor.diatchki at gmail.com> 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 at haskell.org <mailto:ghc-steering-committee%40haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>