Use of forall as a sigil

Thu Dec 3 15:23:33 UTC 2020

> 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 <rae at 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 at 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.schonwald at 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.diatchki at 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 <rae at 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 at 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 <rae at 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 at 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 at haskell.org
> >>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>>>>
> >>>>
> >>>> _______________________________________________
> >>>> ghc-devs mailing list
> >>>> ghc-devs at haskell.org
> >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>>
> >>> _______________________________________________
> >>> ghc-devs mailing list
> >>> ghc-devs at haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>
> >> _______________________________________________
> >> ghc-devs mailing list
> >> ghc-devs at haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20201203/ad7d4141/attachment.html>