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
