<div dir="auto">I do think explaining it relative to the explicit vs implicit arg syntax of agda function argument syntax. </div><div dir="auto"><br></div><div dir="auto">f:  Forall a . B is used with f x. This relates to the new forall -> syntax. </div><div dir="auto"><br></div><div dir="auto">g: forall {c}. D is used either as f or f {x}, aka implicit or forcing it to be explicit.  This maps to our usual Haskell forall with explicit {} being the @ analogue </div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Nov 18, 2020 at 12:09 PM Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Semantically, `forall a -> a -> Int` is the same as `forall a. a -> Int`.  The two only differ in how you use them:<div>  * For the first one, you have to explicitly provide the type to use for `a` at every call site, while</div><div>  * for the second one, you usually omit the type and let GHC infer it.</div><div><br></div><div>So overall I think it's a pretty simple idea. For me it's hard to see that from the text in #281, but I think a lot of the complexity there</div><div>is about a fancy notation for explicitly providing the type at call sites.</div></div><div dir="ltr"><div><br></div><div>-Iavor</div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Nov 18, 2020 at 9:51 AM Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>Hi Bryan,<div><br></div><div>First off, sorry if my first response was a bit snippy -- it wasn't meant to be, and I appreciate the angle you're taking in your question. I just didn't understand it!</div><div><br></div><div>This second question is easier to answer. I say "forall a arrow a arrow Int".</div><div><br></div><div>But I still think there may be a deeper question here left unanswered...</div><div><br></div><div>Richard<br><div><br><blockquote type="cite"><div>On Nov 18, 2020, at 6:11 AM, Bryan Richter <<a href="mailto:b@chreekat.net" target="_blank">b@chreekat.net</a>> wrote:</div><br><div><div dir="ltr"><div dir="auto">Yeah, sorry, I think I'm in a little over my head here. :) But I think I can ask a more answerable question now: how does one pronounce "forall a -> a -> Int"?</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Den tis 17 nov. 2020 16:27Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</a>> skrev:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Bryan,<br>
<br>
I don't think I understand what you're getting at here. The difference between `forall b .` and `forall b ->` is only that the choice of b must be made explicit. Importantly, a function of type e.g. `forall b -> b -> b` can *not* pattern-match on the choice of type; it can bind a variable that will be aliased to b, but it cannot pattern-match (say, against Int). Given this, can you describe how `forall b ->` violates your intuition for the keyword "forall"?<br>
<br>
Thanks!<br>
Richard<br>
<br>
> On Nov 17, 2020, at 1:47 AM, Bryan Richter <<a href="mailto:b@chreekat.net" rel="noreferrer" target="_blank">b@chreekat.net</a>> wrote:<br>
> <br>
> Dear forall ghc-devs. ghc-devs,<br>
> <br>
> As I read through the "Visible 'forall' in types of terms"<br>
> proposal[1], I stumbled over something that isn't relevant to the<br>
> proposal itself, so I thought I would bring it here.<br>
> <br>
> Given<br>
> <br>
>        f :: forall a. a -> a                   (1)<br>
> <br>
> I intuitively understand the 'forall' in (1) to represent the phrase<br>
> "for all". I would read (1) as "For all objects a in Hask, f is some<br>
> relation from a to a."<br>
> <br>
> After reading the proposal, I think my intuition may be wrong, since I<br>
> discovered `forall a ->`. This means something similar to, but<br>
> practically different from, `forall a.`. Thus it seems like 'forall'<br>
> is now simply used as a sigil to represent "here is where some special<br>
> parameter goes". It could as well be an emoji.<br>
> <br>
> What's more, the practical difference between the two forms is *only*<br>
> distinguished by ` ->` versus `.`. That's putting quite a lot of<br>
> meaning into a rather small number of pixels, and further reduces any<br>
> original connection to meaning that 'forall' might have had.<br>
> <br>
> I won't object to #281 based only on existing syntax, but I *do*<br>
> object to the existing syntax. :) Is this a hopeless situation, or is<br>
> there any possibility of bringing back meaning to the syntax of<br>
> "dependent quantifiers"?<br>
> <br>
> -Bryan<br>
> <br>
> [1]: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" rel="noreferrer noreferrer" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281</a><br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" rel="noreferrer" target="_blank">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>
<br>
</blockquote></div>
</div></blockquote></div><br></div></div>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>