Heterogeneous equality into base?

[Wolfgang Jeltsch]

Hi!

Unfortunately, my wish has not been granted, as I wanted the data
constructor of (:~~:) to be named Refl and (:~~:) to be defined in a
separate module. I see that there are no heterogeneous versions of sym,
trans, and so on in base at the moment. If they will be available at
some time, how will they be called? Will they be named hsym, htrans, and
so on? This would be awful, in my opinion.

In Haskell, we have the module system for qualification. I very well
understand the issues Julien Moutinho pointed out. For example, you
cannot have a module that just reexports all the functions from
Data.Sequence and Data.Map, because you would get name clashes.

However, I think that the solution to these kinds of problems is to fix
the module system. An idea would be to allow for exporting qualified
names. Then a module could import Data.Sequence and Data.Map qualified
as Seq and Map, respectively, and export Seq.empty, Map.empty, and so
on. 

If we try to work around those issues with the module system by putting
qualification into the actual identifiers in the form of single letters
(like in mappend, HRef, and so on), we will be stuck with this
workaround forever, even if the module system will be changed at some
time, because identifiers in core libraries are typically not changed.
Just imagine, we would have followed this practice for the containers
package. We would have identifiers like “smap”, “munion”,
“imintersection”, and so on.

All the best,
Wolfgang

Am Freitag, den 07.07.2017, 08:15 -0700 schrieb Ryan Scott:
> Sorry for only just discovering this thread now. A lot of this
> discussion is in fact moot, since (:~~:) already is in base!
> Specifically, it's landing in Data.Type.Equality [1] in the next
> version of base (bundled with GHC 8.2). Moreover, it's constructor is
> named HRefl, so your wish has been granted ;)
> 
> As for why it's being introduced in base, it ended up being useful for
> the new Type-indexed Typeable that's also landing in GHC 8.2. In
> particular, the eqTypeRep function [2] must return heterogeneous
> equality (:~~:), not homogeneous equality (:~:), since it's possible
> that you'll compare two TypeReps with different kinds.
> 
> Ryan S.
> -----
> [1] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37
> [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>