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 <sylv...@haskus.fr> 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 <b...@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 <r...@richarde.dev> skrev: >>> >>> >>> >>> On Dec 3, 2020, at 10:23 AM, Bryan Richter <b...@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@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
