Heterogeneous equality into base?

[David Feuer]

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)

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
>