Heterogeneous equality into base?

[David Feuer]

That's the idea I was after. Is it good for anything?

On Jul 10, 2017 2:06 PM, "Edward Kmett" <ekmett at gmail.com> wrote:

>
>
> Sent from my iPad
>
> > On Jul 10, 2017, at 1:11 PM, David Feuer <david.feuer at gmail.com> wrote:
> >
> > Well, I came up with another notion of heterogeneous equality (much,
> > much more limited in practice):
> >
> > newtype HEqual (a :: j) (b :: k) = HEqual (forall (f :: forall l. l ->
> > Type). f a -> f b)
>
> This is "heterogeneous Leibnizian equality".
>
> > Implementing
> >
> > fromHEqual :: forall j k (a :: j) (b :: k). HEqual a b -> a :~~: b
> > seems to require something like OtherEquality.
> >
> > I'm not sure what you mean about not being able to reorder type
> > indices. OtherEquality can also be defined as a newtype around (:~~:):
> >
> > newtype OtherEquality :: forall j. j -> forall k. k -> Type where
> >  OtherEquality :: a :~~: q -> OtherEquality a q
> >
> > But perhaps you mean it's more convenient than :~~:?
> >
> >> On Mon, Jul 10, 2017 at 1:03 PM, Richard Eisenberg <rae at cs.brynmawr.edu>
> wrote:
> >> This OtherEquality is actually a tad bit more general, given that GHC
> can't (currently) reorder type indices. But would anyone take advantage of
> the generality? I tend to doubt it...
> >>
> >> Richard
> >>
> >>> On Jul 10, 2017, at 12:20 PM, David Feuer <david.feuer at gmail.com>
> wrote:
> >>>
> >>> There's another version of heterogeneous equality that takes its
> >>> arguments in the other order. I'm not sure if this is generally useful
> >>> enough to want to include.
> >>>
> >>> -- (:~~:) :: forall j k. j -> k -> *
> >>>
> >>> data OtherEquality :: forall j. j -> forall k. k -> Type where
> >>> OtherRefl :: OtherEquality a a
> >>>
> >>>> On Mon, Jul 10, 2017 at 11:24 AM, Ryan Scott <ryan.gl.scott at gmail.com>
> wrote:
> >>>> I also agree that we should keep HRefl a distinct name, and moreover,
> we
> >>>> should keep :~: and :~~: as distinct datatypes.
> >>>>
> >>>> I'm also on-board with the idea that we should introduce a separate
> >>>> Data.Type.Equality.Hetero module that reexports :~~: and defines
> >>>> heterogeneous counterparts for sym, trans, etc. from
> Data.Type.Equality. I
> >>>> don't have a strong opinion on how they should be named (e.g., sym vs.
> >>>> hsym).
> >>>>
> >>>> Ryan S.
> >>>>
> >>>> _______________________________________________
> >>>> Libraries mailing list
> >>>> Libraries at haskell.org
> >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>>>
> >>> _______________________________________________
> >>> Libraries mailing list
> >>> Libraries at haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170710/0eeb897b/attachment.html>