Explicit inequality evidence

[Carter Schonwald]

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" <rae at 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.feuer at gmail.com> wrote:
> >
> > On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <oleg.grenrus at 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161214/ea44d2bf/attachment.html>