GADT record syntax and contexts

[Simon Peyton-Jones]

Philip

Thanks for your msg (which appears in full below for reference.)

| data RecContTest a where
|   C { showable :: Show a => a } :: RecContTest a

This definitely isn't going to work: it declares the 'showable' field to be a function that *requires* a Show context, not one that *provides* a Show context.

| type a in function c. My definition of RecContTest is the only
| syntactical form I could come up with that GHC accepts. Is there a
| syntax for what I want here?

Not at the moment, I'm afraid.  The problem is mainly to find a decent syntax -- and that problem made me simply omit it altogether.  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

Simon


| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Philip K.F. Hölzenspies
| Sent: 15 June 2009 11:09
| To: glasgow-haskell-users at haskell.org
| Subject: GADT record syntax and contexts
| 
| Dear GHCers,
| 
| Maybe this question is more for Haskell-cafe, but since it involves
| language extensions as provided by GHC, it seems reasonable to post it
| here.
| 
| The GHC user guide lists under 7.4 [1] the extensions to data types and
| type synonyms. My question involves 7.4.5 (although the overlap with
| 7.4.6 is considerable; maybe the two should be merged). A property of
| GADTs that I really appreciate is the fact that constructor contexts are
| made available by pattern matching (I don't quite understand why normal
| ADTs could do this, btw, but that's another question). The problem I
| have now, though, is that there doesn't seem to be a syntax to combine
| contexts and records in GADTs. Consider this program:
| 
| data ContTest a where
|   A :: Show a => a -> ContTest a
| 
| data RecTest a where
|   B { arg :: a } :: RecTest a
| 
| data RecContTest a where
|   C { showable :: Show a => a } :: RecContTest a
| 
| a :: ContTest a -> String
| a (A a) = show a
| 
| b :: Show a => RecTest a -> String
| b = show . arg
| 
| c :: RecContTest a -> String
| c (C { showable = x }) = show x
| 
| Both ContTest and RecTest work swimmingly (with functions a and b,
| respectively). However, GHC complains that it can not deduce Show for
| type a in function c. My definition of RecContTest is the only
| syntactical form I could come up with that GHC accepts. Is there a
| syntax for what I want here?
| 
| Regards,
| Philip
| 
| 
| 
| PS. As a side-note. In section 7.4.5, the manual states that:
| 
| "At the moment, record updates are not yet possible with GADT-style
| declarations, so support is limited to record construction, selection
| and pattern matching."
| 
| However, if I add:
| 
| update org@(B {}) x = org { arg = x }
| 
| and evaluate "b $ update (B True) False" the response is "False" as one
| would expect. Is this line in the user guide outdated, or is support for
| updates unstable or partial?
| 
| 
| [1]http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html