[ghc-steering-committee] Proposal: Binding existential type variables (#96)

[Simon Peyton Jones]

| great! I like it: It is no less expressive than the original proposal,
| but forward-compatible to the full version of my proposal (which allows
| types, not just type variables).

I'm *much* less keen on the "full version". But I could get behind this more modest version.

Would someone like to communicate something clear back to the author(s).

Simon


| -----Original Message-----
| From: ghc-steering-committee <ghc-steering-committee-
| bounces at haskell.org> On Behalf Of Joachim Breitner
| Sent: 28 March 2018 16:26
| To: ghc-steering-committee at haskell.org
| Subject: Re: [ghc-steering-committee] Proposal: Binding existential type
| variables (#96)
| 
| Hi,
| 
| 
| Am Dienstag, den 27.03.2018, 21:53 +0000 schrieb Simon Peyton Jones:
| > Interesting idea from Joachim.  But it's quite complicated.
| > Here is a much simpler version.
| 
| great! I like it: It is no less expressive than the original proposal,
| but forward-compatible to the full version of my proposal (which allows
| types, not just type variables). I believe we will want the full
| version eventually (Both to say `foo (Nothing @Int) = …` and once we
| have matchable implicit argument – right, Richard?), but we don’t have
| to do both steps at once.
| 
| May I add one constraint to the simpler alternative proposal:
| 
|      It is an error to @-bind a type variables that would shadow
|      type variable that is already in scope (whether from
|      ScopedTypeVariables, from an instance head or from a @-binder).
| 
| 
| Why? Well, for forward compatibility. But also for consistency! To our
| users (or, at least to me) these two expressions are different ways of
| writing the same things:
| 
|   foo1, foo1' :: forall a. a -> Int
|   foo1  x = length (Nothing :: Maybe a)
|   foo1' x = length (Nothing @ a)
| 
| I.e. TypeApplication is just a more convenient alternative to type
| signatures.
| 
| The same is true, in patterns, under your simplified alternative
| proposal:
| 
|   foo2, foo2' :: a -> Maybe Int -> Int
|   foo2  _ (Nothing :: Maybe a) = 42
|   foo2' _ (Nothing @ a)        = 42
| 
| In both forms, a is bound by the pattern (and `a ~ Int` is added to the
| context).
| 
| But note that a change somewhere else (and it could be arbitrarily far
| away if `foo2` is a local function) breaks the symmetry, at least with
| ScopedTypeVariables enabled:
| 
|   foo3, foo3' :: forall a. a -> Maybe Int -> Int
|   foo3  _ (Nothing :: Maybe a) = 42 -- type error (a ≠ Int)
|   foo3' _ (Nothing @ a)        = 42 -- shadows a
| 
| Hence I would ask to simply forbid the latter form in the simplified
| version of the proposal. This
|  * helps the user not shooting in his own leg and
|  * is compatible with the full proposal, where
|    foo3 and foo3' would be equivalent.
| 
| 
| Cheers,
| Joachim
| --
| Joachim Breitner
|   mail at joachim-breitner.de
| 
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joac
| him-
| breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cf159ca2e41fd41ca
| b59d08d594c04f60%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6365784760
| 41656384&sdata=FepuCZE2%2FlQMlBssUMTyHEBmFoyjAVXY%2FXJrsdUxd6Q%3D&reserv
| ed=0