Out of curiosity: where's the current type safety proof, and is it mechanized?
Oleg On 13.12.2016 17:01, Richard Eisenberg 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 >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs