[ghc-steering-committee] GHC proposal #5

[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 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