<div dir="ltr">Injective Type Families are at the core of my "Freelude" (<a href="https://hackage.haskell.org/package/freelude">https://hackage.haskell.org/package/freelude</a>) package, which allows many more types to be defined as Categories, Functors, Applicatives and Monads. <div><br></div><div>For example you can define a tuple of categories as a category and then:</div><div><br></div><div>(f1, f2) . (g1 . g2) = (f1 . g1, f2 . g2)</div><div><br></div><div>as one would expect.</div><div><br></div><div>Also one can define symmetric versions on tuples "fmap", for example:</div><div><br></div><div>fmap (*2) (3,4,5) = (6,8,10)</div><div><br></div><div>The library is currently basically a proof of concept but it wouldn't be possible without Injective Type Families.</div><div><br></div><div>What would also be helpful is if injectivity of type C as mentioned on the page (<a href="https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies">https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies</a>) 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"). </div><div><br></div><div>Cheers,</div><div><br></div><div>Clinton</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden <span dir="ltr"><<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><br><div class="gmail_quote"><span class=""><div dir="auto">On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald <<a href="mailto:redirect@vodafone.co.nz" target="_blank">redirect@vodafone.co.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div dir="auto">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 </div></div></blockquote><div dir="auto"><br></div></span><div dir="auto">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?</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">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?</div><div dir="auto"><br></div><div dir="auto">Is anybody out there using Injective Type Families currently? What for?</div><div dir="auto"><br></div><div dir="auto">AntC</div><div><div class="h5"><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div dir="auto"></div><br><div class="gmail_quote"><div>On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:<br>
<br>
(Moving to ghc-users, there's nothing particularly dev-y.)<br>
<br>
> Sometimes it woulld be useful to be able to reason<br>
backwards<br>
> about type families.<br>
<br>
Hi David, this is a well-known issue/bit of a sore.<br>
Discussed much in the debate between type families<br>
compared to FunDeps.<br>
<br>
> For example, we have<br>
><br>
> type family a && b where<br>
>   'False && b      = 'False<br>
>   'True  && b      = b<br>
>   a      && 'False = 'False<br>
>   a      && 'True  = a<br>
>   a      && a      = a<br>
<br>
> ... if we know something about the *result*,<br>
> GHC doesn't give us any way to learn anything about the<br>
arguments.<br>
<br>
You can achieve the improvement you want today.<br>
<br>
You'll probably find Oleg has a solution<br>
With FunDeps and superclass constraints, it'll go like this<br>
<br>
class (OnResult r a b, OnResult r b a) => And a b r | a b -><br>
r<br>
<br>
instance And 'False b 'False<br>
-- etc, as you'd expect following the tf equations<br>
-- the instances are overlapping but confluent<br>
<br>
class OnResult r a b | r a -> b<br>
instance OnResult 'True a 'True<br>
instance OnResult 'False 'True 'False<br>
<br>
You could equally make `OnResult` a type family.<br>
<br>
If you can trace backwards to where `&&` is used,<br>
you might be able to add suitable constraints there.<br>
<br>
So there's a couple of futures:<br>
* typechecker plugins, using an SMT solver<br>
* injective type families<br>
   the next phase is supposed to allow<br>
<br>
type family a && b = r | r a -> b, r b -> a where ...<br>
<br>
That will help with some type families<br>
(such as addition of Nats),<br>
plug1<br>
<a href="https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#injective-type-families" rel="noreferrer" target="_blank">https://github.com/AntC2/ghc-<wbr>proposals/blob/instance-<wbr>apartness-guards/proposals/<wbr>0000-instance-apartness-<wbr>guards.rst#injective-type-<wbr>families</a><br>
<br>
but I don't see it helping here.<br>
plug2 (this example)<br>
<a href="https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-coincident-overlap" rel="noreferrer" target="_blank">https://github.com/AntC2/ghc-<wbr>proposals/blob/instance-<wbr>apartness-guards/proposals/<wbr>0000-instance-apartness-<wbr>guards.rst#type-family-<wbr>coincident-overlap</a><br>
<br>
Because (for example) if you unify the first two equations,<br>
(that is, looking for coincident overlap)<br>
<br>
    'False && 'False = 'False<br>
    'True && 'False = 'False<br>
<br>
That's inconsistent on dependency ` r b -> a`.<br>
<br>
And you can't fix it by re-ordering the closed equations.<br>
<br>
> For (&&), the obvious things you'd want are ...<br>
><br>
> There's nothing inherently impossible about this sort of<br>
reasoning.<br>
<br>
No-ish but. It relies on knowing kind `Bool` is closed.<br>
And GHC doesn't pay attention to that.<br>
So you need to bring type family `Not`<br>
into the reasoning; hence a SMT solver.<br>
<br>
> ...<br>
> I wouldn't necessarily expect GHC<br>
> to be able to work something like this out on its own.<br>
<br>
That's a relief ;-)<br>
<br>
> But it seems like there should be some way to allow the<br>
user<br>
> to guide it to a proof.<br>
<br>
Yes, an SMT solver with a model for kind `Bool`.<br>
(And a lot of hard work to teach it, by someone.)<br>
<br>
AntC<br>
______________________________<wbr>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.<wbr>org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/glasgow-<wbr>haskell-users</a><br>
</blockquote></div></div>
</blockquote></div></div></div></div>
<br>______________________________<wbr>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.<wbr>org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/glasgow-<wbr>haskell-users</a><br>
<br></blockquote></div><br></div>