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