[was ghc-devs] Reasoning backwards with type families

[Carter Schonwald]

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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171212/ae6bf9b1/attachment.html>