> How do you feel about > > > f :: forall (a :: Type) -> a > or > > g :: (a :: Type) -> a
The former has the same problem as the current syntax. The latter seems better, but then I might be confused again. :) My main concern is with the choice of keyword. With data, instance, class, module, ..., the pattern is clear: name the sort of thing you are introducing. forall, on the other hand, doesn't introduce a "forall". It's making explicit the existing universal quantification. But somewhere, an author decided to reuse the same keyword to herald a type argument. It seems they stopped thinking about the meaning of the word itself, saw that it was syntactically in the right spot, and borrowed it to mean something else. I feel like that borrowing introduced a wart. Consider `forall a -> a -> a`. There's still an implicit universal quantification that is assumed, right? I.e., this type signature would be valid for all types `a` ? But then how do we make that quantification explicit? `forall a. forall a -> a -> a`? But oops, have we now introduced a new type argument? I keep referring to the thing as a "type argument". I know it's hard to introduce a new keyword, but imagine if we had `forall a. typearg a -> a -> a`. It would at least point to its meaning. I guess that's pretty close to your > g :: (a :: Type) -> a which is why I think it seems a bit better. On Fri, Nov 20, 2020 at 10:56 PM Richard Eisenberg <r...@richarde.dev> wrote: > Hi Bryan, > > Thanks for this longer post -- it's very helpful to see this with fresh > eyes. > > > > On Nov 19, 2020, at 2:18 PM, Bryan Richter <b...@chreekat.net> wrote: > > > > So correct me if I'm wrong: from an implementation perspective, > > `forall a. a -> Int` is a function of two arguments, one of which can > > be elided, while `forall a -> a -> Int` is a function of two > > arguments, all of which must be provided. > > Yes, that's how I read these. > > > > > If that's right, then it bumps into my intuition, which says that the > > former is a function of only one argument. I never thought of `f @Int` > > as partial function application, for instance. :) Is my intuition > > leading me astray? *Should* I consider both functions as having two > > arguments? If so, is that somehow "mathematically true" (a very > > not-mathematical phrase, haha), or is it just an "implementation > > detail"? > > I don't think there's one right answer here. And I'm not quite sure how to > interpret "mathematically true". The best I can get is that, if we consider > System F (a direct inspiration for Haskell's type system), then both > functions really do take 2 arguments (as they do in GHC Core). > > > > > > > So that's one avenue of query I have, but it's actually not the one I > > started off with. Focusing on the simpler case of `forall a -> a`, > > which is a function of one argument, I take issue with how the > > quantification is packed into the syntax for the argument, itself. > > I.e., my intuition tells me this function is valid for all types, > > takes the name of a type as an argument, and returns a value of that > > type, which is three distinct pieces of information. I'd expect a > > syntax like `forall a. elem x a. a -> x`, or maybe `forall a. nameof a > > -> a`. The packing and punning conspire to make the syntax seem overly > > clever. > > How do you feel about > > > f :: forall (a :: Type) -> a > > or > > > g :: (a :: Type) -> a > > Somehow, for me too, having the type of `a` listed makes it clearer. The > syntax for f echoes that in Coq, a long-standing dependently typed > language, but it uses , instead of ->. The type of `a` is optional. (An > implicit parameter is put in braces.) The syntax for g echoes that in Agda > and Idris; the type of `a` is not optional. Haskell cannot use the syntax > for `g`, because it looks like a kind annotation. > > In the end, I've never loved the forall ... -> syntax, but I've never seen > anything better. The suggestions you make are akin to those in > https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-727907040. > This alternative might work out, but I've never seen this approach taken in > another language, and it would be quite different from what we have today. > > > > If I had to explain `forall a -> a` to one of my > > Haskell-curious colleagues, I'd have to say "Oh that means you pass > > the name of a type to the function" -- something they'd have no chance > > of figuring out on their own! The 'forall' comes across as > > meaningless. (Case in point: I had no idea what the syntax meant when > > I saw it -- but I'm already invested enough to go digging.) > > I agree that the new syntax is not adequately self-describing. > > > > > I guess my question, then, is if there is some way to make this syntax > > more intuitive for users! > > I agree! But I somehow don't think separating out all the pieces will make > it easier, in the end. > > Richard > > > > > On Wed, Nov 18, 2020 at 10:10 PM Carter Schonwald > > <carter.schonw...@gmail.com> wrote: > >> > >> I do think explaining it relative to the explicit vs implicit arg > syntax of agda function argument syntax. > >> > >> f: Forall a . B is used with f x. This relates to the new forall -> > syntax. > >> > >> g: forall {c}. D is used either as f or f {x}, aka implicit or forcing > it to be explicit. This maps to our usual Haskell forall with explicit {} > being the @ analogue > >> > >> On Wed, Nov 18, 2020 at 12:09 PM Iavor Diatchki < > iavor.diatc...@gmail.com> wrote: > >>> > >>> 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 > >> > >> _______________________________________________ > >> 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
