[Haskell-cafe] Pattern synonyms and explicit forall.

[Kai Prott]

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
>>> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/c6d75976/attachment.html>