<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<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);">
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_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_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="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 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_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.
</body>
</html>