Hi!

I agree with you, Andrew, that types should have different names.
However, (H)Refl is not a type. It is a data constructor; so it is a
special kind of value and as such very similar to sym, trans, and
friends. The similarity of Refl to the ordinary functions of the
Heterogeneous module becomes even more obvious when considering that
Refl is a proof, like sym, trans, and so on.

All the best,
Wolfgang

Am Samstag, den 08.07.2017, 21:25 -0400 schrieb Andrew Martin:

Just wanted to weigh in with my two cents. I also prefer to use the

module system for the most part rather than prefixing function names

with something that indicates the data type they operate on. However,

when it comes to types, I would much rather they have different names.

I like that the data constructor of :~~: is HRefl. However, for the

functions sym, trans, etc., I would rather have a

Data.Type.Equality.Hetero that exports all of these without any kind

of prefixes on them. Then there's the question of where we export :~~:

from. It could be exported only from the Hetero module, or it could be

exported from both.

Sent from my iPhone

On Jul 8, 2017, at 7:56 PM, Wolfgang Jeltsch <wolfgang-it@jeltsch.in

fo> wrote:

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/99adcc8804e91161b35ff1d0e5

f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37

[2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5

f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>; 

_______________________________________________

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