[was ghc-devs] Reasoning backwards with type families

[Anthony Clayden]

On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald <redirect at vodafone.co.nz>
wrote:

> 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
>

Thanks Carter, yes this sort of injectiviy (semi-injectivity? partial
injectivity?) is noted as future work in the 2015 paper. But I'm not seeing
a lot of hollerin' for it(?) Or am I looking in the wrong places?

The classic example is for Nats in length-indexed vectors: if we know the
length of appending two vectors, and one of the arguments, infer the length
of the other. (Oleg provided a solution using FunDeps more than a decade
ago.) But GHC has special handling for type-level Nats (or rather Ints),
hence no need to extend injectivity.

Come to that, the original work that delivered Injective Type Families
failed to find many use cases -- so the motivation was more
keep-up-with-the-Jones's to provide equivalence to FunDeps.

There were lots of newbie mistakes when Type Families first arrived, of
thinking they were injective, because a TF application looks like a type
constructor application `F Int` cp `T Int`. But perhaps that
misunderstanding didn't represent genuine use cases?

Is anybody out there using Injective Type Families currently? What for?

AntC


> 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/20171214/9f7bcec9/attachment.html>