Improve syntax for GADT + records

[simonpj]

This  email thread raised the question of defining data constructors that

• use GADT syntax
• and record syntax
• and have class constraints

This combination isn't supported in GHC 6.10, but it's annoying that it isn't. The problem is just coming up with a plausible syntax. Probably the most plausible possibilities are

(A)   data RecContTest a where
         Show a => C { showable :: a } :: RecContTest a

(B)   data RecContTest a where
         C :: Show a => { showable :: a } -> RecContTest a

The latter (B) looks best to me. I dislike (A) because part of the type (the "Show a =>") occurs before the constructor name C, and part appears after. On the other hand, (B) has something that looks vaguely like a type

   { x::ty, y::ty } -> ty

but that's not really valid type syntax. (Mind you, the ! marks in a constructor signature aren't part of valid types either, so maybe it's not so bad to have a special form in constructor declarations.)

But if we were going to adopt (B), then even when there is no class context we should really say

(B)  data RecTest a where
        B :: { arg :: a } -> RecTest a

rather than the current syntax which is

(A)  data RecTest a where
       B { arg :: a } :: RecTest a

[Note the different placement of the double colon and arrow in (B).]

My take on this

• (B) looks nicer, but it would represent a breaking change
• But perhaps not many people use record-style syntax + GADT-style syntax
• And better to make breaking changes sooner than later

Question for everyone:

• are (A) and (B) the only choices?
• do you agree (B) is best

There are some replies on the above email thread. Please add further opinions as comments to this ticket.

[isaacdupree]

Who implements GHC's version of the syntax currently? GHC and haskell-src-exts, I guess. Both well-maintained.

If we choose (B), I guess the current GADT-records syntax can/should be kept with a 'deprecated' warning for a few releases?

(A) reminds me a little too much of how C tried to make declarations and uses look the same (e.g. function-pointers) and ended up with something nearly incomprehensible!

With (A) and (B), I have a silly question.

data Silly a where
  Silly :: a -> forall b. b -> Silly a
(which would parse like
  Silly :: a -> (forall b. b -> Silly a)
)

Is that allowed or useful? (interacts with impredicativity, IIRC)... Because neither records syntax allows you even to attempt that.

-Isaac

[SamB]

I really don't like the way (B) implies the existance of record types -- unless you would like to add those too?

I am one of those who wants to see the current data type declaration syntax die as soon as reasonably possible, i.e., in H, and do not approve of it's being used as a precedent for anything. In that light, I don't think that (A) looks much like a repeat of C's mistake -- the part to the left of the :: is obviously supposed to be a term. The one issue I have with (A) is the location of the context, and that doesn't seem like a good enough reason to use (B) instead, unless we want to make this possible too:

{ x::ty, y::ty } -> ty

I'll grant that even (B) isn't nearly as bad as what a context on an old-style "data" declaration does, though.

[chak]

I recently needed class constraints in a GADT with record syntax and used (B) with the HEAD. So, there is definitely a need for this.

I definitely prefer (B) out of the two choices listed above. I think it is ok to make a breaking change here. After all, this is very experimental territory still.

[simonpj]

I've mostly implemented this.

Simon

[simonpj]

In fact I'd even committed that patch, so I declare this done:

Thu Jul  2 10:46:57 BST 2009  simonpj@microsoft.com
  * New syntax for GADT-style record declarations, and associated refactoring
  
  The main purpose of this patch is to fix Trac #3306, by fleshing out the
  syntax for GADT-style record declraations so that you have a context in 
  the type.  The new form is
     data T a where
       MkT :: forall a. Eq a => { x,y :: !a } -> T a
  See discussion on the Trac ticket.
  
  The old form is still allowed, but give a deprecation warning.
  
  When we remove the old form we'll also get rid of the one reduce/reduce
  error in the grammar. Hurrah!
  
  While I was at it, I failed as usual to resist the temptation to do lots of
  refactoring.  The parsing of data/type declarations is now much simpler and
  more uniform.  Less code, less chance of errors, and more functionality.
  Took longer than I planned, though.
  
  ConDecl has record syntax, but it was not being used consistently, so I
  pushed that through the compiler.
  

    M ./compiler/deSugar/DsMeta.hs -4 +4
    M ./compiler/hsSyn/Convert.lhs -20 +29
    M ./compiler/hsSyn/HsDecls.lhs -23 +26
    M ./compiler/hsSyn/HsTypes.lhs -2 +21
    M ./compiler/parser/HaddockUtils.hs -6 +5
    M ./compiler/parser/Parser.y.pp -143 +64
    M ./compiler/parser/ParserCore.y -21 +14
    M ./compiler/parser/RdrHsSyn.lhs -188 +205
    M ./compiler/rename/RnHsSyn.lhs +1
    M ./compiler/rename/RnSource.lhs -65 +56
    M ./compiler/rename/RnTypes.lhs -5 +19
    M ./compiler/typecheck/TcHsType.lhs -4 +12
    M ./compiler/typecheck/TcTyClsDecls.lhs -3 +6
    M ./docs/users_guide/glasgow_exts.xml -19 +60

Simon