[Haskell-cafe] Pattern synonyms and explicit forall.

[Richard Eisenberg]

It sounds like the confusion here has been somewhat resolved.

Some of you may know that I'm producing weekly YouTube videos (I aim for 10 minutes apiece, but more often end up around 15 minutes) -- and it happens that this coming week's video is planned for pattern synonym type signatures, and it will cover exactly the material that should illuminate this conversation. I expect it to appear 7am US Eastern time Tuesday morning, but occasional technical glitches may mean it gets delayed until Wednesday.

All the videos are posted to Tweag's channel at https://www.youtube.com/c/tweag

Richard

> On Sep 19, 2021, at 4:05 PM, Kai Prott <kai.prott at hotmail.de> wrote:
> 
> There are many reasons to write explicit foralls: 
> 
> - Documentation
> - Higher-ranked types
> - Existential types
> - ...
> 
> The last two are not possible in GHC without a few foralls and are often quite useful.  
> 
> Also note that a type signature without explicit quantification like 
> 
> id :: a -> a 
> 
> implicitly means 
> 
> id :: forall a. a -> a 
> 
> Best,
> Kai
> 
> On 19/09/2021 13:22, Branimir Maksimovic wrote:
>> What is purpose formal, except to make heterogenous lists?
>> I find it not necessary in practice, exept to emulate OO 
>> passing through lists, when you need to implement OO like
>> Behavior that is polymorphism. Those things come natural
>> in Haskell wihout forall .
>> 
>> Greetings, Branimir.
>> 
>>> On 19.09.2021., at 12:55, Kai-Oliver Prott <kai.prott at hotmail.de <mailto:kai.prott at hotmail.de>> wrote:
>>> 
>>> Some comments in-line :)
>>> Best, 
>>> Kai Prott
>>> 
>>>> 
>>>> >        pattern Any2 :: forall . forall a. a -> Some
>>>> We're friends here. I think I can share that my reaction was a rather loud WTF??!!??
>>> Yep, that is quite weird. 
>>>> And there's not a mention in the docos that this is even a thing. I feel like dragging whoever's responsible to the headmaster's office.
>>>> Ok that seems to work -- in the sense that pattern-matching on it yields an `x` that's unusable on RHS just as much as the `Any` decl with implicit `forall`, or with no type signature at all.
>>>> What would be useful is to be able to introduce a constraint into the sig, so I can do something like
>>>> >    foo (Any2 x) y = x == y
>>>> After playing with it, all I'm getting is weird rejections. 
>>>> >    pattern Any2 :: forall . forall a. () => (Eq a) => a -> Some
>>> Your first error message seems like a case of bad error messages. 
>>> Just out of curiosity, I've tried writing the following: 
>>> 
>>> pattern Refl :: forall a. forall . () => (Eq a) => Bool -> a
>>> pattern Refl a <- (refl -> a)
>>> 
>>> refl :: Eq a => a -> Bool 
>>> refl a = a == a
>>> 
>>> This should not be accepted. Indeed I get the error message with "fewer arrows", although it seems like the given type signature has exactly the number of arrows it needs. The problem here is the misplaced constraint. 
>>> GHC checks the arity of `Eq a => Bool -> a`, which it argues has zero arrows (->) at the top of the type. 
>>> Note that the correct type signature would be 
>>> 
>>> pattern Refl :: forall a. (Eq a) => forall . () =>  Bool -> a
>>> 
>>>> 
>>>> >    * Pattern synonym `Any2' has one argument
>>>> >        but its type signature has 1 fewer arrows
>>>> I need to put the constraints inside the scope of the `forall a.`. A single `(Show a) => a -> Some` complains no instance provided.
>>> The problem here is, that `Some` does not carry around any information that its argument has an `Eq` instance. It was not declared with such a constraint. Thus, pattern matching on `Some` cannot bring any `Eq` instance into scope. This is what the second error is trying to tell you. `Some` does not carry around enough information for `Any` to provide an `Eq` constraint when pattern matched.
>>> 
>>> And as a quick note: Even if we do define `Some :: Eq a => a -> Some` your example still does not work, since x  and y are not guaranteed to be of the same type. But we could write: 
>>> 
>>> data Some where 
>>>   Some :: Eq a => a -> Some 
>>> 
>>> pattern Any2 :: forall . forall a. (Eq a) => a -> Some
>>> pattern Any2 a = Some a
>>> 
>>> foo :: Some -> Bool 
>>> foo (Any2 x) = x == x
>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>>> _______________________________________________
>>>> Haskell-Cafe mailing list
>>>> To (un)subscribe, modify options or view archives go to:
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
>>>> Only members subscribed via the mailman list are allowed to post.
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
>>> Only members subscribed via the mailman list are allowed to post.
>> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/9b998ab5/attachment.html>