Re: Heterogeneous equality into base?

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