[transferring to -users, because there's a much wider
discussion] > > On Dec 13, 2016, at 15:04, Richard Eisenberg wrote: > > I've thought about inequality on and off for years now, The subject has appeared (in various guises) on Haskell forums since well before 2002 [1] -- which went into the 'OutsideIn(X)' model. Search the cafe on 'type disequality', for example. > >> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: > >> First the bike shedding: Id prefer /~ and :/~:. And yes, usually discussed with /~ as the type inequality operator, since at least when ~ was introduced for type equality. > > ... but it's a hard nut to crack. Which is presumably why spj has never shown any interest. > > ... need evidence of inequality in Core, and > > a brand-spanking-new type safety proof. ... One rule of inference that David/Oleg haven't mentioned: If x /~ y and y ~ z then x /~ z. How does this go with (potentially) infinite type (family)s? Thanks Richard for the refs on type safety proofs. I wonder if anything in type safety relies on inequalities? (This would be with, say, overlaps + fundeps extensions.) FunDep 'confluence' (which Richard has re-christened 'coincident overlap' for closed type families), surely relies on proving at some use site that the types can never unify with such-and-such instance (or type family equation). For example if we have instance C a a where ... instance C a b where... We have to prove at a use site that the two types cannot unify, to justify picking the second instance. This goes badly with separate compilation: suppose the `C a a` instance is not visible in every module. I would love type inequality guards on instances to be explored as an alternative approach for overlap. (See some of my reponses to Richard [2].) In my example above: instance C a b | a /~ b where ... So the invisibility of the `C a a` instance would not upset any use sites. [1] Sulzmann and Stuckey 2002 'A theory of Overloading' [2] https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/ AntC _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
> On Dec 13, 2016, at 1:02 AM, David Feuer <david.feuer at
gmail.com> wrote: > >> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <oleg.grenrus at iki.fi> wrote: >> >> I assume that in your rules, variables are not type families, otherwise >> >> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x where F x = ()) >> other direction is true though. > > I was definitely imagining them as first-class types; your point that > f x /~ f y => x /~ y even if f is a type family is an excellent one. > Hmm, yes except: how would evidence ever arise that f x /~ f y ? Would we ever get a 'wanted' constraint to that effect? More likely, we'd be trying to discriminate between instances in which picking some instance depends on f x /~ f y. I don't see that any of the overlap/closed type family work has got us away from the 'groundedness issues' observed in the HList paper. We have to improve both types to a grounded type constructor to get the evidence they're not equal. (Or at least that parameters in the same position are not equal, and that the type constructors are not familys and are the same arity.) AntC _______________________________________________ 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 |