GADT record syntax and contexts
Simon Peyton-Jones
simonpj at microsoft.com
Tue Jun 16 05:19:50 EDT 2009
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
More information about the Glasgow-haskell-users
mailing list