<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Tahoma;
panose-1:2 11 6 4 3 5 4 4 2 4;}
@font-face
{font-family:Verdana;
panose-1:2 11 6 4 3 5 4 4 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
span.hoenzb
{mso-style-name:hoenzb;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Verdana","sans-serif";
color:#1F497D;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri","sans-serif";
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:1493256418;
mso-list-type:hybrid;
mso-list-template-ids:-1311614240 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal" style="margin-left:36.0pt">As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">Iavor is quite right<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.<o:p></o:p></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is.
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A
good start would be to begin a wiki page to flesh out the design issues, perhaps linked from
<a href="http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions">http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions</a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">The main issues are, I think:<o:p></o:p></span></p>
<p class="MsoListParagraph" style="text-indent:-18.0pt;mso-list:l0 level1 lfo1"><![if !supportLists]><span style="font-size:11.0pt;font-family:Symbol;color:#1F497D"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">How to express functional dependencies like “fixing the result type and the first argument will fix the second argument”<o:p></o:p></span></p>
<p class="MsoListParagraph" style="text-indent:-18.0pt;mso-list:l0 level1 lfo1"><![if !supportLists]><span style="font-size:11.0pt;font-family:Symbol;color:#1F497D"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">How to express that idea in the proof language<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">Simon<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> glasgow-haskell-bugs-bounces@haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org]
<b>On Behalf Of </b>Iavor Diatchki<br>
<b>Sent:</b> 26 December 2012 02:48<br>
<b>To:</b> Conal Elliott<br>
<b>Cc:</b> glasgow-haskell-bugs@haskell.org; GHC Users Mailing List<br>
<b>Subject:</b> Re: Fundeps and type equality<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">Hello Conal,<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in
examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this
sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Cheers,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">-Iavor<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><o:p> </o:p></p>
<div>
<p class="MsoNormal">On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:<o:p></o:p></p>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt">I ran into a simple falure with functional dependencies (in GHC 7.4.1):<br>
<br>
> class Foo a ta | a -> ta<br>
> <br>
> foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool<br>
> foo = (==)<br>
<br>
I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but<br>
<br>
Pixie/Bug1.hs:9:7:<br>
Could not deduce (ta ~ tb)<br>
from the context (Foo a ta, Foo a tb, Eq ta)<br>
bound by the type signature for<br>
foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool<br>
at Pixie/Bug1.hs:9:1-10<br>
`ta' is a rigid type variable bound by<br>
the type signature for<br>
foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool<br>
at Pixie/Bug1.hs:9:1<br>
`tb' is a rigid type variable bound by<br>
the type signature for<br>
foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool<br>
at Pixie/Bug1.hs:9:1<br>
Expected type: ta -> tb -> Bool<br>
Actual type: ta -> ta -> Bool<br>
In the expression: (==)<br>
In an equation for `foo': foo = (==)<br>
Failed, modules loaded: none.<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Any insights about what's going wrong here?<o:p></o:p></p>
</div>
<p class="MsoNormal"><span class="hoenzb"><span style="color:#888888">-- Conal</span></span><o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
_______________________________________________<br>
Glasgow-haskell-bugs mailing list<br>
<a href="mailto:Glasgow-haskell-bugs@haskell.org">Glasgow-haskell-bugs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs</a><o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</body>
</html>