Re: Heterogeneous equality into base?

Sent from my iPad

On Jul 10, 2017, at 1:11 PM, David Feuer 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 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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries