Re: [Haskell-cafe] Existential type variables in constraints

There's a lot here. I'm just going to laser lock on the starting impossible part that AntC also tried to address. On Sat, Apr 3, 2021 at 12:26 AM CASANOVA Juan wrote:

This example is just to corner the problem in one example. The reality of what I would do would be more like this:

...

type CType b c = (Ord b, Ord c) instance (Ord a, forall b c. CType b c) => Class1 a where

This doesn't say what you seem to think it says.

It says: When you go to look for an instance for Class1, every such instance is formed as follows: * First go resolve an Ord instance for a. (So far so good). * Next you need to show that for every single pair of types in the universe b and c, Ord b and Ord c hold independently. (Which makes the comparatively narrow ask for an Ord for a seem pretty redundant!) That is an impassable bar. Full stop. It is equivalent to instance (forall x. Ord x) => Class1 a The existence of any type anywhere without an Ord instance that can be uniformly constructed without caring at all about any structure on 'a' stops you cold. That forall isn't denoting existential there, it really is denoting a universal quantifier. If you want 'b' and 'c' to be some function of a, you can use a type family for each to pick them out or a multi-parameter typeclass that includes them in the signature, but that is simply not what you wrote down. -Edward Juan.

------------------------------

*From:* Haskell-Cafe on behalf of Anthony Clayden *Sent:* 03 April 2021 02:18 *To:* The Haskell Cafe *Subject:* Re: [Haskell-cafe] Existential type variables in constraints

This email was sent to you by someone outside the University. You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

...

because UndecidableInstances is definitely required for this and I know it's a problematic one.

Hi Juan, I'll knock that on the head at once. `UndecidableInstances` is not "problematic" (or at least it's far less problematic than others you list). Although we're lacking a proof that it can't lead to incoherence/type unsafety, nobody's demonstrated unsafety due to `UndecidableInstances` alone -- that is, providing the program compiles (i.e. instance resolution terminates).

OTOH `FlexibleInstances` can give `OverlappingInstances` -- maybe overlapping with those in some other module, thus giving the dreaded Orphan instances problems. I'd be much more concerned about them.

...

instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where fun1 = (<)

Why does that even mention `b` or `c`? There's no FunDep from `a`, to get a FunDep there'd be a constraint `D a b c` or something. They seem totally redundant.

...

completely overlooked by the compiler

Yes. Quite. What do you expect the compiler to do? Even if the class decl gave a signature for `fun1` mentioning `b`, `c`, those would be _distinct_ tyvars, because they're not scoped in the class head.

...

is there any way I can make this work?

Sorry, I don't know what you want to "work". Please at least show a class decl with a FunDep. From your second message:

...

it is possible in principle that (Ord a, Ord b) produces a functional dependency between a and b

No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply.

AntC

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336. _______________________________________________ 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.