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

[Roman Leshchinskiy]

On Mon, Mar 26, 2018 at 9:28 PM, Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

>
>
> > On Mar 26, 2018, at 2:43 PM, Joachim Breitner <mail at joachim-breitner.de>
> wrote:
>
> > 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.)
>
> And I'd say that @ should bind existentials, for consistency with the
> usual default for patterns, which is the "output" mode. Besides, I think
> binding existentials will be much more common than instantiating universals.
>

The point about inputs vs. outputs to patterns has clarified things a lot
for me, thanks! I think that if we ever want to allow inputs to patterns,
we could just use a reserved token to separate those (assuming all inputs
come before the outputs). Something like this (\ already means "here come
binders"):

  C <inputs> \ <outputs>

Then @ would instantiate universals before \ and bind existentials after
and \ could be omitted if there are no inputs, thus subsuming the current
pattern syntax.

In any event, this convinces me that we won't be irrevocably taking away
syntax which might prove essential in the future and I now support the
proposal.

Roman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180326/aa25b912/attachment.html>