GADT record syntax and contexts

[Philip Hölzenspies]

Dear Simon and fellow GHCers,

Thank you for having a look at this. I've inlined my response with  
your message.


> | 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.


Absolutely. Like I said, I committed the sin of hacking until GHC  
stopped complaining. At some point, I turned off the semantics in my  
head ;)


> 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


I presume there's a little copy-paste mishap going on here and that  
you mean:

(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.)


I'm afraid I'm not too well informed with regards to type syntax, but  
another reason to prefer B over A is that it looks much more like a  
normal function declaration. When I explain GADTs and their syntax to  
people that haven't used them before, I usually start off by saying  
that constructors are simply functions. With GADTs, the declarations  
of the constructors look exactly like those of functions, but you  
don't have to worry about providing a binding.


> 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).]


Again, B is much more in-sync with "normal GADTs" (i.e. non-record  
syntax) and with the perspective of constructors-as-functions I  
mentioned above. The record parts of B don't seem to be function-like,  
but it is how I would define functions on extensible records  
(regardless of the current status of different implementations /  
alternatives). To me, this

foo :: { bar :: Bool, tutu :: Int } -> String

means that foo is a function on any record that contains at least the  
fields bar and tutu of the mentioned types.


> 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


One very important reason for me to use GADTs nowadays, is that they  
provide contexts in pattern matches. If normal ADTs were to do the  
same, I would use far less GADTs. Record syntax just makes sense when  
you stick more than three arguments in a constructor. Having said  
that, *every* ADT seems to be a record in GHC:

data FooBar = Foo Int Int | Bar Char

isFoo Foo {} = True
isFoo _ = False



Rounding up; B has my strong preference over A. I don't know whether  
very strong alternatives will present themselves, but B seems quite  
nice in general.

Regards,
Philip