[was ghc-devs] Reasoning backwards with type families

[Clinton Mead]

Injective Type Families are at the core of my "Freelude" (
https://hackage.haskell.org/package/freelude) package, which allows many
more types to be defined as Categories, Functors, Applicatives and Monads.

For example you can define a tuple of categories as a category and then:

(f1, f2) . (g1 . g2) = (f1 . g1, f2 . g2)

as one would expect.

Also one can define symmetric versions on tuples "fmap", for example:

fmap (*2) (3,4,5) = (6,8,10)

The library is currently basically a proof of concept but it wouldn't be
possible without Injective Type Families.

What would also be helpful is if injectivity of type C as mentioned on the
page (https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies) but
unfortunately this is currently not implemented so I've worked around this
where possible (this is largely the reason why the library splits
"Functors" and "ExoFunctors").

Cheers,

Clinton

On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

>
> 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
>>>
>>
> _______________________________________________
> 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/51c6fac6/attachment-0001.html>