Sorry for too many long messages as usual, but I think I found out the best way to proceed for my case. Indeed, I had been sort of avoiding type families for too long, and I figured this was the way to go. In general, using type families from the start instead of functional dependencies on type classes seems to work better. Now, I don't wanna go and re-do thousands of lines of code to adapt to this either. But, I found out you can actually wrap a type class with functional dependencies into a type class with type families in a non-intrusive way to use it properly. Going back to the example I offered before: class Class1 a b | b -> a where fun1 :: b -> a I can wrap this with another class that uses a type family instead of a functional dependency: class Class1 (Class1FamRes b) b => Class1Fam b where type Class1FamRes b fun1fam :: b -> Class1FamRes b fun1fam = fun1 And then I can define my fun2 properly: fun2 :: (Class1Fam a, Class1Fam (Class1FamRes a)) => a -> Class1FamRes (Class1FamRes a) fun2 = fun1 . fun1 And then when instantiating the type variables, assuming I already had the functional dep instances implemented: instance Class1 Int String where fun1 x = 5 instance Class1 Bool Int where fun1 x = True It's trivial to wrap them in Class1Fam instances: instance Class1Fam String where type Class1FamRes String = Int instance Class1Fam Int where type Class1FamRes Int = Bool And I can use fun2 properly. So I think I know how to properly deal with my big program's problem without having to rewrite too much code, and I also think I'll be using type families way more instead of functional dependencies moving forward. Any additional comments anyone might have would be very welcome. Sorry for the sort of monologue. Do let me know if there's a feeling I'm misusing the list. Thanks again, Juan Casanova. ________________________________ From: Haskell-Cafe on behalf of CASANOVA Juan Sent: 03 April 2021 08:20 To: The Haskell Cafe Subject: Re: [Haskell-cafe] Existential type variables in constraints Richard's answer sounds like pretty much what I thought on my follow-up message, and I guess I'll have to go the route of re-writing all the constraints that do not contain the type variable no longer there. Anthony, I won't argue with the discussion on which extensions are problematic. The reason I thought people saw UndecidableInstances as problematic is that, precisely because of the undecidability (semidecidability?), you can write incorrect programs that do not terminate to compile, and it can be hard to debug. I do know that whenever the program is correct then it works fine. But we don't always write correct programs, and debugging is an essential thing as well. That said, I have ran into the overlapping instances issues myself plenty of times so I'm not disagreeing, I just had this impression I think from reading people talk about UndecidableInstances. On your discussion of my particular example, I think I did not make it clear enough why I want to do things like that. I did try to explain it, but it seems it did not click with you. Also, I think one of the statements you made is flat out incorrect, but maybe I'm mistaken. One thing at a time.

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. 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 fun1 = (<)

