| 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@haskell.org> On Behalf Of Joachim Breitner | Sent: 28 March 2018 16:26 | To: ghc-steering-committee@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@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