<div dir="ltr"><div dir="ltr">
<br>
> How do you feel about</div><div dir="ltr">></div><div dir="ltr">> > f :: forall (a :: Type) -> a<br>

> or<br>
> > g :: (a :: Type) -> a<br>
</div><div><br></div><div>The former has the same problem as the current syntax. The latter seems better, but then I might be confused again. :)<br></div><div><br></div><div>My main concern is with the choice of keyword. With data, instance, class, module, ..., the pattern is clear: name the sort of thing you are introducing.<br></div><div><br></div><div>forall, on the other hand, doesn't introduce a "forall". It's making explicit the existing universal quantification.</div><div><br></div><div>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.</div><div><br></div><div>I feel like that borrowing introduced a wart.</div><div><br></div><div>Consider `forall a -> a -> a`. There's still an implicit universal quantification that is assumed, right? I.e., this type signature would be valid for all types `a` ? But then how do we make that quantification explicit? `forall a. forall a -> a -> a`? But oops, have we now introduced a new type argument?</div><div><br></div><div>I keep referring to the thing as a "type argument". I know it's hard to introduce a new keyword, but imagine if we had `forall a. typearg a -> a -> a`. It would at least point to its meaning.<br></div><div><br></div><div>I guess that's pretty close to your</div><div><br></div><div>> g :: (a :: Type) -> a</div><div><br></div><div>which is why I think it seems a bit better.<br></div><div><br></div><div><br></div><div><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Nov 20, 2020 at 10:56 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev">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">Hi Bryan,<br>
<br>
Thanks for this longer post -- it's very helpful to see this with fresh eyes.<br>
<br>
<br>
> On Nov 19, 2020, at 2:18 PM, Bryan Richter <<a href="mailto:b@chreekat.net" target="_blank">b@chreekat.net</a>> wrote:<br>
> <br>
> So correct me if I'm wrong: from an implementation perspective,<br>
> `forall a. a -> Int` is a function of two arguments, one of which can<br>
> be elided, while `forall a -> a -> Int` is a function of two<br>
> arguments, all of which must be provided.<br>
<br>
Yes, that's how I read these.<br>
<br>
> <br>
> If that's right, then it bumps into my intuition, which says that the<br>
> former is a function of only one argument. I never thought of `f @Int`<br>
> as partial function application, for instance. :) Is my intuition<br>
> leading me astray? *Should* I consider both functions as having two<br>
> arguments? If so, is that somehow "mathematically true" (a very<br>
> not-mathematical phrase, haha), or is it just an "implementation<br>
> detail"?<br>
<br>
I don't think there's one right answer here. And I'm not quite sure how to interpret "mathematically true". The best I can get is that, if we consider System F (a direct inspiration for Haskell's type system), then both functions really do take 2 arguments (as they do in GHC Core).<br>
<br>
> <br>
> <br>
> So that's one avenue of query I have, but it's actually not the one I<br>
> started off with. Focusing on the simpler case of `forall a -> a`,<br>
> which is a function of one argument, I take issue with how the<br>
> quantification is packed into the syntax for the argument, itself.<br>
> I.e., my intuition tells me this function is valid for all types,<br>
> takes the name of a type as an argument, and returns a value of that<br>
> type, which is three distinct pieces of information. I'd expect a<br>
> syntax like `forall a. elem x a. a -> x`, or maybe `forall a. nameof a<br>
> -> a`. The packing and punning conspire to make the syntax seem overly<br>
> clever.<br>
<br>
How do you feel about<br>
<br>
> f :: forall (a :: Type) -> a<br>
<br>
or<br>
<br>
> g :: (a :: Type) -> a<br>
<br>
Somehow, for me too, having the type of `a` listed makes it clearer. The syntax for f echoes that in Coq, a long-standing dependently typed language, but it uses , instead of ->. The type of `a` is optional. (An implicit parameter is put in braces.) The syntax for g echoes that in Agda and Idris; the type of `a` is not optional. Haskell cannot use the syntax for `g`, because it looks like a kind annotation.<br>
<br>
In the end, I've never loved the forall ... -> syntax, but I've never seen anything better. The suggestions you make are akin to those in <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-727907040" rel="noreferrer" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-727907040</a>. This alternative might work out, but I've never seen this approach taken in another language, and it would be quite different from what we have today.<br>
<br>
<br>
> If I had to explain `forall a -> a` to one of my<br>
> Haskell-curious colleagues, I'd have to say "Oh that means you pass<br>
> the name of a type to the function" -- something they'd have no chance<br>
> of figuring out on their own! The 'forall' comes across as<br>
> meaningless. (Case in point: I had no idea what the syntax meant when<br>
> I saw it -- but I'm already invested enough to go digging.)<br>
<br>
I agree that the new syntax is not adequately self-describing.<br>
<br>
> <br>
> I guess my question, then, is if there is some way to make this syntax<br>
> more intuitive for users!<br>
<br>
I agree! But I somehow don't think separating out all the pieces will make it easier, in the end.<br>
<br>
Richard<br>
<br>
> <br>
> On Wed, Nov 18, 2020 at 10:10 PM Carter Schonwald<br>
> <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:<br>
>> <br>
>> I do think explaining it relative to the explicit vs implicit arg syntax of agda function argument syntax.<br>
>> <br>
>> f:  Forall a . B is used with f x. This relates to the new forall -> syntax.<br>
>> <br>
>> 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<br>
>> <br>
>> On Wed, Nov 18, 2020 at 12:09 PM Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>> wrote:<br>
>>> <br>
>>> Semantically, `forall a -> a -> Int` is the same as `forall a. a -> Int`.  The two only differ in how you use them:<br>
>>>  * For the first one, you have to explicitly provide the type to use for `a` at every call site, while<br>
>>>  * for the second one, you usually omit the type and let GHC infer it.<br>
>>> <br>
>>> 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<br>
>>> is about a fancy notation for explicitly providing the type at call sites.<br>
>>> <br>
>>> -Iavor<br>
>>> <br>
>>> <br>
>>> <br>
>>> 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>
>>>> <br>
>>>> Hi Bryan,<br>
>>>> <br>
>>>> 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!<br>
>>>> <br>
>>>> This second question is easier to answer. I say "forall a arrow a arrow Int".<br>
>>>> <br>
>>>> But I still think there may be a deeper question here left unanswered...<br>
>>>> <br>
>>>> Richard<br>
>>>> <br>
>>>> On Nov 18, 2020, at 6:11 AM, Bryan Richter <<a href="mailto:b@chreekat.net" target="_blank">b@chreekat.net</a>> wrote:<br>
>>>> <br>
>>>> 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"?<br>
>>>> <br>
>>>> Den tis 17 nov. 2020 16:27Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</a>> skrev:<br>
>>>>> <br>
>>>>> 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" 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" 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" 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>
>>>>> <br>
>>>> <br>
>>>> _______________________________________________<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>
>>> <br>
>>> _______________________________________________<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>
>> <br>
>> _______________________________________________<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>
> _______________________________________________<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>
<br>
</blockquote></div></div>