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

[Joachim Breitner]

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
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180328/fedf417f/attachment.sig>