[GHC] #3306: Improve syntax for GADT + records

GHC trac at galois.com
Wed Jun 17 15:47:30 EDT 2009


#3306: Improve syntax for GADT + records
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:                  
        Type:  feature request   |       Status:  new             
    Priority:  normal            |    Milestone:                  
   Component:  Compiler          |      Version:  6.10.2          
    Severity:  normal            |   Resolution:                  
    Keywords:                    |   Difficulty:  Unknown         
    Testcase:                    |           Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |  
---------------------------------+------------------------------------------
Old description:

> This [http://www.haskell.org/pipermail/glasgow-haskell-
> users/2009-June/017391.html 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 :: Show a => a } :: RecContTest a
>
> (B)   data RecContTest a where
>          C :: Show a => { showable :: Show a => 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.

New description:

 This [http://www.haskell.org/pipermail/glasgow-haskell-
 users/2009-June/017391.html 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3306#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the Glasgow-haskell-bugs mailing list