<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 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
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:11.0pt;
font-family:"Calibri",sans-serif;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.Code, li.Code, div.Code
{mso-style-name:Code;
mso-style-link:"Code Char";
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:9.0pt;
font-family:"Courier New";}
span.CodeChar
{mso-style-name:"Code Char";
mso-style-link:Code;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;
mso-fareast-language:EN-GB;}
span.gmail-line
{mso-style-name:gmail-line;}
span.EmailStyle24
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.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;}
--></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="#0563C1" vlink="#954F72">
<div class="WordSection1">
<pre style="margin-left:36.0pt">I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity.<o:p></o:p></pre>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">To call System FC a straitjacket is to suggest that there is a straightforward alternative that would serve the purpose better – let’s take off the straitjacket! I’m all for that, but then we do
need to describe what the new alternative is, at a comparable level of precision.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">For better or worse, GHC uses FC as a statically-typed intermediate language. Vanishingly few compilers do this; almost all use an untyped intermediate language. With an untyped IR, all you need
do is typecheck the source program, and then you are done with typechecking --- provided that all the subsequent transformations and optimisations are sound. <o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">But with a statically typed IR, we have to ensure that every transformation produces a program that is itself well-typed; and that in turn pretty much rules out complicated inference algorithms,
because they are fragile to transformation. Instead, GHC uses a complicated inference algorithm on the (implicitly typed)
<i>source</i> program, but under the straitjacket restriction that the type inference algorithm must
<i>also</i> translate the program into an <i>explicitly</i>-typed IR.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">This is a choice that GHC makes. It’s a choice that I love, and one that makes GHC distinctive. But I accept that it comes with a cost.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">There may be an IR based on fundeps, or CHRs or something, that has similar properties to FC. It would be a great research goal to work on such a thing.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">That said, there may be aspects of GHC’s implementation fundeps that are unsatisfactory or argualbly just plain wrong, and which could be fixed and
<i>still</i> translate into FC. If anyone would like to work on that, I’d be happy to help explain how the current machinery works.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Simon<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><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 #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Glasgow-haskell-users <glasgow-haskell-users-bounces@haskell.org>
<b>On Behalf Of </b>Anthony Clayden<br>
<b>Sent:</b> 25 March 2019 11:50<br>
<b>To:</b> GHC Users List <glasgow-haskell-users@haskell.org>; Tom Schrijvers <tom.schrijvers@cs.kuleuven.be><br>
<b>Subject:</b> Re: Equality constraints (~): type-theory behind them<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">> <span style="color:black">On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote:</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">Thanks Tom, I've also been working through the 2011 expanded version of '</span>System F with Type Equality Coercions<span style="color:black">' that Adam suggested.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">I'm finding your 2017 paper's proposals not up to the job, because it doesn't consider FunDeps for Overlapping Instances; and unnecessary because the examples it's addressing can be fixed purely using FunDeps,
with their semantics per the 2006 'via CHRs' paper. The chief problems with using FunDeps in GHC code is GHC doesn't follow that semantics; neither does it follow any other well-principled/documented semantics.You can get it to accept a bunch of instances
then find that taken together they're not consistent and confluent, in the sense of the 'via CHRs' paper.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">Specifically, re the 2017's paper Challenge 1: Enforcing (essentially Trac #10675). That set of instances in the example is not valid by the 'via CHRs' rules, and should be rejected. Hugs indeed rejects that code.
GHC accepts it and #10675 shows what sort of incoherence can result. I'm not seeing we need to translate to Type Families/System FC to explain it.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:black">Re Challenge 2: Elaborating (which is Trac #9627 that gives the main example for the paper). We can fix that code with an extra `~` constraint:</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<pre><span class="gmail-line"> class C a b | a -> b</span><o:p></o:p></pre>
<pre><span class="gmail-line"> instance C Int Bool</span><o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre><span class="gmail-line"> f :: (C Int b, b ~ Bool) => b -> Bool</span><o:p></o:p></pre>
<pre><span class="gmail-line"> f x = x </span><o:p></o:p></pre>
<pre><span class="gmail-line">(Or in Hugs with a `TypeCast` instead of the `~`.)</span><o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre><span class="gmail-line">Is that extra constraint onerous? The signature already has `Bool` hard-coded as the return type, so I don't see it's any more onerous.</span><o:p></o:p></pre>
<pre><span class="gmail-line">Or put that signature as</span><o:p></o:p></pre>
<pre><span class="gmail-line"> f :: (C Int b) => b -> b</span><o:p></o:p></pre>
<pre><span class="gmail-line">Which also has the effect `b` must be `Bool`.</span><o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre>I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity.<o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre>AntC<o:p></o:p></pre>
</div>
</div>
</div>
</div>
</body>
</html>