[Haskell-cafe] Pattern synonyms and explicit forall.

[Branimir Maksimovic]

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> 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
> 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/9d0f7dbd/attachment.html>