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 th
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 vari
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 fin
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 differenc
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 deep
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 over
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
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 implementat
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, w
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
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
me
sible 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
s,
> 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
> 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, ...,
> 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 t
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
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.
- V
> 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
> t
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:
>
>
>
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 e
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 applica
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 * -> *
22 matches
Mail list logo
