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

[Joachim Breitner]

Hi,

Am Montag, den 26.03.2018, 14:34 -0400 schrieb Richard Eisenberg:
> Bringing this back to the proposal at hand, we would say this to
> mention a universal:
> 
> g (Just *@Int x) = x
> 
> and that would mean g :: Maybe Int -> Int

Yes! Something like that and I would fully support the proposal. But

> Of course, these little syntactic sigils make Haskell look more
> Perlish, and that's not a good thing.

is spot-on, and finding a good syntax is the hard part here.

And once we have syntax to instantiate universals and bind
existentials, there is the question, which of these two deserves @ and
which has to get the yet-to-be-found other one. (Personally, I’d say
that @ should instantiate universals, for consistency with
TypeApplications, but will not insist on this point.)



Somewhat tangentially, how much should it worry us that according to
the current proposal, in

  type Id a = a
  data Foo  a where MkFoo  :: forall a,  a -> Foo a
  data Foo' a where MkFoo' :: forall a,  a -> Foo (Id a)

the constructors MkFoo and MkFoo' behave totally different wrt
universals and existentials? I see the technical justification for it,
but it still feels odd and unsmooth.


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/17016887/attachment.sig>