<div dir="auto"><div>Hm, yes, I might share Eric's intuition.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">I think I'm starting to get it, though. It originally sounded to me like "forall a ->" was being introduced as a new syntax for function arguments. In fact, it is a new syntax for quantification -- one that happens to borrow the syntax for function application. And well it might, because the sort of quantification it introduces is one that requires passing the name of a type to the function!</div><div dir="auto"><br></div><div dir="auto"><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">Den tors 3 dec. 2020 18:39Eric Seidel <<a href="mailto:eric@seidel.io">eric@seidel.io</a>> skrev:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think the confusion for me is that I've trained myself to think of<br>
`forall` as explicitly introducing an implicit argument, and `->`<br>
as introducing an explicit argument. So the syntax `forall a ->`<br>
looks to me like a contradiction.<br>
<br>
On Thu, Dec 3, 2020, at 10:56, Richard Eisenberg wrote:<br>
> <br>
> <br>
> > On Dec 3, 2020, at 10:23 AM, Bryan Richter <<a href="mailto:b@chreekat.net" target="_blank" rel="noreferrer">b@chreekat.net</a>> wrote:<br>
> > <br>
> > Consider `forall a -> a -> a`. There's still an implicit universal quantification that is assumed, right?<br>
> <br>
> No, there isn't, and I think this is the central point of confusion. A <br>
> function of type `forall a -> a -> a` does work for all types `a`. So I <br>
> think the keyword is appropriate. The only difference is that we must <br>
> state what `a` is explicitly. I thus respectfully disagree<br>
</blockquote></div></div></div>