> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
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 On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden <[hidden email]> wrote: > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald <[hidden email]> wrote:
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
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead <[hidden email]> wrote:
Cool!
OK. That's as per the type-level addition of Nats I mentioned. Did you consider using FunDeps instead of Injective Type Families? (I see lower down that page, type C is described as 'generalized' injectivity.) 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: * some values of the result determine (some of) the arguments; and/or * some values of the result with some values of some arguments determine other arguments; but * for some values of the result and/or some arguments, we can't determine the other arguments. You can kinda achieve that now using FunDeps with overlapping instances with UndecidableInstances exploiting GHC's bogus consistency check on FunDeps https://ghc.haskell.org/trac/ghc/ticket/10675#comment:15. Or maybe with (Closed) Type Families if you put a bogus catch-all at the end of the sequence of equations: > type family F a where > ... > F a = F a (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.) None of it is sound or complete or rugged, in particular you can't risk orphan instances -- unless plug3: https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-351289722 AntC
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by AntC
I still haven't really digested what you've written, but I wish to pick a nit (below)
On Nov 20, 2017 3:44 AM, "Anthony Clayden" <[hidden email]> wrote: > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: I don't think this is entirely correct. The fact that Bool is closed does not seem relevant. The key fact, I believe, is that (&&) is closed. Asking GHC to reason like this about open type families smells much harder, but maybe my sense of smell is off. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by AntC
Hi AntC 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). The trick is teaching GHC to do all the type trickery it needs so you can write things like: ((f1,g1), Just h1, [x1,x2]) . ((f2,g2), Nothing. [y1,y2,y3]) 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. 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. Although, I'd love people to look at the code, play with it and suggest improvements. Clinton On Thu, Dec 14, 2017 at 12:33 PM, Anthony Clayden <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by David Feuer
On Thu, 14 Dec 2017 at 3:19 PM, David Feuer <[hidden email]> wrote:
Thanks David. Heh, heh. I think we might be agreeing about the phenomenon, but picking different nits to 'blame'.
Hmm. I wonder what you think "closed" amounts to? Equation 1 `'False && b = 'False` is consistent with `[b ~ Foo]` (unless GHC were to reason about closed kinds) Equation 2 `'True && b = b ` is consistent with `[b ~ Foo]` And so on. The last equation `a && a = a` is consistent with `[a ~ Foo]`. Furthermore it's *inconsistent* with a putative backwards FunDep ` r a -> b` on `'False && 'True ~ 'False`. I think it would be better to omit that equation all together. Then when your o.p. reasons: >>> ... we can calculate (Not a || Not b) as 'True for each of these LHSes. What will it calculate for (Not Foo)?
Hmm. Your o.p. said >>> In order for the constraint (a && b) ~ 'True to hold, the type family application *must have reduced* using one of its equations.
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Clinton Mead
On Thu, 14 Dec 2017 at 4:13 PM, Clinton Mead <[hidden email]> wrote:
;-) Fair enough. "bogus" is SPJ's way of saying: it works, but it isn't supported by deep type theory. 'C'est brutal mais ca marche.' And that particular exploit has been stable since 2004 at least: the HList library totally relied on it until Closed Type Families arrived. AntC _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Happy to go with the bogusness if it works better than injective types, feel free to submit a patch. :) On Thu, 14 Dec 2017 at 9:08 pm, Anthony Clayden <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Free forum by Nabble | Edit this page |