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

> On Mar 26, 2018, at 2:43 PM, Joachim Breitner <mail@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