Heterogeneous equality into base?

[Edward Kmett]

Not sure. You can go back and forth between normal Leibnizian equality and :~: in Haskell.

The notion of an Equality in lens can be seen as a Leibnizian equality, just with an extra set of parameters and encoding it that way lets us compose them with (.) from the Prelude. I suppose if you stripped off your newtype you could do the same here. Other than that? If we didn't have ~ or ~~ already it'd bring something to the table as it provides you some ability to talk about type equality without them in your language. But we do have them.

Sent from my iPhone

> On Jul 10, 2017, at 2:18 PM, David Feuer <david.feuer at gmail.com> wrote:
> 
> 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/7258d1ce/attachment-0001.html>