Use of forall as a sigil

Fri Nov 20 20:56:03 UTC 2020

Hi Bryan,

Thanks for this longer post -- it's very helpful to see this with fresh eyes.

> On Nov 19, 2020, at 2:18 PM, Bryan Richter <b at chreekat.net> wrote:
> 
> So correct me if I'm wrong: from an implementation perspective,
> `forall a. a -> Int` is a function of two arguments, one of which can
> be elided, while `forall a -> a -> Int` is a function of two
> arguments, all of which must be provided.

Yes, that's how I read these.

> 
> If that's right, then it bumps into my intuition, which says that the
> former is a function of only one argument. I never thought of `f @Int`
> as partial function application, for instance. :) Is my intuition
> leading me astray? *Should* I consider both functions as having two
> arguments? If so, is that somehow "mathematically true" (a very
> not-mathematical phrase, haha), or is it just an "implementation
> detail"?

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).

> 
> 
> So that's one avenue of query I have, but it's actually not the one I
> started off with. Focusing on the simpler case of `forall a -> a`,
> which is a function of one argument, I take issue with how the
> quantification is packed into the syntax for the argument, itself.
> I.e., my intuition tells me this function is valid for all types,
> takes the name of a type as an argument, and returns a value of that
> type, which is three distinct pieces of information. I'd expect a
> syntax like `forall a. elem x a. a -> x`, or maybe `forall a. nameof a
> -> a`. The packing and punning conspire to make the syntax seem overly
> clever.

How do you feel about

> f :: forall (a :: Type) -> a

or

> g :: (a :: Type) -> a

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.

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 https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-727907040. 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.

> If I had to explain `forall a -> a` to one of my
> Haskell-curious colleagues, I'd have to say "Oh that means you pass
> the name of a type to the function" -- something they'd have no chance
> of figuring out on their own! The 'forall' comes across as
> meaningless. (Case in point: I had no idea what the syntax meant when
> I saw it -- but I'm already invested enough to go digging.)

I agree that the new syntax is not adequately self-describing.

> 
> I guess my question, then, is if there is some way to make this syntax
> more intuitive for users!

I agree! But I somehow don't think separating out all the pieces will make it easier, in the end.

Richard

> 
> On Wed, Nov 18, 2020 at 10:10 PM Carter Schonwald
> <carter.schonwald at gmail.com> wrote:
>> 
>> I do think explaining it relative to the explicit vs implicit arg syntax of agda function argument syntax.
>> 
>> f:  Forall a . B is used with f x. This relates to the new forall -> syntax.
>> 
>> 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
>> 
>> On Wed, Nov 18, 2020 at 12:09 PM Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
>>> 
>>> Semantically, `forall a -> a -> Int` is the same as `forall a. a -> Int`.  The two only differ in how you use them:
>>>  * For the first one, you have to explicitly provide the type to use for `a` at every call site, while
>>>  * for the second one, you usually omit the type and let GHC infer it.
>>> 
>>> 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
>>> is about a fancy notation for explicitly providing the type at call sites.
>>> 
>>> -Iavor
>>> 
>>> 
>>> 
>>> On Wed, Nov 18, 2020 at 9:51 AM Richard Eisenberg <rae at richarde.dev> wrote:
>>>> 
>>>> Hi Bryan,
>>>> 
>>>> 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!
>>>> 
>>>> This second question is easier to answer. I say "forall a arrow a arrow Int".
>>>> 
>>>> But I still think there may be a deeper question here left unanswered...
>>>> 
>>>> Richard
>>>> 
>>>> On Nov 18, 2020, at 6:11 AM, Bryan Richter <b at chreekat.net> wrote:
>>>> 
>>>> 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"?
>>>> 
>>>> Den tis 17 nov. 2020 16:27Richard Eisenberg <rae at richarde.dev> skrev:
>>>>> 
>>>>> Hi Bryan,
>>>>> 
>>>>> 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"?
>>>>> 
>>>>> Thanks!
>>>>> Richard
>>>>> 
>>>>>> On Nov 17, 2020, at 1:47 AM, Bryan Richter <b at chreekat.net> wrote:
>>>>>> 
>>>>>> Dear forall ghc-devs. ghc-devs,
>>>>>> 
>>>>>> As I read through the "Visible 'forall' in types of terms"
>>>>>> proposal[1], I stumbled over something that isn't relevant to the
>>>>>> proposal itself, so I thought I would bring it here.
>>>>>> 
>>>>>> Given
>>>>>> 
>>>>>>       f :: forall a. a -> a                   (1)
>>>>>> 
>>>>>> I intuitively understand the 'forall' in (1) to represent the phrase
>>>>>> "for all". I would read (1) as "For all objects a in Hask, f is some
>>>>>> relation from a to a."
>>>>>> 
>>>>>> After reading the proposal, I think my intuition may be wrong, since I
>>>>>> discovered `forall a ->`. This means something similar to, but
>>>>>> practically different from, `forall a.`. Thus it seems like 'forall'
>>>>>> is now simply used as a sigil to represent "here is where some special
>>>>>> parameter goes". It could as well be an emoji.
>>>>>> 
>>>>>> What's more, the practical difference between the two forms is *only*
>>>>>> distinguished by ` ->` versus `.`. That's putting quite a lot of
>>>>>> meaning into a rather small number of pixels, and further reduces any
>>>>>> original connection to meaning that 'forall' might have had.
>>>>>> 
>>>>>> I won't object to #281 based only on existing syntax, but I *do*
>>>>>> object to the existing syntax. :) Is this a hopeless situation, or is
>>>>>> there any possibility of bringing back meaning to the syntax of
>>>>>> "dependent quantifiers"?
>>>>>> 
>>>>>> -Bryan
>>>>>> 
>>>>>> [1]: https://github.com/ghc-proposals/ghc-proposals/pull/281
>>>>>> _______________________________________________
>>>>>> ghc-devs mailing list
>>>>>> ghc-devs at haskell.org
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>>> 
>>>> 
>>>> _______________________________________________
>>>> ghc-devs mailing list
>>>> ghc-devs at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>> 
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>> 
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs