This seems like the kind of thing that first should be fleshed out in its own package. Is there some reason that this module would need to be in base? On Thu, Jul 6, 2017 at 1:56 PM David Feuer wrote:

That seems generally reasonable to me. It'll need the usual discussion process here and then it can be added to `base`. However, I think it should not be added to `Data.Type.Equality`, but rather to a new module, perhaps `Data.Type.Equality.Heterogeneous`. That module will then be able to offer the full complement of basic functions (sym, trans, ...) without stepping on the pre-existing names. I imagine you'll also want one or two extra casting operations, and conversions between `:~:` and `:~~:`. Also, you have called the constructor of this type HRefl in the past, which strikes me as better than Refl.

David

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch wrote:

...

Hi!

The module Data.Type.Equality in the base package contains the type (:~:) for homogeneous equality. However, a type for heterogeneous equality would be very useful as well. I would define such a type as follows:

...

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

data (a :: k) :~~: (b :: l) where

Refl :: a :~~: a

Is there already such a type in the base package? If not, does it make sense to file a feature request (or would such a proposal be likely to not being accepted for some reason)?

All the best, Wolfgang _______________________________________________ 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

Hi libraries@, My 2 cents inlined below :) ~~julm Le jeu. 06 juil. 2017 à 17:15:36 -0400, David Menendez a écrit :

Do you have any code examples that use heterogeneous equality? In the past, GHC has been less flexible with kind variables than with type variables, so I’m not sure what this would enable. I have been using (:~~:) to return two proofs when two type-indexed runtime representations of types are equal: one proof for the equality of kinds, and another proof for the equality of types. For instance, this can be seen in eqVarKi, eqConstKi, and eqTypeKi in https://hackage.haskell.org/package/symantic-6.3.0.20170703/

It's also done here: https://ghc.haskell.org/trac/ghc/wiki/Typeable#Step4:Decomposingarbitrarytyp... Le ven. 07 juil. 2017 à 00:47:50 +0300, Wolfgang Jeltsch a écrit :

I also think that creating a new module Data.Type.Equality.Heterogeneous is the way to go. I would call the constructor of (:~~:) Refl, not HRefl. If you need to distinguish between the Refl of (:~:) and the Refl of (:~~:), you can qualify the name using the module system.

I think it is generally better to use the module system for qualifying names than putting the qualification into the identifiers like in “HRefl”. The module system is made to express qualification. On the other hand, qualification in identifiers is typically done with single letters to save space, which is not very descriptive and quickly results in ambiguities (for example, “m” means “monoid” in “mappend”, but “monad” in “mplus”).

By myself I came up with the name KRefl, but changed it to HRefl to reduce cognitive efforts, when I discovered Richard's thesis which is introducing it. http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf I'm using both Refl and HRefl in the same package, so I prefer to name the latter HRefl instead of H.Refl, to keep a flat namespace which allows open imports and re-exports in parent modules. This also makes grep-ing/web-searching easier, and Haddock generated docs more readable (because there the module paths are hidden). https://www.reddit.com/r/haskell/comments/6j2t1o/on_naming_things_library_de... This said, some of these concerns may not apply to base. Cheers :]

Hi! Yes, I have some code that uses this heterogeneous equality type apparently successfully. I will try to explain the idea behind this code a bit. There is a kind-polymorphic class Q that contains an associated type synonym family that maps instances of Q to types of kind *. This type synonym family shall be injective, and there should be actual witness of this injectivity. This is achieved by requiring every instantiation of Q to provide a heterogeneous equality proof of some kind. The equality must be heterogeneous, because Q is kind-polymorphic. Here is some code that illustrates the idea in more detail:

{-# LANGUAGE GADTs,               PolyKinds,               TypeFamilies,               TypeOperators,               UndecidableInstances,               UndecidableSuperClasses #-}   import GHC.Exts (Constraint)   -- * Heterogeneous equality   data (a :: l) :~~: (b :: k) where        Refl :: a :~~: a   transLike :: a :~~: c -> b :~~: c -> a :~~: b transLike Refl Refl = Refl   -- * Interface   type family C a :: k -> Constraint   class C (F q) q => Q q where        type F q :: *        eq :: (Q q', F q ~ F q') => q :~~: q'   -- * Implementation for []/Bool   class ListQ q where        listEq :: q :~~: []   instance ListQ [] where        listEq = Refl   type instance C Bool = ListQ   instance Q [] where        type F [] = Bool        eq = transLike listEq listEq

The central thing is the eq method, whose complete type is as follows:     forall q q' . (Q q, Q q', F q ~ F q') => q :~~: q' All the best, Wolfgang Am Donnerstag, den 06.07.2017, 17:15 -0400 schrieb David Menendez:

Do you have any code examples that use heterogeneous equality? In the past, GHC has been less flexible with kind variables than with type variables, so I’m not sure what this would enable.

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch wrote:

...

Hi!

The module Data.Type.Equality in the base package contains the type (:~:) for homogeneous equality. However, a type for heterogeneous equality would be very useful as well. I would define such a type as follows:

...

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

data (a :: k) :~~: (b :: l) where

    Refl :: a :~~: a

Is there already such a type in the base package? If not, does it make sense to file a feature request (or would such a proposal be likely to not being accepted for some reason)?

All the best, Wolfgang _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries