Possibly naive question: do we have decidable inequality in a meta theoretical sense? I feel like we have definite equality and fuzzy might not always be equal but could be for polymorphic types. And that definite inequality on non polymorphic terms is a lot smaller than what folks likely want?
On Dec 13, 2016 10:01 AM, "Richard Eisenberg" <r...@cs.brynmawr.edu> wrote: > I've thought about inequality on and off for years now, but it's a hard > nut to crack. If we want this evidence to affect closed type family > reduction, then we would need evidence of inequality in Core, and a > brand-spanking-new type safety proof. I don't wish to discourage this > inquiry, but I also don't think this battle will be won easily. > > Richard > > > On Dec 13, 2016, at 1:02 AM, David Feuer <david.fe...@gmail.com> wrote: > > > > On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <oleg.gren...@iki.fi> > wrote: > >> First the bike shedding: I’d prefer /~ and :/~:. > > > > Those are indeed better. > > > >> new Typeable [1] would actually provide heterogenous equality: > >> > >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > >> TypeRep a -> TypeRep b -> Maybe (a :~~: b) > >> > >> And this one is tricky, should it be: > >> > >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > >> TypeRep a -> TypeRep b -> > >> Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) > >> > >> i.e. how kind inequality would work? > > > > I don't know. It sounds like some details of how kinds are expressed > > in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe > > we should punt and use heterogeneous inequality? That's over my head. > > > >> I'm not sure about propagation rules, with inequality you have to be > *very* careful! > >> > >> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. > >> > >> 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. > > > >> Also: > >> > >> f x ~ a -> b, is true with f ~ (->) a, x ~ b. > > > > Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just > > leave out that bogus piece. > > > > Thanks, > > David Feuer > > _______________________________________________ > > ghc-devs mailing list > > ghc-devs@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs