Use of forall as a sigil

Bryan Richter b at chreekat.net
Tue Nov 17 06:47:18 UTC 2020


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


More information about the ghc-devs mailing list