Why do I do this? Because, as I tried to explain, my CType in practice is much larger, and it includes many more type variables. I do it to avoid having 5-line constraints on every function I write. Maybe if I show you the actual example it'll click with you. Here's some of the examples: type ESMGUConstraints t pd fn v sov = (Ord sov, SimpleTerm t, Eq fn, HasArity fn, HasArity sov, ChangeArity sov, Functor (t (SOTerm fn sov)), Functor (t fn), Bifunctor t, Traversable (t (GroundSOT fn)), Unifiable (t (SOTerm fn sov)), Variabilizable v, Variable v, Variabilizable sov, Variable sov, Ord v, Functor (t (GroundSOT fn)), Eq (t fn (Fix (t fn))), Show sov, Show fn, Show v, Show (t (SOTerm fn sov) (UTerm (t (SOTerm fn sov)) v)), Show (t (GroundSOT fn) (UTerm (t (GroundSOT fn)) v)), Ord fn, Ord (t (SOTerm fn sov) (UTerm (t (SOTerm fn sov)) v))) type ESMGUConstraintsU t pd fn v sov uv = (ESMGUConstraints t pd fn v sov, Show uv, Ord uv, Variable uv, Variabilizable uv) type ESMGUConstraintsPdPmv pd pmv = (Ord pd, Ord pmv, Eq pd, Eq pmv, Show pmv, Show pd, HasArity pd, HasArity pmv, Variable pmv, Variabilizable pmv, ChangeArity pmv) type ESMGUConstraintsUPmv t pd fn v pmv fmv uv = (ESMGUConstraintsU t pd fn v fmv uv, ESMGUConstraintsPdPmv pd pmv) type ESMGUConstraintsA a = (SimpleTerm a) type ESMGUConstraintsAMpd a mpd = (ESMGUConstraintsA a, Functor (a mpd), Eq mpd, Ord mpd) type ESMGUConstraintsSS ss = (Functor ss, Unifiable ss) type ESMGUConstraintsAMpdSs a t ss mpd pd fn v pmv fmv = (ESMGUConstraints t pd fn v fmv, ESMGUConstraintsSS ss, ESMGUConstraintsAMpd a mpd, Eq (a mpd (ss (SOAtom pd fn pmv fmv))), Eq (a (SOAtom pd fn pmv fmv) (SOMetawrap t fn v fmv)), ESMGUConstraintsPdPmv pd pmv) type ESMGUConstraintsALL a t ss mpd pd fn v pmv fmv uv = (ESMGUConstraintsU t pd fn v fmv uv, ESMGUConstraintsAMpdSs a t ss mpd pd fn v pmv fmv) I think you can see why I would want to avoid having to write all of this on every function that I write. In fact you can see I already have it partially split, but not in all the ways I may want to use it. In particular, there are others in other modules that build on these and add a few others, and I want those except I no longer have the "uv" type variable on one of the functions I have, but I internally use functions that use the constraints that include it, and functional dependencies should ensure that it is instantiated to one particular class. But this leads to your second point, the one in which I think you said something incorrect, or maybe you didn't see how my example was simplified on purpose. You said: No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply. What about the following code then: class Class1 a b | b -> a where fun1 :: b -> a type CType a b = (Ord a, Class1 a b) fun2 :: (forall b. CType a b) => a -> a -> Bool fun2 = (>) Now, fun2 in particular can be made to work because it only makes use of (Ord a) and not (Class1 a b), but the tuple constraint type (CType a b) does have a functional dependency from b to a, so I can see why a is not an entirely separable variable in the forall-quantified constraint, which is why I think ultimately GHC works the way Richard mentioned and why I can't do what I want, even if the specific (Ord a) constraint can be used. Of course the issue, I see, is that this could produce (and does, in my case) chains of functional dependencies that, when existentially quantified, become difficult/problematic. For example: class Class1 a b | b -> a where fun1 :: b -> a type CType a b c = (Class1 a b, Class1 b c) fun2 :: (forall c. CType a b c) => b -> a fun2 = fun1 fun1 does not depend on c, but the type b does, through the functional dependency in (Class1 b c). I don't even know if it would make sense for this to work or not. You can separate (Class1 a b) like you could with (Ord a), but now it's not completely independent of the rest. of (CType a b c). In other words, I'm not sure if the semantics of (forall c. CType a b c) are the same as the semantics of (Class1 a b, forall c. Class1 b c). Now, my actual situation in practice is more something like this: class Class1 a b | b -> a where fun1 :: b -> a type CType a b c = (Class1 a b, Class1 b c) fun2 :: (forall b. CType a b c) => c -> a fun2 c = fun1 (fun1 c) This makes sense conceptually. fun2 does not specify which b we are talking about, but for every c, there should be only one b that works. That, of course, ultimately means that fun2 will not work for any a and c, but only for those for which there is a b linking them. It seems as if GHC does not have the ability to do this. Actually at this point I'm not sure if I can do what I want without instantiating the type variables. 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.

Edward,

That forall isn't denoting existential there, it really is denoting a universal quantifier.

Huh! You seem to be completely right. I think I had thought it would have an existential meaning like when you use constraints in data definitions, like: data Foo = forall a. Ord a => Foo a But I guess here the existential meaning comes from reading it as a universal quantifier on the co-variant argument: "For every a that is an Ord, we can build a Foo with the constructor Foo", which when used the other way around becomes: "If you have a foo, then you have some type with Ord". This definitely does explain the entire problem with the behaviour I am expecting.

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.

Yes, this definitely seems to be the way to go (type families), though I still don't think what I'm trying to do is possible without type families, while keeping the genericity of the type parameters. Thanks for confirming this, and for clarifying my fundamental misunderstanding with quantified constraints. Juan. ________________________________ From: Edward Kmett Sent: 04 April 2021 23:35 To: CASANOVA Juan Cc: 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. 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 mailto:Juan.Casanova@ed.ac.uk> 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 mailto:haskell-cafe-bounces@haskell.org> on behalf of Anthony Clayden mailto:anthony_clayden@clear.net.nz> Sent: 03 April 2021 02:18 To: The Haskell Cafe mailto:haskell-cafe@haskell.org> 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.