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

Edward,<br>

<br>

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

<br>

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

<br>

data Foo = forall a. Ord a => Foo a<br>

<br>

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

<br>

This definitely does explain the entire problem with the behaviour I am expecting.<br>

<br>

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

<br>

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

<br>

Thanks for confirming this, and for clarifying my fundamental misunderstanding with quantified constraints.<br>

<br>

Juan.<br>

<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> Edward Kmett <ekmett@gmail.com><br>

<b>Sent:</b> 04 April 2021 23:35<br>

<b>To:</b> CASANOVA Juan <Juan.Casanova@ed.ac.uk><br>

<b>Cc:</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">

<div>There's a lot here. I'm just going to laser lock on the starting impossible part that AntC also tried to address.</div>

<div dir="ltr"><br>

</div>

<div dir="ltr">On Sat, Apr 3, 2021 at 12:26 AM CASANOVA Juan <<a href="mailto:Juan.Casanova@ed.ac.uk">Juan.Casanova@ed.ac.uk</a>> wrote:<br>

</div>

<div class="x_gmail_quote">

<blockquote class="x_gmail_quote" style="margin:0px 0px 0px 0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">

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

<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

</font></pre>

</div>

</div>

</div>

</blockquote>

<div>This doesn't say what you seem to think it says. <br>

<br>

It says:</div>

<div><br>

</div>

<div>    When you go to look for an instance for Class1, every such instance is formed as follows:</div>

<div>    </div>

<div>    * First go resolve an Ord instance for a. (So far so good).</div>

<div> </div>

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

</div>

<div><br>

</div>

<div>That is an impassable bar. Full stop.</div>

<div><br>

</div>

<div>It is equivalent to </div>

<div><font face="monospace"><br>

</font></div>

<div><font face="monospace">instance (forall x. Ord x) => Class1 a</font></div>

<div><br>

</div>

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

<div><br>

</div>

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

<div><br>

</div>

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

<div> <br>

</div>

<div>-Edward</div>

<div><br>

</div>

<blockquote class="x_gmail_quote" style="margin:0px 0px 0px 0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">

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

<div><span style="font-size:12pt">Juan.</span><br>

</div>

</div>

</div>

</blockquote>

<blockquote class="x_gmail_quote" style="margin:0px 0px 0px 0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">

<div dir="ltr">

<div id="x_gmail-m_5303934640092723238appendonsend"></div>

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

<div id="x_gmail-m_5303934640092723238divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Haskell-Cafe <<a href="mailto:haskell-cafe-bounces@haskell.org" target="_blank">haskell-cafe-bounces@haskell.org</a>>

 on behalf of Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>><br>

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

<b>To:</b> The Haskell Cafe <<a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a>><br>

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

<div> </div>

</div>

<div>

<div style="background-color:rgb(255,242,230); border:2px dotted rgb(255,136,77)">

<span style="font-size:12pt; font-family:sans-serif; color:black; font-weight:bold; padding:0.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:0.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>

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

_______________________________________________<br>

Haskell-Cafe mailing list<br>

To (un)subscribe, modify options or view archives go to:<br>

<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>

Only members subscribed via the mailman list are allowed to post.</blockquote>

</div>

</div>

</div>

</div>

</body>

</html>