Re: Use of forall as a sigil

Reading proposal 281, I would be similarly confused. In point 4 of section 4.1, primary change, it states that type constructors are now allowed in the grammar of patterns; which if I understand correctly is mostly a name-resolving thing. Perhaps I read the proposal too quickly, but I couldn't find a sentence anywhere that explicitly said that type-checking will subsequently throw an error when name-resolution resolved a pattern to be a type constructor. -- Christiaan On Tue, 17 Nov 2020 at 15:27, Richard Eisenberg wrote:

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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs