<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">

<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>

</head>

<body dir="ltr">

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

Sorry for too many long messages as usual, but I think I found out the best way to proceed for my case.<br>

<br>

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.<br>

<br>

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:<br>

<br>

class Class1 a b | b -> a where

<div>fun1 :: b -> a</div>

<br>

I can wrap this with another class that uses a type family instead of a functional dependency:<br>

<br>

class Class1 (Class1FamRes b) b => Class1Fam b where

<div>   type Class1FamRes b</div>

<div>   fun1fam :: b -> Class1FamRes b</div>

<div>   fun1fam = fun1</div>

<br>

<br>

And then I can define my fun2 properly:<br>

<br>

fun2 :: (Class1Fam a, Class1Fam (Class1FamRes a)) => a -> Class1FamRes (Class1FamRes a)</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

fun2 = fun1 . fun1</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

<br>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

And then when instantiating the type variables, assuming I already had the functional dep instances implemented:<br>

<br>

instance Class1 Int String where

<div>   fun1 x = 5</div>

<div><br>

</div>

instance Class1 Bool Int where

<div>   fun1 x = True</div>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

<br>

It's trivial to wrap them in Class1Fam instances:<br>

<br>

instance Class1Fam String where

<div>  type Class1FamRes String = Int</div>

<br>

<div>instance Class1Fam Int where</div>

<div>  type Class1FamRes Int = Bool</div>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

<br>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">

<br>

And I can use fun2 properly.<br>

<br>

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.<br>

<br>

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.<br>

<br>

Thanks again,<br>

Juan Casanova.<br>

</div>

<div id="appendonsend"></div>

<hr style="display:inline-block;width:98%" tabindex="-1">

<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of CASANOVA Juan <Juan.Casanova@ed.ac.uk><br>

<b>Sent:</b> 03 April 2021 08:20<br>

<b>To:</b> The Haskell Cafe <haskell-cafe@haskell.org><br>

<b>Subject:</b> Re: [Haskell-cafe] Existential type variables in constraints</font>

<div> </div>

</div>

<style type="text/css" style="display:none">

<!--

p

        {margin-top:0;

        margin-bottom:0}

-->

</style>

<div dir="ltr">

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

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.<br>

<br>

Anthony,<br>

<br>

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.<br>

<br>

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.<br>

<br>

<div>

<pre style="color:rgb(0,0,0)"><font face="monospace">> instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where

>   fun1 = (<)

</font></pre>

<font face="monospace"><br class="x_x_gmail-Apple-interchange-newline">

</font></div>

<pre style="color:rgb(0,0,0)"><font face="monospace"><span style="font-size:1em">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.</span></font></pre>

<br>

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

<br>

<div>

<pre style="color:rgb(0,0,0)"><font face="monospace">> type CType b c = (Ord b, Ord c)<br>> instance (Ord a, forall b c. CType b c) => Class1 a where

>   fun1 = (<)

</font></pre>

<font face="monospace">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:<br>

<br>

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)))

<div>type ESMGUConstraintsU t pd fn v sov uv = (ESMGUConstraints t pd fn v sov, Show uv, Ord uv, Variable uv, Variabilizable uv)</div>

<div>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)</div>

<div>type ESMGUConstraintsUPmv t pd fn v pmv fmv uv = (ESMGUConstraintsU t pd fn v fmv uv, ESMGUConstraintsPdPmv pd pmv)</div>

<div>type ESMGUConstraintsA a = (SimpleTerm a)</div>

<div>type ESMGUConstraintsAMpd a mpd = (ESMGUConstraintsA a, Functor (a mpd), Eq mpd, Ord mpd)</div>

<div>type ESMGUConstraintsSS ss = (Functor ss, Unifiable ss)</div>

<div>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)</div>

<div>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)<br>

</div>

<br class="x_x_gmail-Apple-interchange-newline">

</font></div>

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.<br>

<br>

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:<br>

<br>

<pre style="color:rgb(0,0,0)"><font face="monospace">No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply.</font></pre>

</div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

What about the following code then:<br>

<br>

<font face="monospace">class Class1 a b | b -> a where</font></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">  fun1 :: b -> a<br>

</font></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace"><br>

</font></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">type CType a b = (Ord a, Class1 a b)<br>

<br>

fun2 :: (forall b. CType a b) => a -> a -> Bool</font></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">fun2 = (>)<br>

</font></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<br>

<br>

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.<br>

<br>

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:<br>

<br>

<span style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)"><font face="monospace">class Class1 a b | b -> a where</font></span>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">  fun1 :: b -> a</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace"><br>

</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">type CType a b c = (Class1 a b, Class1 b c)<br>

<br>

fun2 :: (forall c. CType a b c) => b -> a<br>

</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">fun2 = fun1<br>

</font></div>

<span style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)"></span></div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<br>

</div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

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).<br>

<br>

Now, my actual situation in practice is more something like this:<br>

<br>

</div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<span style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)"><font face="monospace">class Class1 a b | b -> a where</font></span>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">  fun1 :: b -> a</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace"><br>

</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">type CType a b c = (Class1 a b, Class1 b c)</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace"><br>

</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">fun2 :: (forall b. CType a b c) => c -> a</font></div>

<div style="font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<font face="monospace">fun2 c = fun1 (fun1 c)<br>

</font></div>

</div>

<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">

<br>

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.<br>

<br>

Actually at this point I'm not sure if I can do what I want without instantiating the type variables.<br>

<br>

Juan.<br>

</div>

<div id="x_appendonsend"></div>

<hr tabindex="-1" style="display:inline-block; width:98%">

<div id="x_divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of Anthony Clayden <anthony_clayden@clear.net.nz><br>

<b>Sent:</b> 03 April 2021 02:18<br>

<b>To:</b> The Haskell Cafe <haskell-cafe@haskell.org><br>

<b>Subject:</b> Re: [Haskell-cafe] Existential type variables in constraints</font>

<div> </div>

</div>

<div>

<div style="background-color:#fff2e6; border:2px dotted #ff884d"><span style="font-size:12pt; font-family:sans-serif; color:black; font-weight:bold; padding:.2em">This email was sent to you by someone outside the University.</span>

<div style="font-size:10pt; font-family:sans-serif; font-style:normal; padding:.2em">

You should only click on links or attachments if you are certain that the email is genuine and the content is safe.</div>

</div>

<div>

<div dir="ltr"><font face="monospace">> <span style="color:rgb(0,0,0); font-size:1em; white-space:pre-wrap">because UndecidableInstances is definitely required for this and I know it's a problematic one.</span></font>

<div><span style="color:rgb(0,0,0); font-size:1em; white-space:pre-wrap"><font face="monospace"><br>

</font></span></div>

<div><span style="color:rgb(0,0,0); font-size:1em; white-space:pre-wrap"><font face="monospace">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).</font></span></div>

<div><span style="color:rgb(0,0,0); font-size:1em; white-space:pre-wrap"><font face="monospace"><br>

</font></span></div>

<div><span style="color:rgb(0,0,0); font-size:1em; white-space:pre-wrap"><font face="monospace">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.</font></span></div>

<div><br>

</div>

<div>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">> instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where

>   fun1 = (<)

</font></pre>

<font face="monospace"><br class="x_x_gmail-Apple-interchange-newline">

</font></div>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><span style="font-size:1em">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.</span><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><span style="font-size:1em"><font face="monospace"><br></font></span></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><span style="font-size:1em">> </span>completely overlooked by the compiler</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">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.</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">> is there any way I can make this work?</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">Sorry, I don't know what you want to "work". Please at least show a class decl with a FunDep. From your second message:</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">> it is possible in principle that (Ord a, Ord b) produces a functional dependency between a and b</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">No it isn't possible, even in principle: `(..., ...)` is a tuple constructor, not a class; therefore no FunDep could apply.</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace"><br></font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><font face="monospace">AntC</font></pre>

<pre style="white-space:pre-wrap; color:rgb(0,0,0)"><br></pre>

</div>

</div>

</div>

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.

</div>

</body>

</html>