<div dir="auto"><div>There is no *implicit* universal quantification in that example, but there is an explicit quantifier. It is written as follows:<div dir="auto"><br></div><div dir="auto">  forall a -></div><div dir="auto"><br></div><div dir="auto">which is entirely analogous to:</div><div dir="auto"><br></div><div dir="auto">  forall a.</div><div dir="auto"><br></div><div dir="auto">in all ways other than the additional requirement to instantiate the type vatiable visibly at use sites.</div><div dir="auto"><br></div><div dir="auto">- Vlad</div><br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Dec 3, 2020, 19:12 Bryan Richter <<a href="mailto:b@chreekat.net">b@chreekat.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div>I must be confused, because it sounds like you are contradicting yourself. :) In one sentence you say that there is no assumed universal quantification going on, and in the next you say that the function does indeed work for all types. Isn't that the definition of universal quantification?</div><div dir="auto"><br></div><div dir="auto">(We're definitely getting somewhere interesting!)</div><div dir="auto"><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">Den tors 3 dec. 2020 17:56Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank" rel="noreferrer">rae@richarde.dev</a>> skrev:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><br><div><br><blockquote type="cite"><div>On Dec 3, 2020, at 10:23 AM, Bryan Richter <<a href="mailto:b@chreekat.net" rel="noreferrer noreferrer" target="_blank">b@chreekat.net</a>> wrote:</div><br><div><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline!important">Consider `forall a -> a -> a`. There's still an implicit universal quantification that is assumed, right?</span></div></blockquote></div><br><div>No, there isn't, and I think this is the central point of confusion. A function of type `forall a -> a -> a` does work for all types `a`. So I think the keyword is appropriate. The only difference is that we must state what `a` is explicitly. I thus respectfully disagree with</div><div><br></div><div><blockquote type="cite">But somewhere, an author decided to reuse the same keyword to herald a type argument. It seems they stopped thinking about the meaning of the word itself, saw that it was syntactically in the right spot, and borrowed it to mean something else.</blockquote><br></div><div>Does this help clarify? And if it does, is there a place you can direct us to where the point could be made more clearly? I think you're far from the only one who has tripped here.</div><div><br></div><div>Richard</div></div></blockquote></div></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank" rel="noreferrer">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div></div>