
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://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0005-bi...

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@haskell.org] On Behalf Of David Feuer | Sent: 25 May 2017 06:28 | To: ghc-steering-committee@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%2Fgithub.c | om%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0005- | bidir-constr- | sigs.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C8f0f0cb282eb4990ce1308d | 4a3b0fa63%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636313427896469235 | &sdata=pbr9v2OY4hhg5qmZNA9rEOBnbO5ttZG%2BDtvzbEUSNnI%3D&reserved=0 | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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
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@haskell.org] On Behalf Of David Feuer | Sent: 25 May 2017 06:28 | To: ghc-steering-committee@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%2Fgithub.c | om%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0005- | bidir-constr- | sigs.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C8f0f0cb282eb4990ce1308d | 4a3b0fa63%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636313427896469235 | &sdata=pbr9v2OY4hhg5qmZNA9rEOBnbO5ttZG%2BDtvzbEUSNnI%3D&reserved=0 | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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@gmail.com]
| Sent: 26 May 2017 00:08
| To: Simon Peyton Jones

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"

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"
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"
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@gmail.com] | Sent: 26 May 2017 00:08 | To: Simon Peyton Jones
| Cc: ghc-steering-committee@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 | 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@haskell.org] On Behalf Of David Feuer | > | Sent: 25 May 2017 06:28 | > | To: ghc-steering-committee@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@haskell.org | > | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | commi | > | ttee

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
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"
mailto:david.feuer@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"
mailto:simonpj@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@gmail.com mailto:david.feuer@gmail.com] | Sent: 26 May 2017 00:08 | To: Simon Peyton Jones
mailto:simonpj@microsoft.com> | Cc: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@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 | mailto:simonpj@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- mailto:ghc-steering-committee- | > | bounces@haskell.org mailto:bounces@haskell.org] On Behalf Of David Feuer | > | Sent: 25 May 2017 06:28 | > | To: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@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 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 http://40microsoft.com/%7C8f0f0cb282eb4990ce | > | 1308d | > | | 4a3b0fa63%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6363134278964 | > | 69235 | > | &sdata=pbr9v2OY4hhg5qmZNA9rEOBnbO5ttZG%2BDtvzbEUSNnI%3D&reserved=0 | > | _______________________________________________ | > | ghc-steering-committee mailing list | > | ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org | > | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | commi | > | ttee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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"
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
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"
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"
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@gmail.com] | Sent: 26 May 2017 00:08 | To: Simon Peyton Jones
| Cc: ghc-steering-committee@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 | 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@haskell.org] On Behalf Of David Feuer | > | Sent: 25 May 2017 06:28 | > | To: ghc-steering-committee@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@haskell.org | > | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | commi | > | ttee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
participants (3)
-
David Feuer
-
Richard Eisenberg
-
Simon Peyton Jones