Use of forall as a sigil

[Christiaan Baaij]

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