On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead <redir...@vodafone.co.nz> wrote:
> 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. > Cool! > What would also be helpful is if injectivity of type C as mentioned on the > page ... > 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 > On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden < > anthony_clay...@clear.net.nz> wrote: > >> >> On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald <redir...@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_clay...@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@haskell.org >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >>>> >>> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >> >> >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users