[was ghc-devs] Reasoning backwards with type families
Anthony Clayden
anthony_clayden at clear.net.nz
Mon Nov 20 08:43:29 UTC 2017
> 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
More information about the Glasgow-haskell-users
mailing list