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 On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden < anthony_clayden@clear.net.nz> wrote:
On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:
(Moving to ghc-users, there's nothing particularly dev-y.)
Sometimes it woulld be useful to be able to reason backwards about type families.
Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type families compared to FunDeps.
For example, we have
type family a && b where 'False && b = 'False 'True && b = b a && 'False = 'False a && 'True = a a && a = a
... if we know something about the *result*, GHC doesn't give us any way to learn anything about the arguments.
You can achieve the improvement you want today.
You'll probably find Oleg has a solution With FunDeps and superclass constraints, it'll go like this
class (OnResult r a b, OnResult r b a) => And a b r | a b -> r
instance And 'False b 'False -- etc, as you'd expect following the tf equations -- the instances are overlapping but confluent
class OnResult r a b | r a -> b instance OnResult 'True a 'True instance OnResult 'False 'True 'False
You could equally make `OnResult` a type family.
If you can trace backwards to where `&&` is used, you might be able to add suitable constraints there.
So there's a couple of futures: * typechecker plugins, using an SMT solver * injective type families the next phase is supposed to allow
type family a && b = r | r a -> b, r b -> a where ...
That will help with some type families (such as addition of Nats), plug1
https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/propos...
but I don't see it helping here. plug2 (this example)
https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/propos...
Because (for example) if you unify the first two equations, (that is, looking for coincident overlap)
'False && 'False = 'False 'True && 'False = 'False
That's inconsistent on dependency ` r b -> a`.
And you can't fix it by re-ordering the closed equations.
For (&&), the obvious things you'd want are ...
There's nothing inherently impossible about this sort of reasoning.
No-ish but. It relies on knowing kind `Bool` is closed. And GHC doesn't pay attention to that. So you need to bring type family `Not` into the reasoning; hence a SMT solver.
... I wouldn't necessarily expect GHC to be able to work something like this out on its own.
That's a relief ;-)
But it seems like there should be some way to allow the user to guide it to a proof.
Yes, an SMT solver with a model for kind `Bool`. (And a lot of hard work to teach it, by someone.)
AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users