Heterogeneous equality into base?
Edward Kmett
ekmett at gmail.com
Mon Jul 10 18:06:43 UTC 2017
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
More information about the Libraries
mailing list