> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote: > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Free forum by Nabble | Edit this page |