Use of forall as a sigil

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
22 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: Use of forall as a sigil

Bryan Richter-2
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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Use of forall as a sigil

Krzysztof Gogolewski
In reply to this post by Sylvain Henry-2
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> skrev:
>>>
>>>
>>>
>>> On Dec 3, 2020, at 10:23 AM, Bryan Richter <[hidden email]> 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
>> [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
12