<div dir="ltr">Hi AntC<br><br>I've panicked GHC enough whilst developing Freelude so whilst I'm not sure exactly what you're saying I'd be hestiant about exploiting anything bogus (8.2 btw seems far more stable than 8.0 btw). <div><br>The trick is teaching GHC to do all the type trickery it needs so you can write things like:</div><div><br></div><div>((f1,g1), Just h1, [x1,x2]) . ((f2,g2), Nothing. [y1,y2,y3])</div><div><br></div><div>Under Freelude this should happily compile (assuming all the bits are categories themselves such as functions). Pairs of categories is a category, Maybe of a category is a category, and a list of categories is a category, and finally a triple of categories is a category. So composition should be defined. </div><div><br></div><div>I'm no expert in the GHC type system (I don't really know any type theory at all) but from what I observed injectivity allows the compiler to "dig" all the way down this chain whilst still leaving some breadcrumbs to find it's way back up. It's the two way equivalence that seems to help, GHC can jump back and forth. I've tried this with non injective type families and just making "inverse" type families but it just seems to end in tears and a mass of type mismatches. <br><br>Although, I'd love people to look at the code, play with it and suggest improvements.</div><div><br></div><div>Clinton</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 14, 2017 at 12:33 PM, 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"><div dir="auto">On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead <<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>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" target="_blank">https://ghc.haskell.<wbr>org/trac/ghc/ticket/10675#<wbr>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" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals/pull/<wbr>56#issuecomment-351289722</a></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><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_3670645637805871987m_-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-<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" 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>
<br></blockquote></div><br></div>
</blockquote></div></div></div></div>
</blockquote></div><br></div>