Concrete syntax for pattern synonym type signatures

[Edward Kmett]

Lamely, I can't seem to reconstruct the problem.

GHC seems to be more careful about gathering the constraints up into a
tuple even when I give an explicit type signature involving nested contexts
nowadays.

-Edward

On Mon, Nov 10, 2014 at 4:07 PM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

>   Note though, it doesn't mean the same thing to say (Foo a, Bar a b) =>
> ... as it does to say
>
> Foo a => Bar a b => ...
>
> The latter can use Foo a when working on Bar a b, but not Bar a b to
> discharge Foo a, which makes a difference when you have functional
> dependencies.
>
>
>
> I disagree.  Can you offer a concrete example, and show that one
> typechecks when the other does not?
>
>
>
> Simon
>
>
>
> *From:* Edward Kmett [mailto:ekmett at gmail.com]
> *Sent:* 10 November 2014 15:46
> *To:* Richard Eisenberg
> *Cc:* Simon Peyton Jones; GHC Devs
> *Subject:* Re: Concrete syntax for pattern synonym type signatures
>
>
>
> Note though, it doesn't mean the same thing to say (Foo a, Bar a b) => ...
> as it does to say
>
>
>
> Foo a => Bar a b => ...
>
>
>
> The latter can use Foo a when working on Bar a b, but not Bar a b to
> discharge Foo a, which makes a difference when you have functional
> dependencies.
>
>
>
> So in some sense the 'pattern requires/supplies' split is just that.
>
>
>
>
>
>
>
> That said, Richard's other option
>
>
>
> pattern Foo a => P :: Bar a => a
>
>
>
> has the benefit that it looks a bit like the old datatype contexts (but
> here applied to the constructor/pattern).
>
>
>
> If we expect the left hand side or the right hand side to be most often
> trivial then that may be worth considering.
>
>
>
> You'd occasionally have things like
>
>
>
> pattern (Num a, Eq a) => Foo :: a
>
>
>
> for
>
>
>
> pattern Foo = 8
>
>
>
> but most of the time they'd wind up just looking like a GADT constructor.
>
>
>
> -Edward
>
>
>
> On Sun, Nov 9, 2014 at 10:02 PM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
>
>
> On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
> >
> > * One other possibility would be two => thus
> >       pattern P :: (Eq b) => (Num a, Eq a) => ...blha...
> >
>
> I should note that I can say this in 7.8.3:
>
> foo :: Show a => Eq a => a -> String
> foo x = show x ++ show (x == x)
>
> Note that I've separated the two constraints with a =>, not a comma. This
> syntax does what you might expect. (I actually believe that this is an
> improvement over the conventional syntax, but that's a story for another
> day.) For better or worse, this trick does not work for GADT constructors
> (which is a weird incongruence with function type signatures), so adding
> the extra arrow does not really steal syntax from GADT pattern synonyms.
>
> Richard
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141111/e5b28b0c/attachment-0001.html>