[ghc-steering-committee] GHC proposal #5
David Feuer
david.feuer at gmail.com
Tue May 30 14:21:51 UTC 2017
All right. I don't personally think this should block implementation, but
I'll otherwise go ahead with the process you suggest.
On May 30, 2017 9:54 AM, "Richard Eisenberg" <rae at cs.brynmawr.edu> wrote:
> I'm afraid I think the best way to have this discussion is to submit
> another proposal. Is there a Trac ticket for the first one? That ticket
> should track implementation, and we could put a note there saying not to
> implement, pending the new proposal.
>
> Why do I want yet more process? Because I'm worried about having design
> conversations "behind closed doors", as doing so can be exclusionary. My
> other motivation is that I initially agree with Simon and say "no" -- but I
> want to give you a chance to convince me. Your best opportunity will be to
> get others to agree with you. Incidentally, my suggestion here agrees with
> what has been said on the initial pull request.
>
> Richard
>
> On May 26, 2017, at 2:58 PM, David Feuer <david.feuer at gmail.com> wrote:
>
> 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
>>
>>
>> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20170530/5e18bdbf/attachment-0001.html>
More information about the ghc-steering-committee
mailing list