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_clay...@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/proposals/0000-instance-apartness-guards.rst#injective-type-families > > but I don't see it helping here. > plug2 (this example) > > https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-coincident-overlap > > 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 >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
