Use of forall as a sigil
Sylvain Henry
sylvain at haskus.fr
Thu Dec 3 17:31:57 UTC 2020
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 <b at chreekat.net
> <mailto:b at chreekat.net>> 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 <rae at richarde.dev
> <mailto:rae at richarde.dev>> skrev:
>
>
>
>> On Dec 3, 2020, at 10:23 AM, Bryan Richter <b at chreekat.net
>> <mailto:b at 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 at haskell.org <mailto:ghc-devs at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> <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/e7f5d350/attachment.html>
More information about the ghc-devs
mailing list