<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Mar 26, 2018 at 9:28 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
<br>
> On Mar 26, 2018, at 2:43 PM, Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>> wrote:<br>
<br>
> And once we have syntax to instantiate universals and bind<br>
> existentials, there is the question, which of these two deserves @ and<br>
> which has to get the yet-to-be-found other one. (Personally, I’d say<br>
> that @ should instantiate universals, for consistency with<br>
> TypeApplications, but will not insist on this point.)<br>
<br>
</span>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.<br></blockquote><div><br></div><div>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"):</div><div><br></div><div>  C <inputs> \ <outputs></div><div><br></div><div>Then @ would instantiate universals before \ and bind existentials after and \ could be omitted if there are no inputs, thus subsuming the current pattern syntax.</div><div><br></div><div>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.</div><div><br></div><div>Roman</div></div><br></div><div class="gmail_extra"><br></div></div>