Heterogeneous equality into base?

[Wolfgang Jeltsch]

Hi!

From https://wiki.haskell.org/Library_submissions, I understood that the
discussion should take place on the GHC Trac and will be moved to the
Libraries Mailing List only in serious cases. Is this the
case?(Interestingly, the link on the aforementioned page contains a
bogus URL. However, I do not know for sure the correct URL to fix this.)

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”).

I will try to come up with an initial implementation of this new
Data.Type.Equality.Heterogeneous module.

All the best,
Wolfgang

Am Donnerstag, den 06.07.2017, 16:55 -0400 schrieb David Feuer:
> 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
> <wolfgang-it at jeltsch.info> 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