Re: Use of forall as a sigil

3 Dec 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  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-7279070....
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
...
...
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@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
...
...
...
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
syntax of agda function argument syntax.
that from the text in #281, but I think a lot of the complexity there
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

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