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

[Joachim Breitner]

Hi,

without adding much to the discussion, I agree with Roman’s sentiment
here. And maybe that is an indication that more people out there, who
are not as deep into the theory and implementation of this feature,
will be similarly surprised.

Am Montag, den 26.03.2018, 09:24 +0000 schrieb Simon Peyton Jones:
> Also, you can readily do what you want with an ordinary type
> signature in a pattern
>            
> h (C n :: C Int) = n      -- infers h :: C Int -> Int

Isn’t that true for most uses of TypeApplications in expressions as
well, that they could readily be replaced by type signatures? And yet
we offer the TypeApplications extension?

Here is another example where the current proposal superficially breaks
the nice equational nature of Haskell:

   data U a where MkU :: forall a b. Show a => b -> T a

   idU :: forall a. U a -> U a
   idU (MkU @b x) = MkU @a @b x

or even

   idU :: forall a. U a -> U a
   idU (MkU @b x) = MkU @a x

It is the identity! Why don’t I write the same things on both sides?


I think all reserverations would disappear if we can find a good syntax
for existential type variable that does not clash with
TypeApplication. 

Maybe @? instead of @ (given that ? is commonly used to refer to ∃)?

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/20180326/4ac5422f/attachment.sig>