Use of forall as a sigil

[Carter Schonwald]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20201118/c4c923ae/attachment.html>