Re: Use of forall as a sigil

[Krzysztof Gogolewski]

We should not reuse the lambda abstraction syntax for foralls. One is
defining a function, and the other a function type. With Dependent
Haskell, we could have:

type T = forall a -> Maybe a
type R = \a -> Maybe a

Here, T has kind * and (\_ -> Nothing) is a value of type T, while R
has kind * -> * and could be defined with 'type R a = Maybe a'.



On Thu, Dec 3, 2020 at 6:32 PM Sylvain Henry  wrote:
>
> I don't know if this has been discussed but couldn't we reuse the lambda 
> abstraction syntax for this?
>
> That is instead of writing: forall a ->
> Write: \a ->
>
> Sylvain
>
>
> On 03/12/2020 17:21, Vladislav Zavialov wrote:
>
> There is no *implicit* universal quantification in that example, but there is 
> an explicit quantifier. It is written as follows:
>
>   forall a ->
>
> which is entirely analogous to:
>
>   forall a.
>
> in all ways other than the additional requirement to instantiate the type 
> vatiable visibly at use sites.
>
> - Vlad
>
>
> On Thu, Dec 3, 2020, 19:12 Bryan Richter  wrote:
>>
>> I must be confused, because it sounds like you are contradicting yourself. 
>> :) In one sentence you say that there is no assumed universal quantification 
>> going on, and in the next you say that the function does indeed work for all 
>> types. Isn't that the definition of universal quantification?
>>
>> (We're definitely getting somewhere interesting!)
>>
>> Den tors 3 dec. 2020 17:56Richard Eisenberg  skrev:
>>>
>>>
>>>
>>> On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
>>>
>>> Consider `forall a -> a -> a`. There's still an implicit universal 
>>> quantification that is assumed, right?
>>>
>>>
>>> No, there isn't, and I think this is the central point of confusion. A 
>>> function of type `forall a -> a -> a` does work for all types `a`. So I 
>>> think the keyword is appropriate. The only difference is that we must state 
>>> what `a` is explicitly. I thus respectfully disagree with
>>>
>>> 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.
>>>
>>>
>>> Does this help clarify? And if it does, is there a place you can direct us 
>>> to where the point could be made more clearly? I think you're far from the 
>>> only one who has tripped here.
>>>
>>> Richard
>>
>> ___
>> 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

Re: Use of forall as a sigil

[Bryan Richter]

Hm, yes, I might share Eric's intuition.


I think I'm starting to get it, though. It originally sounded to me like
"forall a ->" was being introduced as a new syntax for function arguments.
In fact, it is a new syntax for quantification -- one that happens to
borrow the syntax for function application. And well it might, because the
sort of quantification it introduces is one that requires passing the name
of a type to the function!


Den tors 3 dec. 2020 18:39Eric Seidel  skrev:

> I think the confusion for me is that I've trained myself to think of
> `forall` as explicitly introducing an implicit argument, and `->`
> as introducing an explicit argument. So the syntax `forall a ->`
> looks to me like a contradiction.
>
> On Thu, Dec 3, 2020, at 10:56, Richard Eisenberg wrote:
> >
> >
> > > On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
> > >
> > > Consider `forall a -> a -> a`. There's still an implicit universal
> quantification that is assumed, right?
> >
> > No, there isn't, and I think this is the central point of confusion. A
> > function of type `forall a -> a -> a` does work for all types `a`. So I
> > think the keyword is appropriate. The only difference is that we must
> > state what `a` is explicitly. I thus respectfully disagree
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[Sylvain Henry]

I don't know if this has been discussed but couldn't we reuse the lambda 
abstraction syntax for this?


That is instead of writing: forall a ->
Write: \a ->

Sylvain


On 03/12/2020 17:21, Vladislav Zavialov wrote:
There is no *implicit* universal quantification in that example, but 
there is an explicit quantifier. It is written as follows:


  forall a ->

which is entirely analogous to:

  forall a.

in all ways other than the additional requirement to instantiate the 
type vatiable visibly at use sites.


- Vlad


On Thu, Dec 3, 2020, 19:12 Bryan Richter > wrote:


I must be confused, because it sounds like you are contradicting
yourself. :) In one sentence you say that there is no assumed
universal quantification going on, and in the next you say that
the function does indeed work for all types. Isn't that the
definition of universal quantification?

(We're definitely getting somewhere interesting!)

Den tors 3 dec. 2020 17:56Richard Eisenberg mailto:r...@richarde.dev>> skrev:




On Dec 3, 2020, at 10:23 AM, Bryan Richter mailto:b...@chreekat.net>> wrote:

Consider `forall a -> a -> a`. There's still an implicit
universal quantification that is assumed, right?


No, there isn't, and I think this is the central point of
confusion. A function of type `forall a -> a -> a` does work
for all types `a`. So I think the keyword is appropriate. The
only difference is that we must state what `a` is explicitly.
I thus respectfully disagree with


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.


Does this help clarify? And if it does, is there a place you
can direct us to where the point could be made more clearly? I
think you're far from the only one who has tripped here.

Richard

___
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

Re: Use of forall as a sigil

[Eric Seidel]

I think the confusion for me is that I've trained myself to think of
`forall` as explicitly introducing an implicit argument, and `->`
as introducing an explicit argument. So the syntax `forall a ->`
looks to me like a contradiction.

On Thu, Dec 3, 2020, at 10:56, Richard Eisenberg wrote:
> 
> 
> > On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
> > 
> > Consider `forall a -> a -> a`. There's still an implicit universal 
> > quantification that is assumed, right?
> 
> No, there isn't, and I think this is the central point of confusion. A 
> function of type `forall a -> a -> a` does work for all types `a`. So I 
> think the keyword is appropriate. The only difference is that we must 
> state what `a` is explicitly. I thus respectfully disagree with
> 
> > 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.
> Does this help clarify? And if it does, is there a place you can direct 
> us to where the point could be made more clearly? I think you're far 
> from the only one who has tripped here.
> 
> Richard
> ___
> 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

Re: Use of forall as a sigil

[Richard Eisenberg]

> On Dec 3, 2020, at 11:11 AM, Bryan Richter  wrote:
> 
> I must be confused, because it sounds like you are contradicting yourself. :) 
> In one sentence you say that there is no assumed universal quantification 
> going on, and in the next you say that the function does indeed work for all 
> types. Isn't that the definition of universal quantification?

