Re: Heterogeneous equality into base?

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 wrote:

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

...

On Jul 10, 2017 2:06 PM, "Edward Kmett" wrote:

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