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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Reading proposal 281, I would be similarly confused. In point 4 of section 4.1, primary change, it states that type constructors are now allowed in the grammar of patterns; which if I understand correctly is mostly a name-resolving thing.
Perhaps I read the proposal too quickly, but I couldn't find a sentence anywhere that explicitly said that type-checking will subsequently throw an error when name-resolution resolved a pattern to be a type constructor. -- Christiaan On Tue, 17 Nov 2020 at 15:27, Richard Eisenberg <[hidden email]> wrote: Hi Bryan, _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Richard Eisenberg-5
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 <[hidden email]> skrev: Hi Bryan, _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Thanks for the replies! Let's see if I can make a stab at those deeper
questions now. I'm playing a form of devil's advocate here, dissecting the syntax with my intuition as a ghc *user*, and trying to bridge the gap to how ghc *devs* understand it. 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. 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"? 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. 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 guess my question, then, is if there is some way to make this syntax more intuitive for users! On Wed, Nov 18, 2020 at 10:10 PM Carter Schonwald <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >>>> > [hidden email] >>>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>>> >>> >>> _______________________________________________ >>> ghc-devs mailing list >>> [hidden email] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >> _______________________________________________ >> ghc-devs mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> 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 > <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >>>>>> [hidden email] >>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>>>> >>>> >>>> _______________________________________________ >>>> ghc-devs mailing list >>>> [hidden email] >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >>> _______________________________________________ >>> ghc-devs mailing list >>> [hidden email] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >> _______________________________________________ >> ghc-devs mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Bryan Richter-2
Hi Richard,
> In the end, I've never loved the forall ... -> syntax, but I've never seen > anything better. What about the forall @a. syntax? For example: sizeOf :: forall @a. Sized a => Int We already use @ to explicitly specify types, so it seems natural mark type parameters that must be explicitly specified with @ too. Here's how one would read it: "for all explicitly specified a, ..." Apologies if this has been discussed and I missed it. It doesn't seem to be mentioned in the Alternatives section of the proposal but perhaps it will just never work for some reason. Cheers, Andrey _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
I have thought about this too, and don't believe it has been widely
discussed. - We are already getting `forall {a}.`, so it fits nicely with that. - However, it would have to be `forall @a ->`, because `forall a.` is already an invisible quantification, unless one wants to just change the meaning of `forall a.`! John On 11/22/20 6:23 AM, Andrey Mokhov wrote: > Hi Richard, > >> In the end, I've never loved the forall ... -> syntax, but I've never seen >> anything better. > What about the forall @a. syntax? > > For example: > > sizeOf :: forall @a. Sized a => Int > > We already use @ to explicitly specify types, so it seems natural mark type parameters that must be explicitly specified with @ too. > > Here's how one would read it: "for all explicitly specified a, ..." > > Apologies if this has been discussed and I missed it. It doesn't seem to be mentioned in the Alternatives section of the proposal but perhaps it will just never work for some reason. > > Cheers, > Andrey > > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Hi John,
> - We are already getting `forall {a}.`, so it fits nicely with that. Interesting, I wasn't aware of this. Could you point me to the relevant proposal? > - However, it would have to be `forall @a ->`, Oh, that seems even worse than `forall a ->` to me. > because `forall a.` is already an invisible quantification, > unless one wants to just change the meaning of `forall a.`! I'm confused. I wasn't suggesting to change the meaning of `forall a.`. My suggestion was pretty incremental: * `forall a.` stays as is: it allows for both invisible and visible type arguments. * `forall @a.` requires a visible type argument. Cheers, Andrey -----Original Message----- From: John Ericson [mailto:[hidden email]] Sent: 22 November 2020 16:41 To: Andrey Mokhov <[hidden email]>; Richard Eisenberg <[hidden email]> Cc: [hidden email] Subject: Re: Use of forall as a sigil I have thought about this too, and don't believe it has been widely discussed. - We are already getting `forall {a}.`, so it fits nicely with that. - However, it would have to be `forall @a ->`, because `forall a.` is already an invisible quantification, unless one wants to just change the meaning of `forall a.`! John _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
For me, the problem with `forall @a .` is that it seems to go in the wrong direction: parameters declared with @ must not have @ when passed, and parameters declared without @ must have a @ if the parameter is passed explicitly.
However, if we say that @ makes a thing that is normally implicit explicit, maybe it works? Richard > On Nov 22, 2020, at 3:03 PM, Andrey Mokhov <[hidden email]> wrote: > > Hi John, > >> - We are already getting `forall {a}.`, so it fits nicely with that. > > Interesting, I wasn't aware of this. Could you point me to the relevant proposal? > >> - However, it would have to be `forall @a ->`, > > Oh, that seems even worse than `forall a ->` to me. > >> because `forall a.` is already an invisible quantification, >> unless one wants to just change the meaning of `forall a.`! > > I'm confused. I wasn't suggesting to change the meaning of `forall a.`. > > My suggestion was pretty incremental: > > * `forall a.` stays as is: it allows for both invisible and visible type arguments. > * `forall @a.` requires a visible type argument. > > Cheers, > Andrey > > -----Original Message----- > From: John Ericson [mailto:[hidden email]] > Sent: 22 November 2020 16:41 > To: Andrey Mokhov <[hidden email]>; Richard Eisenberg <[hidden email]> > Cc: [hidden email] > Subject: Re: Use of forall as a sigil > > > I have thought about this too, and don't believe it has been widely > discussed. > > - We are already getting `forall {a}.`, so it fits nicely with that. > > - However, it would have to be `forall @a ->`, because `forall a.` is > already an invisible quantification, unless one wants to just change the > meaning of `forall a.`! > > John > _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |