<div><br><div class="gmail_quote"><div dir="auto">On Thu, 14 Dec 2017 at 3:19 PM, David Feuer <<a href="mailto:redirect@vodafone.co.nz">redirect@vodafone.co.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">I still haven't really digested what you've written, but I wish to pick a nit (below)<br><div class="gmail_extra" dir="auto"></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Thanks David. Heh, heh. I think we might be agreeing about the phenomenon, but picking different nits to 'blame'.</div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div class="gmail_extra" dir="auto"><br><div class="gmail_quote"></div></div></div><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote">On Nov 20, 2017 3:44 AM, "Anthony Clayden" <<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>> wrote:<br type="attribution"></div></div></div><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_2277495843905463485m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:<br>
<br></blockquote></div></div></div><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_2277495843905463485m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">...</blockquote></div></div></div><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_2277495843905463485m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
<br>
> For (&&), the obvious things you'd want are ...<br>
><br>
> There's nothing inherently impossible about this sort of<br>
reasoning.<br>
<br>
No-ish but. It relies on knowing kind `Bool` is closed.<br>
And GHC doesn't pay attention to that.<br>
So you need to bring type family `Not`<br>
into the reasoning; hence a SMT solver.<br></blockquote></div></div></div><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_2277495843905463485m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I don't think this is entirely correct. The fact that Bool is closed does not seem relevant. The key fact, I believe, is that (&&) is closed.</div></div></blockquote><div dir="auto"><br></div><div dir="auto">Hmm. I wonder what you think "closed" amounts to? </div><div dir="auto"><br></div><div dir="auto">Equation 1 `'False && b = 'False` is consistent with `[b ~ Foo]`</div><div dir="auto"> (unless GHC were to reason about closed kinds)</div><div dir="auto"><br></div><div dir="auto">Equation 2 `'True && b = b ` is consistent with `[b ~ Foo]`</div><div dir="auto"><br></div><div dir="auto">And so on.</div><div dir="auto"><br></div><div dir="auto">The last equation `a && a = a` is consistent with `[a ~ Foo]`.</div><div dir="auto">Furthermore it's *inconsistent* with a putative backwards FunDep ` r a -> b` on `'False && 'True ~ 'False`.</div><div dir="auto">I think it would be better to omit that equation all together.</div><div dir="auto"><br></div><div dir="auto">Then when your o.p. reasons:</div><div dir="auto"><br></div><div dir="auto">>>> ... <span style="white-space:pre-wrap;background-color:rgb(255,255,255)">we can calculate (Not a || Not b) as 'True for each of these LHSes.</span></div><div dir="auto"><br></div><div dir="auto">What will it calculate for (Not Foo)?</div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div dir="auto"> Asking GHC to reason like this about open type families smells much harder, but maybe my sense of smell is off.</div><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_2277495843905463485m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div></div></div>
</blockquote></div></div><div dir="auto">Hmm. Your o.p. said</div><div dir="auto"><br></div><div dir="auto">>>> <span style="white-space:pre-wrap;background-color:rgb(255,255,255)">In order for the </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">constraint (a && b) ~ 'True to hold, the type family application *must have reduced* </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">using one of its equations.</span></div><pre style="white-space:pre-wrap;background-color:rgb(255,255,255)"><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">I think that's smelly logic: if you want to reason backwards, then you can't make assumptions about what "must" have reduced if GHC were reasoning forward. That is, unless you're expecting GHC to behave like an SMT solver over closed kinds.</span><br></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)"><br></span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">Remember that the logic for selecting Closed Type Family equations works from top to bottom *ignoring anything known about the result*. So not only must it have reduced using one of the equations; it must have rejected equations above the one it selected; and it must have seen evidence for rejecting them. (It's more complicated than that in practice: if there's coincident overlap, GHC will pick some equation eagerly. And your `&&` equations exhibit coincident overlap, apart from the last.)</span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)"><br></span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">If you want it to benefit from something known about the result, you won't (in general) find the same top-to-bottom sequence helps with type improvement. With the FunDep inconsistency in your last equation for `&&`, I suspect that equation-selection will get 'stuck' looking for evidence to reject earlier equations.</span><br></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)"><br></span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">If we do expect GHC to behave like an SMT solver over closed kinds, then it can reason just as well for an open type family; on the proviso that it can see all the equations.</span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)"><br></span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">For a bit of history: during discussions around Injective Type Families, one suggestion was to infer injectivity by examining the equations given -- along the lines you're positing. That was rejected on grounds the equations might exhibit injectivity 'by accident'. Also that the programmer might intend injectivity, but their equations be inconsistent. So it was decided there must be explicit declaration; and the equations must be consistent with that declaration. No equations for `&&` could be consistent that way.</span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)"><br></span></div><div dir="auto"><span style="font-family:-apple-system,HelveticaNeue;white-space:normal;background-color:rgb(253,253,253)">AntC</span></div></pre>