Heterogeneous equality into base?

[Oleg Grenrus]

It's not only a value, it's also a pattern. We have PatternSynonyms, but IMHO it's not a strong argument for having constructors with a same name.

- Oleg

Sent from my iPhone

> On 9 Jul 2017, at 22.47, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
> 
> 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 at 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 at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170710/35e14ca6/attachment-0001.html>