<div><div dir="auto">This was / perhaps still is one goal of injective type families too!  I’m not sure why the current status is, but it’s defjnitely related </div><br><div class="gmail_quote"><div>On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz">anthony_clayden@clear.net.nz</a>> wrote:<br></div><blockquote class="gmail_quote" 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>
(Moving to ghc-users, there's nothing particularly dev-y.)<br>
<br>
> Sometimes it woulld be useful to be able to reason<br>
backwards<br>
> about type families.<br>
<br>
Hi David, this is a well-known issue/bit of a sore.<br>
Discussed much in the debate between type families<br>
compared to FunDeps.<br>
<br>
> For example, we have<br>
><br>
> type family a && b where<br>
>   'False && b      = 'False<br>
>   'True  && b      = b<br>
>   a      && 'False = 'False<br>
>   a      && 'True  = a<br>
>   a      && a      = a<br>
<br>
> ... if we know something about the *result*,<br>
> GHC doesn't give us any way to learn anything about the<br>
arguments.<br>
<br>
You can achieve the improvement you want today.<br>
<br>
You'll probably find Oleg has a solution<br>
With FunDeps and superclass constraints, it'll go like this<br>
<br>
class (OnResult r a b, OnResult r b a) => And a b r | a b -><br>
r<br>
<br>
instance And 'False b 'False<br>
-- etc, as you'd expect following the tf equations<br>
-- the instances are overlapping but confluent<br>
<br>
class OnResult r a b | r a -> b<br>
instance OnResult 'True a 'True<br>
instance OnResult 'False 'True 'False<br>
<br>
You could equally make `OnResult` a type family.<br>
<br>
If you can trace backwards to where `&&` is used,<br>
you might be able to add suitable constraints there.<br>
<br>
So there's a couple of futures:<br>
* typechecker plugins, using an SMT solver<br>
* injective type families<br>
   the next phase is supposed to allow<br>
<br>
type family a && b = r | r a -> b, r b -> a where ...<br>
<br>
That will help with some type families<br>
(such as addition of Nats),<br>
plug1<br>
<a href="https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#injective-type-families" rel="noreferrer" target="_blank">https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#injective-type-families</a><br>
<br>
but I don't see it helping here.<br>
plug2 (this example)<br>
<a href="https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-coincident-overlap" rel="noreferrer" target="_blank">https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-coincident-overlap</a><br>
<br>
Because (for example) if you unify the first two equations,<br>
(that is, looking for coincident overlap)<br>
<br>
    'False && 'False = 'False<br>
    'True && 'False = 'False<br>
<br>
That's inconsistent on dependency ` r b -> a`.<br>
<br>
And you can't fix it by re-ordering the closed equations.<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>
<br>
> ...<br>
> I wouldn't necessarily expect GHC<br>
> to be able to work something like this out on its own.<br>
<br>
That's a relief ;-)<br>
<br>
> But it seems like there should be some way to allow the<br>
user<br>
> to guide it to a proof.<br>
<br>
Yes, an SMT solver with a model for kind `Bool`.<br>
(And a lot of hard work to teach it, by someone.)<br>
<br>
AntC<br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div></div>