Heterogeneous equality into base?

[Richard Eisenberg]

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