[ghc-steering-committee] GHC proposal #5

Fri May 26 18:58:21 UTC 2017

I thought of something that coops be a good compromise. You could require
the signatures to be the same, modulo constraints, unless another extension
allowed equality constraints. So using just PatternSynonyms, only
"sensible" types would occur, but adding GADTs or TypeFamilies would let
the signatures be totally wild.

On May 26, 2017 9:10 AM, "David Feuer" <david.feuer at gmail.com> wrote:

> I really am advocating allowing that, although I don't believe any library
> writer should write such a ridiculous pattern. Here's my reasoning. The
> proposal, even with the restriction, fundamentally adds expressiveness to
> the pattern synonym extension. This is a good thing, because it allows
> people to write substantially more useful patterns than they can today. As
> soon as you add expressiveness, I think it makes sense to see just how much
> you've added. As I've demonstrated, it seems that the restricted proposal
> adds enough power to allow effectively unrelated pattern and builder
> signatures. That is, the restriction doesn't really seem to restrict! So it
> seems primarily to serve to punish anyone who wants to do something too
> weird by making weird things inconvenient and ugly, which doesn't seem very
> valuable to me.
>
> Note: I really want this proposal to go through, even if restricted; I
> just don't see the wisdom of the restriction.
>
> David
>
> On May 26, 2017 8:54 AM, "Simon Peyton Jones" <simonpj at microsoft.com>
> wrote:
>
> Are you really advocating NO restrictions?  Eg
>
> pattern P :: Int -> Maybe Int
> pattern P x = Just w
>   where
>      P :: Char -> Int
>      P x = ord x
>
> This seems deeply peculiar to me.  No value produced by an expression
> using P can be consumed by a pattern matching on P.
>
> My instinct is always to accept /fewer/ programs to start with, and expand
> in response to demand, rather than the reverse.
>
> I don't feel qualified to judge how convincing the lens example is.
>
>
> |  Pattern synonyms are fundamentally about *syntax*. While particular
> |  use cases provide the motivation to have them, users are free to do
> |  with them as they will. I tend to think that a pattern synonym should
>
> I don't agree.  A pattern synonym introduces an abstraction, and so far as
> possible we should be able to reason about it without looking inside it. We
> can't check that matching and construction are mutually inverse, but
> usually they should be.  Familiar laws should hold, so that
>    case P e of P y -> rhs
> means the same as
>    let y=e in rhs
> It's hard to enforce that, but I'd like to nudge programmers firmly in
> that direction.
> So I'm not convinced.  What about others.
>
> Simon
>
>
> |  -----Original Message-----
> |  From: David Feuer [mailto:david.feuer at gmail.com]
> |  Sent: 26 May 2017 00:08
> |  To: Simon Peyton Jones <simonpj at microsoft.com>
> |  Cc: ghc-steering-committee at haskell.org
> |  Subject: Re: [ghc-steering-committee] GHC proposal #5
> |
> |  The reason I did not include the lens example in the original proposal
> |  is that I hadn't thought of it by then.
> |  I had the nagging feeling that I (or someone else) would eventually
> |  find a motivating example, but I didn't manage to come up with a
> |  sufficiently realistic one until last night.
> |  I'm sorry about that. As for your
> |  questions:
> |
> |  1. As I stated in the original pull request, before I was asked to
> |  modify it, I believe that the type signatures should not have any
> |  restrictions whatsoever. As the first example in my last email
> |  demonstrates, it seems impossible to actually preclude "unreasonable"
> |  pairs of signatures while still accomplishing the basic objectives. I
> |  don't think mismatched signatures are likely ever to be common, but I
> |  don't think making them harder to write and harder to read serves any
> |  obvious purpose. In the case of DefaultSignatures, there was
> |  apparently a compelling reason to impose a similar restriction to make
> |  correct implementation feasible.
> |  I am not aware of any similar reason in this case. Should one arise, I
> |  will certainly accept the restriction.
> |
> |  2. The ALens/Lens -> ReifiedLens pattern in my last email strikes me
> |  as a decent example: it may reasonable in some cases for pattern
> |  matching to provide a value with a type that subsumes the type
> |  required to apply the builder.
> |
> |  I imagine it might sometimes be useful to go in the opposite
> |  direction, but I haven't been able to find a good example of that yet.
> |  Intuitively, one possible direction an example might take would be a
> |  builder that requires its argument to be polymorphic in order to make
> |  some guarantee by parametricity, with an efficient monomorphic
> |  representation that can only provide a monomorphic pattern.
> |
> |  A final thought, for now:
> |
> |  Pattern synonyms are fundamentally about *syntax*. While particular
> |  use cases provide the motivation to have them, users are free to do
> |  with them as they will. I tend to think that a pattern synonym should
> |  always be cheap, both when building and when matching. Others
> |  disagree. I would be very much opposed to any attempt to restrict
> |  pattern synonyms to cheap operations, as a matter of principle. I
> |  similarly believe that building and matching should never throw
> |  exceptions or fail to terminate when given non-bottom input, but would
> |  oppose attempts to enforce such a law. In the present instance, I ask
> |  you to set aside how you think pattern synonyms and builders *should*
> |  relate in type, and to consider instead whether they really must.
> |
> |  Thanks,
> |  David
> |
> |  On Thu, May 25, 2017 at 5:57 PM, Simon Peyton Jones
> |  <simonpj at microsoft.com> wrote:
> |  > So what do you propose?  The current rendered proposal has many
> |  alternatives, so I don't know what you propose.
> |  >
> |  > Moreover, all the example you give in the proposal /do/ obey the
> |  restriction; and all the /motivation/ in the proposal concerns
> |  variations in the constraints due to extra constraints required for
> |  pattern matching.
> |  >
> |  > So:
> |  >
> |  > * What proposal do you advocate? In particular...
> |  > * What restrictions -- if any! -- must the two type signatures
> |  satisfy
> |  > * What examples motivate whatever extra flexibility you advocate?
> |  >
> |  > Simon
> |  >
> |  > | -----Original Message-----
> |  > | From: ghc-steering-committee [mailto:ghc-steering-committee-
> |  > | bounces at haskell.org] On Behalf Of David Feuer
> |  > | Sent: 25 May 2017 06:28
> |  > | To: ghc-steering-committee at haskell.org
> |  > | Subject: [ghc-steering-committee] GHC proposal #5
> |  > |
> |  > | GHC proposal  #5 [*], which I drafted, was recently merged. I was
> |  > | asked to modify the proposal to restrict the type signatures of
> |  > | patterns and builders to be the same, except for their contexts. I
> |  > | would like to make one last plea to remove this restriction,
> |  unless
> |  > | there are fundamental reasons it cannot be done. The reasons are
> |  as follows.
> |  > |
> |  > | 1. Despite the restriction, it remains possible, at least in many
> |  > | cases, to achieve exactly the same effect, albeit in a manner that
> |  > | is considerably more difficult to read. For example, one could
> |  write
> |  > | the following (ill-advised) pattern:
> |  > |
> |  > | pattern Ha :: a ~ Int => Word -> a
> |  > | pattern Ha x <- (fromIntegral -> x)
> |  > |   where
> |  > |     Ha :: a ~ (Word -> Word) => Word -> a
> |  > |     Ha x = (x +)
> |  > |
> |  > | which, after more thinking than one might wish to apply, turns out
> |  > | to mean
> |  > |
> |  > | pattern Ha :: Word -> Int
> |  > | pattern Ha x <- (fromIntegral -> x)
> |  > |   where
> |  > |     Ha :: Word -> Word -> Word
> |  > |     Ha x = (x +)
> |  > |
> |  > | 2. It would be *extremely unpleasant* to make this trick work with
> |  > | RankNTypes, where such mismatched signatures seem likely to have
> |  the
> |  > | most practical value. For example, suppose I want to write
> |  > |
> |  > | import Control.Lens
> |  > | import Control.Lens.Reified
> |  > |
> |  > | pattern Package :: Lens s t a b -> ReifiedLens s t a b pattern
> |  > | Package f
> |  > | <- Lens f
> |  > |   where
> |  > |     Package :: ALens s t a b -> ReifiedLens s t a b
> |  > |     Package f = Lens $ cloneLens f
> |  > |
> |  > | This convenience pattern would pack up an ALens into a
> |  ReifiedLens;
> |  > | when unpacked, I'd get back a full Lens (The type Lens s t a b
> |  > | subsumes the type ALens s t a b). Without being able to use those
> |  > | different type signatures, I'd have to write something like this
> |  > | monstrosity:
> |  > |
> |  > | import Control.Lens.Internal.Context -- additionally
> |  > |
> |  > | pattern Package :: c ~ Functor
> |  > |                => (forall f. c f => LensLike f s t a b)
> |  > |                -> ReifiedLens s t a b pattern Package f <- Lens f
> |  > |   where
> |  > |     Package :: c ~ ((~) (Pretext (->) a b))
> |  > |            => (forall f. c f => LensLike f s t a b)
> |  > |            -> ReifiedLens s t a b
> |  > |     Package f = Lens $ cloneLens f
> |  > |
> |  > | I pity the poor soul who has to try to reverse engineer what those
> |  > | signatures are supposed to mean!
> |  > |
> |  > | While it's certainly possible to implement the restricted version
> |  > | now and expand it later, that would add *yet another*
> |  > | PatternSynonyms change for users to hack around with CPP. I hope
> |  > | you'll reconsider that decision in light of these examples.
> |  > |
> |  > | Thank you for your time,
> |  > | David Feuer
> |  > |
> |  > |
> |  > | [*]
> |  > |
> |  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgit
> |  > | hub.c
> |  > | om%2Fghc-proposals%2Fghc-
> |  proposals%2Fblob%2Fmaster%2Fproposals%2F000
> |  > | 5-
> |  > | bidir-constr-
> |  > |
> |  sigs.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C8f0f0cb282eb4990ce
> |  > | 1308d
> |  > |
> |  4a3b0fa63%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6363134278964
> |  > | 69235
> |  > | &sdata=pbr9v2OY4hhg5qmZNA9rEOBnbO5ttZG%2BDtvzbEUSNnI%3D&reserved=0
> |  > | _______________________________________________
> |  > | ghc-steering-committee mailing list
> |  > | ghc-steering-committee at haskell.org
> |  > | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-
> |  commi
> |  > | ttee
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20170526/0f9f6427/attachment.html>