I agree with Vlad's comment here: There *is* universal quantification here, but 
there is not *implicit* universal quantification, as it's *explicit*. You've 
made the universal quantification with your `forall a ->`.

Richard___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[Vladislav Zavialov]

There is no *implicit* universal quantification in that example, but there
is an explicit quantifier. It is written as follows:

  forall a ->

which is entirely analogous to:

  forall a.

in all ways other than the additional requirement to instantiate the type
vatiable visibly at use sites.

- Vlad


On Thu, Dec 3, 2020, 19:12 Bryan Richter  wrote:

> I must be confused, because it sounds like you are contradicting yourself.
> :) In one sentence you say that there is no assumed universal
> quantification going on, and in the next you say that the function does
> indeed work for all types. Isn't that the definition of universal
> quantification?
>
> (We're definitely getting somewhere interesting!)
>
> Den tors 3 dec. 2020 17:56Richard Eisenberg  skrev:
>
>>
>>
>> On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
>>
>> Consider `forall a -> a -> a`. There's still an implicit universal
>> quantification that is assumed, right?
>>
>>
>> No, there isn't, and I think this is the central point of confusion. A
>> function of type `forall a -> a -> a` does work for all types `a`. So I
>> think the keyword is appropriate. The only difference is that we must state
>> what `a` is explicitly. I thus respectfully disagree with
>>
>> 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.
>>
>>
>> Does this help clarify? And if it does, is there a place you can direct
>> us to where the point could be made more clearly? I think you're far from
>> the only one who has tripped here.
>>
>> Richard
>>
> ___
> 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

Re: Use of forall as a sigil

[Bryan Richter]

I must be confused, because it sounds like you are contradicting yourself.
:) In one sentence you say that there is no assumed universal
quantification going on, and in the next you say that the function does
indeed work for all types. Isn't that the definition of universal
quantification?

(We're definitely getting somewhere interesting!)

Den tors 3 dec. 2020 17:56Richard Eisenberg  skrev:

>
>
> On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
>
> Consider `forall a -> a -> a`. There's still an implicit universal
> quantification that is assumed, right?
>
>
> No, there isn't, and I think this is the central point of confusion. A
> function of type `forall a -> a -> a` does work for all types `a`. So I
> think the keyword is appropriate. The only difference is that we must state
> what `a` is explicitly. I thus respectfully disagree with
>
> 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.
>
>
> Does this help clarify? And if it does, is there a place you can direct us
> to where the point could be made more clearly? I think you're far from the
> only one who has tripped here.
>
> Richard
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[Richard Eisenberg]

> On Dec 3, 2020, at 10:23 AM, Bryan Richter  wrote:
> 
> Consider `forall a -> a -> a`. There's still an implicit universal 
> quantification that is assumed, right?

No, there isn't, and I think this is the central point of confusion. A function 
of type `forall a -> a -> a` does work for all types `a`. So I think the 
keyword is appropriate. The only difference is that we must state what `a` is 
explicitly. I thus respectfully disagree with

> 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.

Does this help clarify? And if it does, is there a place you can direct us to 
where the point could be made more clearly? I think you're far from the only 
one who has tripped here.

Richard___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[Bryan Richter]

> 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  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  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
> >  wrote:
> >>
> >> I do think 

Re: Use of forall as a sigil

[Richard Eisenberg]

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  
> 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:john.ericson@obsidian.systems] 
> Sent: 22 November 2020 16:41
> To: Andrey Mokhov ; Richard Eisenberg 
> 
> Cc: ghc-devs@haskell.org
> 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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Use of forall as a sigil

[Andrey Mokhov]

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:john.ericson@obsidian.systems] 
Sent: 22 November 2020 16:41
To: Andrey Mokhov ; Richard Eisenberg 

Cc: ghc-devs@haskell.org
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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[John Ericson]

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
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

Re: Use of forall as a sigil

[Andrey Mokhov]

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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Use of forall as a sigil

[Richard Eisenberg]

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  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
>  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  
>> 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  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  wrote:
 
 Yeah, sorry, I think I'm 

Re: Use of forall as a sigil

[Bryan Richter]

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
 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  
> 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  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  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  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  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 

Re: Use of forall as a sigil

[Carter Schonwald]

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 
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 
> 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  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  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  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

Re: Use of forall as a sigil

[Iavor Diatchki]

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  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  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  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  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

Re: Use of forall as a sigil

[Richard Eisenberg]

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  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  > 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  > > 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

Re: Use of forall as a sigil

[Bryan Richter]

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  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  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

Re: Use of forall as a sigil

[Christiaan Baaij]

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  wrote:

> 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  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

Re: Use of forall as a sigil

[Richard Eisenberg]

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  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