<div dir="ltr"><div dir="ltr">On Tue, Mar 26, 2019 at 1:05 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br></div><div dir="ltr"><br></div><div>Whoa, whoa. Your reply is making a number of presuppositions, and putting words in my mouth I did not say.</div><div><br></div><div>Firstly: I am totally in favour of a typed intermediate language. Then the question is what type-theory do we use within the IR? Well it should be one that fits the surface language.</div><div><br></div><div>System F-in-general broadly fits functional languages in general. Does System FC in particular fit Haskell specifically? I've seen no demonstration of that; and there are reasons to think it's only an approximate fit. That's why I've talked about "squeezing" and "straitjacket".</div><div><br></div><div>Quite apart from FunDeps: does FC fit nicely to overlapping instances? I think not. Does FC fit nicely to Type Families? "<span style="color:rgb(0,0,0);font-family:"Lucida Grande",helvetica,arial,verdana,sans-serif;font-size:15.12px">type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions.</span>" say Eisenberg and Morris 2017. So that's a 'No'. E&M go on to translate Type Families into something that looks more like FunDeps, to my eye.</div><div><br></div><div>The whole point about FunDeps is they are constrained by typeclasses. So they don't suffer those complications.</div><div><br></div><div>One of the reasons coders prefer FunDeps is because they can use Overlapping Instances. Then for Schrijvers et al to translate FunDeps to Type Families that a) don't accommodate Overlaps; and b) use a feature (Type Families) that introduce "nonsensical types" and "complicating the metatheory" looks a fortiori like a poor fit.</div><div><br></div><div>> There may be an IR based on fundeps, or CHRs or something, that has similar properties to FC.</div><div><br></div><div>Perhaps it's already in FC and it's hiding in plain sight: the 'via CHRs' paper gives its rules in terms of quantified implications (or bi-implications). We now have in GHC the beginnings of Quantified/implication constraints. How are they translated into FC? I've tried looking at the Oliveira et al 2017 paper (section 5), but it's too dense for me. I can see it's in terms of constructing dictionaries, not Type Families. Tom should understand this far better than me: he and George are among the et al. Yet despite all 3 papers I've mentioned dating to 2017, there seems to be no mutual recognition. Tom+George's paper doesn't say they've considered Quantified/implication constraints amongst 'Related Work'. Yet this logic screams at me:</div><div><pre><span class="gmail-m_-2823694426909329247gmail-line"> class C a b | a -> b, b -> a -- two-way FunDeps</span></pre><pre> instance C Int Bool</pre><pre>Mark Jones and the 'via CHRs' paper says that translates to axioms</pre></div><div><br></div><div> (forall b. C Int b => b ~ Bool, forall a. C a Bool => a ~ Int)</div><div><br></div><div>That is actual legal code in GHC today, as a constraint. Then all I need is a way to get those axioms into the program's type theory, presuming it can be expressed in FC. Look how succinct that constraint is, compare to introducing two Type Families, one for each direction of the FunDeps; and two TF instances; and two `~` superclass constraints. (I know the Schrijvers et al translates to Associated Types. But those are just sugar for top-level TFs, so they don't avoid the complications E&M talk about.)</div><div><br></div><div>> I’d be happy to help explain how the current machinery works.</div><div><br></div><div>Thank you. Is there somewhere a write-up/dummies guide for how GHC translates Quantified/implication constraints into FC?</div><div><br></div><div>One further thing:</div><div><br></div><div>> there may be aspects of GHC’s implementation fundeps that are unsatisfactory or argualbly just plain wrong,</div><div><br></div><div>Yes there are. You can write code in GHC that is just incoherent. There's no hope of translating it into any type theory, and nobody should try. The tenor of your message is that the "just plain wrong" bits are still an open question. Not so: all the explanations are in the 'via CHRs' paper (not to mention flagged with Notes inside GHC source that say "bogus"). There are programs that the 'via CHRs' rules say should be rejected, but that GHC on the face of it accepts. You then find those programs are unusable/can only be used if you're very careful with your function signatures. My rule of thumb is: if Hugs accepts the code, then it will be coherent. If Hugs rejects, the error message corresponds to a rule in 'via CHRs'. No further research needed.</div><div><br></div><div>AntC</div><div dir="ltr"><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-GB">
<div class="gmail-m_-2823694426909329247WordSection1">
<pre style="margin-left:36pt">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.<u></u><u></u></pre>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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. <u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-top:none;border-right:none;border-bottom:none;border-left:1.5pt solid blue;padding:0cm 0cm 0cm 4pt">
<div>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(225,225,225);padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Glasgow-haskell-users <<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-bounces@haskell.org</a>>
<b>On Behalf Of </b>Anthony Clayden<br>
<b>Sent:</b> 25 March 2019 11:50<br>
<b>To:</b> GHC Users List <<a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a>>; Tom Schrijvers <<a href="mailto:tom.schrijvers@cs.kuleuven.be" target="_blank">tom.schrijvers@cs.kuleuven.be</a>><br>
<b>Subject:</b> Re: Equality constraints (~): type-theory behind them<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">> <span style="color:black">On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote:</span><u></u><u></u></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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<pre><span class="gmail-m_-2823694426909329247gmail-line"> class C a b | a -> b</span><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line"> instance C Int Bool</span><u></u><u></u></pre>
<pre><u></u> <u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line"> f :: (C Int b, b ~ Bool) => b -> Bool</span><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line"> f x = x </span><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line">(Or in Hugs with a `TypeCast` instead of the `~`.)</span><u></u><u></u></pre>
<pre><u></u> <u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-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><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line">Or put that signature as</span><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line"> f :: (C Int b) => b -> b</span><u></u><u></u></pre>
<pre><span class="gmail-m_-2823694426909329247gmail-line">Which also has the effect `b` must be `Bool`.</span><u></u><u></u></pre>
<pre><u></u> <u></u></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.<u></u><u></u></pre>
<pre><u></u> <u></u></pre>
<pre>AntC<u></u><u></u></pre>
</div>
</div>
</div>
</div>
</div>
</blockquote></div></div>