GADT record syntax and contexts
Philip Hölzenspies
p.k.f.holzenspies at utwente.nl
Tue Jun 16 08:45:10 EDT 2009
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
More information about the Glasgow-haskell-users
mailing list