<div><br><div class="gmail_quote"><div dir="auto">On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead <<a href="mailto:redirect@vodafone.co.nz">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>Injective Type Families are at the core of my "Freelude" package, which allows many more types to be defined as Categories, Functors, Applicatives and Monads. </div></blockquote><div dir="auto"><br></div><div dir="auto">Cool!</div><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><br></div><div>What would also be helpful is if injectivity of type C as mentioned on the page ...</div></div></blockquote><div dir="auto"><br></div><div dir="auto">OK. That's as per the type-level addition of Nats I mentioned. Did you consider using FunDeps instead of Injective Type Families?</div><div dir="auto"><br></div><div dir="auto">(I see lower down that page, type C is described as 'generalized' injectivity.)</div><div dir="auto"><br></div><div dir="auto">The variety of injectivity David F's o.p. talked about is orthogonal across types A, B, C. We might call it 'partial injectivity' as in partial function:</div><div dir="auto">* some values of the result determine (some of) the arguments; and/or</div><div dir="auto">* some values of the result with some values of some arguments determine other arguments; but</div><div dir="auto">* for some values of the result and/or some arguments, we can't determine the other arguments.</div><div dir="auto"><br></div><div dir="auto">You can kinda achieve that now using FunDeps with overlapping instances with UndecidableInstances exploiting GHC's bogus consistency check on FunDeps <a href="https://ghc.haskell.org/trac/ghc/ticket/10675#comment:15">https://ghc.haskell.org/trac/ghc/ticket/10675#comment:15</a>.</div><div dir="auto"><br></div><div dir="auto">Or maybe with (Closed) Type Families if you put a bogus catch-all at the end of the sequence of equations:</div><div dir="auto"><br></div><div dir="auto">> type family F a where</div><div dir="auto">>   ...</div><div dir="auto">>   F a = F a</div><div dir="auto"><br></div><div dir="auto">(But then it can't be injective, so you have to stitch it together with type classes and superclass equality constraints and who-knows-what.)<br></div><div dir="auto"><br></div><div dir="auto">None of it is sound or complete or rugged, in particular you can't risk orphan instances -- unless plug3: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-351289722">https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-351289722</a></div><div dir="auto"><br></div><div dir="auto">AntC</div><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><br></div></div><div class="gmail_extra"><div class="gmail_quote">On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden <span><<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><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="m_-5353410098934350088h5"><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-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#injective-type-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-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-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>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.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-bin/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div></div>
</blockquote></div></div></div></div>
<br>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.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-bin/mailman/listinfo/glasgow-haskell-users</a><br>
<br></blockquote></div><br></div>
</blockquote></div></div>