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@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@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@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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs