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