[Haskell-cafe] Pattern synonyms and explicit forall.
kai.prott at hotmail.de
Sun Sep 19 20:05:51 UTC 2021
There are many reasons to write explicit foralls:
- Higher-ranked types
- Existential types
The last two are not possible in GHC without a few foralls and are often
Also note that a type signature without explicit quantification like
id :: a -> a
id :: forall a. a -> a
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 :)
>> 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
>> 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:
>>> 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:
>> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe