[ghc-steering-committee] GHC proposal #5

[David Feuer]

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%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 at haskell.org
> | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee