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