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 <r...@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...@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 <r...@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 >> >> > _______________________________________________ > 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